588bc99...master · Idris-dev

.travis.yml+23−14

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

88

99matrix:

1010 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

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

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

1414 compiler: ": #GHC 8.2.2"

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

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

2020 compiler: ": #GHC 8.2.2"

2121 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

23− addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.2], 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]}}

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

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

3442 fast-finish: true

3543

3644cache:

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

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

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

121129 fi

122−

130+

123131

124132before_script:

125133 - ORIGINAL_DIR=$(pwd)

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

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

129137 - cd ${PKGNAME}*

130138script:

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

131140###

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

133142 - 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

130130## Issue with GHC on Ubuntu/Fedora

131131

132132There 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+

134135See the following GHC issue page for more information:

135136

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

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

141142

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

143144

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 = {

251251# Additional stuff for the LaTeX preamble.

252252'preamble': r'''

253253\usepackage{lmodern}

254+\usepackage{textalpha}

254255\usepackage[T1]{fontenc}

255256\usepackage[utf8x]{inputenc}

256257\usepackage{titlesec}

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

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

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

302303latex_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')

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

305306]

306307

docs/effects/introduction.rst+2−1

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

1717This tutorial assumes familiarity with pure programming in Idris,

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

1919presented 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.

2122

2223Consider, for example, the following introductory function which

2324illustrates 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:

115115 import Syntax.PreorderReasoning

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

117117 multThree a b c =

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

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

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

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

122− (c * a * b) QED

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

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

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

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

122+ (c * a * b) QED

123123

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

125125be 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

4646

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

4848

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

50+-- heavily discouraged.

4951Data-files: idrisdoc/styles.css

50− jsrts/**/*.js

52+ jsrts/jsbn/*.js

53+ jsrts/*.js

5154 jsrts/jsbn/LICENSE

5255 rts/Makefile

53− rts/**/*.c

54− rts/**/*.h

56+ rts/*.c

57+ rts/seL4/*.c

58+ rts/arduino/*.c

59+ rts/windows/*.c

60+ rts/windows/*.h

61+ rts/*.h

5562 rts/seL4/CMakeLists.txt

5663 rts/seL4/README.md

5764

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

6471 RELEASE-CHECKS.md

6572 idris-tutorial.pdf

6673 man/idris.1

67− samples/**/*.idr

68− samples/**/*.lidr

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

80+ samples/misc/*.lidr

6981

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

7183Extra-source-files:

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

7385 config.mk

7486 custom.mk-alldeps

7587 mkpkg.sh

76− stack-alt.yaml

7788 stack-shell.nix

7889 stack.yaml

7990 stylize.sh

8091 win-release.sh

81−

92+

8293 benchmarks/*.pl

83− benchmarks/**/*.idr

84− benchmarks/**/*.ipkg

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

101+ benchmarks/trivial/*.ipkg

85102 benchmarks/quasigroups/board

86103

87104 icons/*.png

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

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

305322 , aeson >= 0.6 && < 1.5

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

307− , ansi-terminal < 0.10

324+ , ansi-terminal < 0.11

308325 , ansi-wl-pprint < 0.7

309326 , array >= 0.4.0.1 && < 0.6

310327 , base64-bytestring < 1.1

311328 , binary >= 0.8.4.1 && < 0.9

312329 , 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

314331 , bytestring < 0.11

315332 , cheapskate >= 0.1.1.2 && < 0.2

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

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

321338 , fingertree >= 0.1.4.1 && < 0.2

322339 , haskeline >= 0.7 && < 0.8

323340 , ieee754 >= 0.7 && < 0.9

324− , megaparsec >= 7.0.4 && < 8

341+ , megaparsec >= 7.0.4 && < 9

325342 , mtl >= 2.1 && < 2.3

326− , network >= 2.7 && < 2.9

343+ , network >= 2.7 && < 3.1.2

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

328345 , parser-combinators >= 1.0.0

329346 , pretty < 1.2

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

341358 , vector < 0.13

342359 , vector-binary-instances < 0.3

343360 , zip-archive > 0.2.3.5 && < 0.5

344− , fsnotify >= 0.2 && < 2.2

361+ , fsnotify >= 0.2 && < 0.4

345362 , async < 2.3

346363

347364 if !impl(ghc >= 8.0)

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

459476 Default-Language: Haskell2010

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

461478 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

325325instance Monad TC where

326326 return x = OK x

327327 x >>= k = bindTC x k

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

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

329329 fail = Fail.fail

330330#endif

331331

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

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

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

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

99module Idris.Parser.Stack

1010 ( -- * Parsing

1111 Parser(..)

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

7777instance Message ParseError where

7878 messageExtent err = sourcePositionFC pos

7979 where

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

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

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

83+#else

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

85+#endif

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

8287 messageSource err = Just sline

8388 where

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

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

91+#else

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

93+#endif

8594

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

8796prettyError :: ParseError -> String

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

8998

9099{- * Mark and restore -}

91100

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

102+type Mark = P.State String Void

103+#else

92104type Mark = P.State String

105+#endif

93106

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

95108mark :: 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