588bc99..master · Idris-dev

.travis.yml+23−14

since splitsnapshots

unifiedsplit

@@ -8,7 +8,7 @@ env:

8

9matrix:

10 include:

11− - env: CABALVER="2.4" GHCVER="8.6.5" STACKVER="14.15" STYLISH=YES

11+ - env: CABALVER="2.4" GHCVER="8.6.5" STACKVER="15.4" STYLISH=YES

12 addons: {apt: {packages: [cabal-install-2.4,ghc-8.6.5,hscolour], sources: [hvr-ghc]}}

13 - env: CABALVER="2.4" GHCVER="8.2.2" TESTS="lib_doc doc"

14 compiler: ": #GHC 8.2.2"

@@ -19,18 +19,26 @@ matrix:

19 - env: CABALVER="2.4" GHCVER="8.2.2" TESTS="test_c"

20 compiler: ": #GHC 8.2.2"

21 addons: {apt: {packages: [cabal-install-2.4,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}

22− - env: CABALVER="3.0" GHCVER="8.8.2" IDRIS2=YES

22+ - env: CABALVER="2.4" GHCVER="8.4.4" TESTS="lib_doc doc"

23+ compiler: ": #GHC 8.4.4"

24+ addons: {apt: {packages: [cabal-install-2.4,ghc-8.4.4,cppcheck,hscolour], sources: [hvr-ghc]}}

25+ - env: CABALVER="2.4" GHCVER="8.4.4" TESTS="test_js"

26+ compiler: ": #GHC 8.4.4"

27+ addons: {apt: {packages: [cabal-install-2.4,ghc-8.4.4,cppcheck,hscolour], sources: [hvr-ghc]}}

28+ - env: CABALVER="2.4" GHCVER="8.4.4" TESTS="test_c"

29+ compiler: ": #GHC 8.4.4"

30+ addons: {apt: {packages: [cabal-install-2.4,ghc-8.4.4,cppcheck,hscolour], sources: [hvr-ghc]}}

31+ - env: CABALVER="3.0" GHCVER="8.8.3" TESTS="lib_doc doc"

32+ compiler: ": #GHC 8.8.3"

33+ addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.3,cppcheck,hscolour], sources: [hvr-ghc]}}

34+ - env: CABALVER="3.0" GHCVER="8.8.3" TESTS="test_js"

35+ compiler: ": #GHC 8.8.3"

36+ addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.3,cppcheck,hscolour], sources: [hvr-ghc]}}

37+ - env: CABALVER="3.0" GHCVER="8.8.3" TESTS="test_c"

38+ compiler: ": #GHC 8.8.3"

39+ addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.3,cppcheck,hscolour], sources: [hvr-ghc]}}

40+ - env: CABALVER="3.0" GHCVER="8.8.3" IDRIS2=YES

23− addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.2], sources: [hvr-ghc]}}

41+ addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.3], sources: [hvr-ghc]}}

24−

25−# - env: CABALVER="3.0" GHCVER="8.8.1" TESTS="lib_doc doc"

26−# compiler: ": #GHC 8.8.1"

27−# addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.1,cppcheck,hscolour], sources: [hvr-ghc]}}

28−# - env: CABALVER="3.0" GHCVER="8.8.1" TESTS="test_js"

29−# compiler: ": #GHC 8.8.1"

30−# addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.1,cppcheck,hscolour], sources: [hvr-ghc]}}

31−# - env: CABALVER="3.0" GHCVER="8.8.1" TESTS="test_c"

32−# compiler: ": #GHC 8.8.1"

33−# addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.1,cppcheck,hscolour], sources: [hvr-ghc]}}

34 fast-finish: true

42 fast-finish: true

35

43

36cache:

44cache:

@@ -119,7 +127,7 @@ install:

119 cp -a $HOME/.ghc $HOME/.cabsnap/ghc;

127 cp -a $HOME/.ghc $HOME/.cabsnap/ghc;

120 cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin installplan.txt $HOME/.cabsnap/;

128 cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin installplan.txt $HOME/.cabsnap/;

121 fi

129 fi

122−

130+

123

131

124before_script:

132before_script:

125 - ORIGINAL_DIR=$(pwd)

133 - ORIGINAL_DIR=$(pwd)

@@ -128,6 +136,7 @@ before_script:

128 - tar -xf ${ORIGINAL_DIR}/dist/${PKGNAME}*.tar.gz

136 - tar -xf ${ORIGINAL_DIR}/dist/${PKGNAME}*.tar.gz

129 - cd ${PKGNAME}*

137 - cd ${PKGNAME}*

130script:

138script:

139+ - export LD_PRELOAD=/opt/ghc/${GHCVER}/lib/ghc-${GHCVER}/rts/libffi.so.7

131###

140###

132 - echo 'Configure...' && echo -en 'travis_fold:start:script.configure\\r'

141 - echo 'Configure...' && echo -en 'travis_fold:start:script.configure\\r'

133 - cabal v1-configure -f FFI -f CI --enable-tests

142 - cabal v1-configure -f FFI -f CI --enable-tests

INSTALL.md+11−2

@@ -130,7 +130,8 @@ PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig stack build

130## Issue with GHC on Ubuntu/Fedora

131

132There is an upstream issue with GHC on some Ubuntu and Fedora machines.

133−The issue is that for GHC versions greater than 8.4.X linking to libFFI is broken.

133+The issue is that for GHC versions greater than 8.4.X linking to libFFI uses the version of libFFI shipped with GHC, instead of the system version.

134+

134See the following GHC issue page for more information:

135See the following GHC issue page for more information:

135

136

136 <https://gitlab.haskell.org/ghc/ghc/issues/15397>

137 <https://gitlab.haskell.org/ghc/ghc/issues/15397>

@@ -141,4 +142,12 @@ Specifically, one will see an error message along the lines of:

141

142

142> error while loading shared libraries: libffi.so.7: cannot open shared object file: No such file or directory

143> error while loading shared libraries: libffi.so.7: cannot open shared object file: No such file or directory

143

144

144−We have supplied an alternative stack configuration file (`stack-alt.yaml`) that will use a version of GHC prior to the upstream issue being introduced.

145+A workround for this bug is to override the used libffi version (this is what we use on CI):

146+

147+```bash

148+export LD_PRELOAD=/opt/ghc/${GHCVER}/lib/ghc-${GHCVER}/rts/libffi.so.7

149+```

150+

151+## GHC 8.6

152+

153+For reasons that haven't been investigated building the Idris compiler with GHC 8.6 leads to a compiler which doesn't pass test.

docs/conf.py+2−1

@@ -251,6 +251,7 @@ latex_elements = {

251# Additional stuff for the LaTeX preamble.

252'preamble': r'''

253\usepackage{lmodern}

254+\usepackage{textalpha}

254\usepackage[T1]{fontenc}

255\usepackage[T1]{fontenc}

255\usepackage[utf8x]{inputenc}

256\usepackage[utf8x]{inputenc}

256\usepackage{titlesec}

257\usepackage{titlesec}

@@ -300,7 +301,7 @@ latex_elements = {

300# (source start file, target name, title,

301# (source start file, target name, title,

301# author, documentclass [howto, manual, or own class]).

302# author, documentclass [howto, manual, or own class]).

302latex_documents = [

303latex_documents = [

303− ('index', 'idris-documentation-complete.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report'),

304+ # (master_doc, 'idris.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report')

304 ('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'howto'),

305 ('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'howto'),

305]

306]

306

307

docs/effects/introduction.rst+2−1

@@ -17,7 +17,8 @@ exceptions, and verified resource management.

17This tutorial assumes familiarity with pure programming in Idris,

18as described in Sections 1–6 of the main tutorial [1]_. The examples

19presented are tested with Idris and can be found in the

20−examples directory of the Idris repository.

20+examples directory of the Idris repository. The ``-p effects`` flag

21+is needed when starting Idris.

21

22

22Consider, for example, the following introductory function which

23Consider, for example, the following introductory function which

23illustrates the kind of properties which can be expressed in the type

24illustrates the kind of properties which can be expressed in the type

docs/reference/misc.rst+5−5

@@ -115,11 +115,11 @@ Here is an example:

115 import Syntax.PreorderReasoning

116 multThree : (a, b, c : Nat) -> a * b * c = c * a * b

117 multThree a b c =

118− (a * b * c) ={ sym (multAssociative a b c) }=

118+ (a * b * c) ={ sym (multAssociative a b c) }=

119− (a * (b * c)) ={ cong (multCommutative b c) }=

119+ (a * (b * c)) ={ cong (multCommutative b c) }=

120− (a * (c * b)) ={ multAssociative a c b }=

120+ (a * (c * b)) ={ multAssociative a c b }=

121− (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=

121+ (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=

122− (c * a * b) QED

122+ (c * a * b) QED

123

124Note that the parentheses are required -- only a simple expression can

125be on the left of ``={ }=`` or ``QED``. Also, when using preorder

idris-tutorial.pdf

Binary file not shown.

idris.cabal+31−15

@@ -46,12 +46,19 @@ Build-type: Custom

46

47Tested-With: GHC == 7.10.3, GHC == 8.0.1

48

49+-- NOTE: due to https://github.com/haskell/cabal/issues/6125 the use of ** is

50+-- heavily discouraged.

49Data-files: idrisdoc/styles.css

51Data-files: idrisdoc/styles.css

50− jsrts/**/*.js

52+ jsrts/jsbn/*.js

53+ jsrts/*.js

51 jsrts/jsbn/LICENSE

54 jsrts/jsbn/LICENSE

52 rts/Makefile

55 rts/Makefile

53− rts/**/*.c

56+ rts/*.c

57+ rts/seL4/*.c

58+ rts/arduino/*.c

59+ rts/windows/*.c

54− rts/**/*.h

60+ rts/windows/*.h

61+ rts/*.h

55 rts/seL4/CMakeLists.txt

62 rts/seL4/CMakeLists.txt

56 rts/seL4/README.md

63 rts/seL4/README.md

57

64

@@ -64,8 +71,13 @@ Extra-doc-files:

64 RELEASE-CHECKS.md

71 RELEASE-CHECKS.md

65 idris-tutorial.pdf

72 idris-tutorial.pdf

66 man/idris.1

73 man/idris.1

67− samples/**/*.idr

74+ samples/effects/*.idr

75+ samples/misc/*.idr

76+ samples/tutorial/*.idr

77+ samples/ST/*.idr

78+ samples/ST/Graphics/*.idr

79+ samples/ST/Net/*.idr

68− samples/**/*.lidr

80+ samples/misc/*.lidr

69

81

70-- extra-source-files is generated by Setup.hs using `git --ls-files`.

82-- extra-source-files is generated by Setup.hs using `git --ls-files`.

71Extra-source-files:

83Extra-source-files:

@@ -73,15 +85,20 @@ Extra-source-files:

73 config.mk

85 config.mk

74 custom.mk-alldeps

86 custom.mk-alldeps

75 mkpkg.sh

87 mkpkg.sh

76− stack-alt.yaml

77 stack-shell.nix

88 stack-shell.nix

78 stack.yaml

89 stack.yaml

79 stylize.sh

90 stylize.sh

80 win-release.sh

91 win-release.sh

81−

92+

82 benchmarks/*.pl

93 benchmarks/*.pl

83− benchmarks/**/*.idr

94+ benchmarks/fasta/*.idr

95+ benchmarks/fasta/*.ipkg

96+ benchmarks/pidigits/*.idr

97+ benchmarks/pidigits/*.ipkg

98+ benchmarks/quasigroups/*.idr

99+ benchmarks/quasigroups/*.ipkg

100+ benchmarks/trivial/*.idr

84− benchmarks/**/*.ipkg

101+ benchmarks/trivial/*.ipkg

85 benchmarks/quasigroups/board

102 benchmarks/quasigroups/board

86

103

87 icons/*.png

104 icons/*.png

@@ -304,13 +321,13 @@ Library

304 Build-depends: base >=4 && <5

321 Build-depends: base >=4 && <5

305 , aeson >= 0.6 && < 1.5

322 , aeson >= 0.6 && < 1.5

306 , annotated-wl-pprint >= 0.7 && < 0.8

323 , annotated-wl-pprint >= 0.7 && < 0.8

307− , ansi-terminal < 0.10

324+ , ansi-terminal < 0.11

308 , ansi-wl-pprint < 0.7

325 , ansi-wl-pprint < 0.7

309 , array >= 0.4.0.1 && < 0.6

326 , array >= 0.4.0.1 && < 0.6

310 , base64-bytestring < 1.1

327 , base64-bytestring < 1.1

311 , binary >= 0.8.4.1 && < 0.9

328 , binary >= 0.8.4.1 && < 0.9

312 , blaze-html >= 0.6.1.3 && < 0.10

329 , blaze-html >= 0.6.1.3 && < 0.10

313− , blaze-markup >= 0.5.2.1 && < 0.9

330+ , blaze-markup >= 0.5.2.1 && < 0.10

314 , bytestring < 0.11

331 , bytestring < 0.11

315 , cheapskate >= 0.1.1.2 && < 0.2

332 , cheapskate >= 0.1.1.2 && < 0.2

316 , code-page >= 0.1 && < 0.3

333 , code-page >= 0.1 && < 0.3

@@ -321,9 +338,9 @@ Library

321 , fingertree >= 0.1.4.1 && < 0.2

338 , fingertree >= 0.1.4.1 && < 0.2

322 , haskeline >= 0.7 && < 0.8

339 , haskeline >= 0.7 && < 0.8

323 , ieee754 >= 0.7 && < 0.9

340 , ieee754 >= 0.7 && < 0.9

324− , megaparsec >= 7.0.4 && < 8

341+ , megaparsec >= 7.0.4 && < 9

325 , mtl >= 2.1 && < 2.3

342 , mtl >= 2.1 && < 2.3

326− , network >= 2.7 && < 2.9

343+ , network >= 2.7 && < 3.1.2

327 , optparse-applicative >= 0.13 && < 0.16

344 , optparse-applicative >= 0.13 && < 0.16

328 , parser-combinators >= 1.0.0

345 , parser-combinators >= 1.0.0

329 , pretty < 1.2

346 , pretty < 1.2

@@ -341,7 +358,7 @@ Library

341 , vector < 0.13

358 , vector < 0.13

342 , vector-binary-instances < 0.3

359 , vector-binary-instances < 0.3

343 , zip-archive > 0.2.3.5 && < 0.5

360 , zip-archive > 0.2.3.5 && < 0.5

344− , fsnotify >= 0.2 && < 2.2

361+ , fsnotify >= 0.2 && < 0.4

345 , async < 2.3

362 , async < 2.3

346

363

347 if !impl(ghc >= 8.0)

364 if !impl(ghc >= 8.0)

@@ -459,4 +476,3 @@ Executable idris-codegen-node

459 Default-Language: Haskell2010

476 Default-Language: Haskell2010

460 ghc-prof-options: -auto-all -caf-all

477 ghc-prof-options: -auto-all -caf-all

461 ghc-options: -threaded -rtsopts -funbox-strict-fields

478 ghc-options: -threaded -rtsopts -funbox-strict-fields

462−

src/Idris/Core/TT.hs+1−1

@@ -325,7 +325,7 @@ bindTC x k = case x of

325instance Monad TC where

326 return x = OK x

327 x >>= k = bindTC x k

328−#if !(MIN_VERSION_base(4,12,0))

328+#if !(MIN_VERSION_base(4,13,0))

329 fail = Fail.fail

330#endif

331

src/Idris/Parser/Stack.hs+14−1

@@ -5,7 +5,7 @@ Description : Idris parser stack and its primitives.

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}

8+{-# LANGUAGE CPP, ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}

9module Idris.Parser.Stack

10 ( -- * Parsing

11 Parser(..)

@@ -77,11 +77,20 @@ parseErrorOffset = P.errorOffset . parseError

77instance Message ParseError where

78 messageExtent err = sourcePositionFC pos

79 where

80+#if MIN_VERSION_megaparsec(8,0,0)

81+ P.PosState {P.pstateSourcePos = pos} =

82+ P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)

83+#else

80 (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)

84 (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)

85+#endif

81 messageText = PP.text . init . P.parseErrorTextPretty . parseError

86 messageText = PP.text . init . P.parseErrorTextPretty . parseError

82 messageSource err = Just sline

87 messageSource err = Just sline

83 where

88 where

89+#if MIN_VERSION_megaparsec(8,0,0)

90+ (sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)

91+#else

84 (_, sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)

92 (_, sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)

93+#endif

85

94

86-- | A fully formatted parse error, with caret and bar, etc.

95-- | A fully formatted parse error, with caret and bar, etc.

87prettyError :: ParseError -> String

96prettyError :: ParseError -> String

@@ -89,7 +98,11 @@ prettyError = P.errorBundlePretty . unParseError

89

98

90{- * Mark and restore -}

99{- * Mark and restore -}

91

100

101+#if MIN_VERSION_megaparsec(8,0,0)

102+type Mark = P.State String Void

103+#else

92type Mark = P.State String

104type Mark = P.State String

105+#endif

93

106

94-- | Retrieve the parser state so we can restart from this point later.

107-- | Retrieve the parser state so we can restart from this point later.

95mark :: Parsing m => m Mark

108mark :: Parsing m => m Mark

stack-11.22.yamlnew file+21

@@ -0,0 +1,21 @@

1+#recheck extra-deps next on resolver or cabal file change

2+resolver: lts-11.22

3+

4+extra-deps:

5+- cheapskate-0.1.1.2

6+- megaparsec-7.0.5

7+- Cabal-2.4.1.0

8+- network-3.1.1.1

9+- parser-combinators-1.0.0

10+

11+flags:

12+ idris:

13+ FFI: true

14+ GMP: true

15+

16+ghc-options:

17+ idris: -fwarn-unused-imports -fwarn-unused-binds

18+

19+nix:

20+ enable: false

21+ shell-file: stack-shell.nix

stack-12.26.yamlnew file+20

@@ -0,0 +1,20 @@

1+#recheck extra-deps next on resolver or cabal file change

2+resolver: lts-12.26

3+

4+extra-deps:

5+- cheapskate-0.1.1.2

6+- megaparsec-7.0.5

7+- Cabal-2.4.1.0

8+- network-3.1.1.1

9+

10+flags:

11+ idris:

12+ FFI: true

13+ GMP: true

14+

15+ghc-options:

16+ idris: -fwarn-unused-imports -fwarn-unused-binds

17+

18+nix:

19+ enable: false

20+ shell-file: stack-shell.nix

stack-15.3.yamlnew file+17

@@ -0,0 +1,17 @@

1+#recheck extra-deps next on resolver or cabal file change

2+resolver: lts-15.3

3+

4+extra-deps:

5+- cheapskate-0.1.1.2

6+

7+flags:

8+ idris:

9+ FFI: true

10+ GMP: true

11+

12+ghc-options:

13+ idris: -fwarn-unused-imports -fwarn-unused-binds

14+

15+nix:

16+ enable: false

17+ shell-file: stack-shell.nix

stack-15.4.yamlnew file+17

@@ -0,0 +1,17 @@

1+#recheck extra-deps next on resolver or cabal file change

2+resolver: lts-15.4

3+

4+extra-deps:

5+- cheapskate-0.1.1.2

6+

7+flags:

8+ idris:

9+ FFI: true

10+ GMP: true

11+

12+ghc-options:

13+ idris: -fwarn-unused-imports -fwarn-unused-binds

14+

15+nix:

16+ enable: false

17+ shell-file: stack-shell.nix

stack-alt.yamldeleted−25

@@ -1,25 +0,0 @@

1−#recheck extra-deps next on resolver or cabal file change

2−resolver: lts-11.4

3−

4−packages:

5− - location: .

6−

7−extra-deps:

8− - network-2.8.0.0@sha256:aae171e6c6028a7791dbe4de5b9d2da398056359e3cc7927465ffa3cdae1aa0b

9− - Cabal-2.2.0.1@sha256:2a80d8fb655474f0eaeb20434c47f64f84e6302e55973056f00df8ca050b9683

10− - megaparsec-7.0.4

11− - parser-combinators-1.0.0

12− - zip-archive-0.3.3@sha256:47cf2d66cc8e237f7226837758e1b041e24048ef3820d3d10276c500edb921bf

13− - containers-0.5.11.0@sha256:28ad7337057442f75bc689315ab4ec7bdf5e6b2c39668f306672cecd82c02798

14−

15−flags:

16− idris:

17− FFI: true

18− GMP: true

19−

20−ghc-options:

21− idris: -fwarn-unused-imports -fwarn-unused-binds

22−

23−nix:

24− enable: false

25− shell-file: stack-shell.nix

stack.yamlmode 100644 → 120000+1−26

@@ -1,26 +0,0 @@

1−#recheck extra-deps next on resolver or cabal file change

2−resolver: lts-13.21

3−

4−extra-deps:

5− - network-2.8.0.0@sha256:aae171e6c6028a7791dbe4de5b9d2da398056359e3cc7927465ffa3cdae1aa0b

6− - megaparsec-7.0.4

7− - parser-combinators-1.0.0

8− - zip-archive-0.3.3@sha256:47cf2d66cc8e237f7226837758e1b041e24048ef3820d3d10276c500edb921bf

9− - containers-0.5.11.0@sha256:28ad7337057442f75bc689315ab4ec7bdf5e6b2c39668f306672cecd82c02798

10− - tasty-rerun-1.1.14@sha256:ba9c19a281535bea566e1044bc02c36ef17abcb310af4b6a149ec11780c7ce35

11− - binary-0.8.7.0@sha256:ae3e6cca723ac55c54bbb3fa771bcf18142bc727afd57818e66d6ee6c8044f12

12− - text-1.2.4.0@sha256:8c24450feb8e3bbb7ea3e17af24ef57e85db077c4bf53e5bcc345b283d1b1d5b

13− - HsYAML-0.2.1.0@sha256:e4677daeba57f7a1e9a709a1f3022fe937336c91513e893166bd1f023f530d68,5311

14− - HsYAML-aeson-0.2.0.0@sha256:04796abfc01cffded83f37a10e6edba4f0c0a15d45bef44fc5bb4313d9c87757,1791

15−

16−flags:

17− idris:

18− FFI: true

19− GMP: true

20−

21−ghc-options:

22− idris: -fwarn-unused-imports -fwarn-unused-binds

23−

24−nix:

25− enable: false

26− shell-file: stack-shell.nix

@@ -0,0 +1 @@

1+stack-15.4.yaml