161573f...master · Idris-dev

git.iko.soy/Idris-dev

610 files changed+891−541

since splitsnapshots

unifiedsplit

.travis.yml+53−35

@@ -1,5 +1,4 @@

1−dist: trusty

2−sudo: false

1+dist: xenial

43language: c

@@ -9,35 +8,37 @@ env:

109matrix:

1110 include:

12− - 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

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

14− - env: CABALVER="2.2" GHCVER="7.10.3" TESTS="test_c"

15− compiler: ": #GHC 7.10.3"

16− addons: {apt: {packages: [cabal-install-2.2,ghc-7.10.3,cppcheck,hscolour], sources: [hvr-ghc]}}

17−# Disabled because it's always timing out

18−# - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"

19−# compiler: ": #GHC 8.0.1"

20−# addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,cppcheck,hscolour], sources: [hvr-ghc]}}

21− - env: CABALVER="2.0" GHCVER="8.2.2" TESTS="lib_doc doc"

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

2214 compiler: ": #GHC 8.2.2"

23− addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}

24− - env: CABALVER="2.0" GHCVER="8.2.2" TESTS="test_js"

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

16+ - env: CABALVER="2.4" GHCVER="8.2.2" TESTS="test_js"

2517 compiler: ": #GHC 8.2.2"

26− addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}

27− - env: CABALVER="2.0" GHCVER="8.2.2" TESTS="test_c"

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

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

2820 compiler: ": #GHC 8.2.2"

29− addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}

30−#TODO: The idris built with those fails due to libffi dynamic linking version mismatch.

31−# Caused by the GHC backport to Trusty?

32−# - env: CABALVER="2.2" GHCVER="8.4.1" TESTS="lib_doc doc"

33−# compiler: ": #GHC 8.4.1"

34−# addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,cppcheck,hscolour], sources: [hvr-ghc]}}

35−# - env: CABALVER="2.2" GHCVER="8.4.1" TESTS="test_js"

36−# compiler: ": #GHC 8.4.1"

37−# addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,cppcheck,hscolour], sources: [hvr-ghc]}}

38−# - env: CABALVER="2.2" GHCVER="8.4.1" TESTS="test_c"

39−# compiler: ": #GHC 8.4.1"

40−# addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,cppcheck,hscolour], sources: [hvr-ghc]}}

21+ addons: {apt: {packages: [cabal-install-2.4,ghc-8.2.2,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]}}

4142 fast-finish: true

4243

4344cache:

@@ -56,7 +57,7 @@ before_install:

5657 - unset CC

5758 - if [[ $TRAVIS_OS_NAME == 'linux' ]];

5859 then

59− export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$HOME/.cabal/bin:$PATH;

60+ export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$HOME/.cabal/bin:$HOME/opt/scheme/bin/:$PATH;

6061 export SED=sed;

6162 export ZCAT=zcat;

6263 fi

@@ -71,6 +72,21 @@ before_install:

7172 export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:$PKG_CONFIG_PATH;

7273 fi

7374 - if [ -n "$STYLISH" ]; then ./stylize.sh; exit $?; fi

75+ - if [ -n "$IDRIS2" ];

76+ then

77+ git clone https://github.com/edwinb/Idris2 &&

78+ wget https://github.com/cisco/ChezScheme/archive/v9.5.2.tar.gz &&

79+ tar xvzf v9.5.2.tar.gz &&

80+ cd ChezScheme-9.5.2 &&

81+ ./configure --threads --installprefix=$HOME/opt/scheme &&

82+ make -j install &&

83+ cd .. &&

84+ cabal v1-update &&

85+ travis_wait cabal v1-install &&

86+ cd Idris2 &&

87+ make idris2 && make base && make contrib;

88+ exit $?;

89+ fi

7490

7591install:

7692 - which cabal

@@ -88,7 +104,7 @@ install:

88104 # causing cabal's default configuration (jobs: $ncpus)

89105 # to run into the GHC #9221 bug which can result in longer build-times.

90106 - $SED -i -r 's/(^jobs:).*/\1 2/' $HOME/.cabal/config

91− - cabal install -f FFI --only-dependencies --enable-tests --dry -v > installplan.txt

107+ - cabal v1-install -f FFI --only-dependencies --enable-tests --dry -v > installplan.txt

92108 - $SED -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt

93109 # check whether current requested install-plan matches cached package-db snapshot

94110 - if diff -u installplan.txt $HOME/.cabsnap/installplan.txt;

@@ -101,7 +117,7 @@ install:

101117 echo "cabal build-cache MISS";

102118 rm -rf $HOME/.cabsnap;

103119 mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;

104− cabal install -f FFI --only-dependencies --enable-tests;

120+ cabal v1-install -f FFI --only-dependencies --enable-tests;

105121 fi

106122 # snapshot package-db on cache miss

107123 - if [ ! -d $HOME/.cabsnap ];

@@ -112,28 +128,30 @@ install:

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

113129 fi

114130

131+

115132before_script:

116133 - ORIGINAL_DIR=$(pwd)

117− - cabal sdist

134+ - cabal v1-sdist

118135 - cd ..

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

120137 - cd ${PKGNAME}*

121138script:

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

122140###

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

124− - cabal configure -f FFI -f CI --enable-tests

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

125143 - echo -en 'travis_fold:end:script.configure\\r'

126144###

127145 - echo 'Build...' && echo -en 'travis_fold:start:script.build\\r'

128− - cabal build

146+ - cabal v1-build

129147 - echo -en 'travis_fold:end:script.build\\r'

130148###

131149 - echo 'Copy...' && echo -en 'travis_fold:start:script.copy\\r'

132− - cabal copy

150+ - cabal v1-copy

133151 - echo -en 'travis_fold:end:script.copy\\r'

134152###

135153 - echo 'Register...' && echo -en 'travis_fold:start:script.register\\r'

136− - cabal register

154+ - cabal v1-register

137155 - echo -en 'travis_fold:end:script.register\\r'

138156###

139157 - echo 'Cppcheck...' && echo -en 'travis_fold:start:script.cppcheck\\r'

CHANGELOG.md+3

@@ -1,3 +1,6 @@

1+# New since last release

2++ Updated to work with GHC 8.8 and cabal 3.0

14# New in 1.3.2

25+ Documentation added to proof section

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.

Makefile+4−4

@@ -30,15 +30,15 @@ stylize:

3030 ./stylize.sh

3131

3232test_c:

33− $(CABAL) test $(ARGS) --test-options \

33+ $(CABAL) v1-test $(ARGS) --test-options \

3434 "$(TEST-ARGS) --rerun-update +RTS -N$(TEST-JOBS) -RTS"

3535

3636test_js:

37− $(CABAL) test $(ARGS) --test-options \

37+ $(CABAL) v1-test $(ARGS) --test-options \

3838 "$(TEST-ARGS) --node --rerun-update +RTS -N$(TEST-JOBS) -RTS"

3939

4040test_update:

41− $(CABAL) test $(ARGS) --test-options \

41+ $(CABAL) v1-test $(ARGS) --test-options \

4242 "$(TEST-ARGS) --accept +RTS -N$(TEST-JOBS) -RTS"

4343

4444test_clean:

@@ -56,7 +56,7 @@ linecount:

5656

5757#Note: this doesn't yet link to Hackage properly

5858doc: dist/setup-config

59− $(CABAL) haddock --hyperlink-source --html --hoogle --html-location="https://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"

59+ $(CABAL) v1-haddock --hyperlink-source --html --hoogle --html-location="https://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"

6060

6161lib_doc:

6262 $(MAKE) -C libs IDRIS=../../dist/build/idris/idris doc

README.md+3

@@ -44,3 +44,6 @@ where some interesting projects are being hosted.

4444

4545For those interested in contributing to Idris directly we kindly ask that

4646prospective developers please consult the [Contributing Guide](CONTRIBUTING.md) first.

47+

48+[Idris 2](https://github.com/edwinb/Idris2) is an early preview of the next generation

49+of Idris, implemented in Idris.

Setup.hs−33

@@ -215,36 +215,6 @@ idrisConfigure _ flags pkgdesc local = do

215215 autogenComponentModulesDir lbi _ = autogenModulesDir lbi

216216#endif

217217

218−idrisPreSDist args flags = do

219− let dir = S.fromFlag (S.sDistDirectory flags)

220− let verb = S.fromFlag (S.sDistVerbosity flags)

221− generateVersionModule verb "src" True

222− generateBuildFlagsModule verb "src" []

223− generateTargetModule verb "src" "./libs"

224− generateToolchainModule verb "src" Nothing

225− preSDist simpleUserHooks args flags

226−

227−idrisSDist sdist pkgDesc bi hooks flags = do

228− pkgDesc' <- addGitFiles pkgDesc

229− sdist pkgDesc' bi hooks flags

230− where

231− addGitFiles :: PackageDescription -> IO PackageDescription

232− addGitFiles pkgDesc = do

233− files <- gitFiles

234− return $ pkgDesc { extraSrcFiles = extraSrcFiles pkgDesc ++ files}

235− gitFiles :: IO [FilePath]

236− gitFiles = liftM lines (readProcess "git" ["ls-files"] "")

237−

238−idrisPostSDist args flags desc lbi = do

239− Control.Exception.catch (do let file = "src" </> "Version_idris" Px.<.> "hs"

240− let targetFile = "src" </> "Target_idris" Px.<.> "hs"

241− putStrLn $ "Removing generated modules:\n "

242− ++ file ++ "\n" ++ targetFile

243− removeFile file

244− removeFile targetFile)

245− (\e -> let e' = (e :: SomeException) in return ())

246− postSDist simpleUserHooks args flags desc lbi

247−

248218#if !(MIN_VERSION_Cabal(2,0,0))

249219rewriteFileEx :: Verbosity -> FilePath -> String -> IO ()

250220rewriteFileEx _ = rewriteFile

@@ -353,8 +323,5 @@ main = defaultMainWithHooks $ simpleUserHooks

353323 , postInst = \_ flags pkg local ->

354324 idrisInstall (S.fromFlag $ S.installVerbosity flags)

355325 NoCopyDest pkg local

356− , preSDist = idrisPreSDist

357− , sDistHook = idrisSDist (sDistHook simpleUserHooks)

358− , postSDist = idrisPostSDist

359326 , testHook = idrisTestHook

360327 }

appveyor.yml+3−3

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

11version: 1.0.{build}

22init:

33- ps: >-

4− choco install cabal --version=2.4.1.0 --no-progress

4+ choco install cabal --no-progress

66 mkdir C:\ghc

8− Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"

8+ Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.8.2/ghc-8.8.2-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"

1010 7z x C:\ghc\ghc.tar.xz -oC:\ghc

1111

1212 7z x C:\ghc\ghc.tar -oC:\ghc

1313

14− $env:PATH="$env:PATH;c:\ghc\ghc-8.4.3\bin;$HOME\AppData\Roaming\cabal\bin"

14+ $env:PATH="$env:PATH;c:\ghc\ghc-8.8.2\bin;$HOME\AppData\Roaming\cabal\bin"

1515

1616 cabal v1-update

1717

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/codegen.rst+4−4

@@ -36,10 +36,10 @@ issue the following command:

3636 $ idris --codegen javascript hello.idr -o hello.js

3737

3838

39−Idris can produce very big chunks of JavaScript code (hello world

40−weighs in at 1500 lines). However, the generated code can be minified

41−using the `closure-compiler

42−<https://developers.google.com/closure/compiler/>`__ from Google.

39+Idris can produce big chunks of JavaScript code (hello world weighs in at about

40+60 lines). However, the generated code can be minified using the

41+`closure-compiler <https://developers.google.com/closure/compiler/>`__ from

42+Google.

4343

4444::

4545

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+101−47

@@ -1,6 +1,7 @@

1+Cabal-Version: 2.4

12Name: idris

23Version: 1.3.2

3−License: BSD3

4+License: BSD-3-Clause

45License-file: LICENSE

56Author: Edwin Brady

67Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>

@@ -41,42 +42,25 @@ Description: Idris is a general purpose language with full dependent types.

4142 .

4243 * Hugs style interactive environment

4344

44−Cabal-Version: >= 1.22

45−

4645Build-type: Custom

4746

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

4948

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

50+-- heavily discouraged.

5051Data-files: idrisdoc/styles.css

51− jsrts/jsbn/jsbn-browser.js

52− jsrts/jsbn/jsbn-node.js

53− jsrts/Runtime-common.js

54− jsrts/Runtime-javascript.js

55− jsrts/Runtime-node.js

52+ jsrts/jsbn/*.js

53+ jsrts/*.js

5654 jsrts/jsbn/LICENSE

57− rts/arduino/idris_main.c

58− rts/idris_bitstring.c

59− rts/idris_bitstring.h

60− rts/idris_gc.c

61− rts/idris_gc.h

62− rts/idris_gmp.c

63− rts/idris_gmp.h

64− rts/idris_heap.c

65− rts/idris_heap.h

66− rts/idris_main.c

67− rts/idris_net.c

68− rts/idris_net.h

69− rts/idris_opts.c

70− rts/idris_opts.h

71− rts/idris_rts.c

72− rts/idris_rts.h

73− rts/idris_stats.c

74− rts/idris_stats.h

75− rts/idris_stdfgn.c

76− rts/idris_stdfgn.h

77− rts/mini-gmp.c

78− rts/mini-gmp.h

79− rts/libtest.c

55+ rts/Makefile

56+ rts/*.c

57+ rts/seL4/*.c

58+ rts/arduino/*.c

59+ rts/windows/*.c

60+ rts/windows/*.h

61+ rts/*.h

62+ rts/seL4/CMakeLists.txt

63+ rts/seL4/README.md

8064

8165Extra-doc-files:

8266 CHANGELOG.md

@@ -86,13 +70,75 @@ Extra-doc-files:

8670 README.md

8771 RELEASE-CHECKS.md

8872 idris-tutorial.pdf

73+ man/idris.1

8974 samples/effects/*.idr

9075 samples/misc/*.idr

91− samples/misc/*.lidr

9276 samples/tutorial/*.idr

77+ samples/ST/*.idr

78+ samples/ST/Graphics/*.idr

79+ samples/ST/Net/*.idr

80+ samples/misc/*.lidr

9381

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

9583Extra-source-files:

84+ Makefile

85+ config.mk

86+ custom.mk-alldeps

87+ mkpkg.sh

88+ stack-shell.nix

89+ stack.yaml

90+ stylize.sh

91+ win-release.sh

92+

93+ benchmarks/*.pl

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

102+ benchmarks/quasigroups/board

103+

104+ icons/*.png

105+ icons/*.ico

106+ icons/*.rc

107+ icons/*.svg

108+ icons/*.xml

109+

110+ libs/**/*.idr

111+ libs/**/*.ipkg

112+ libs/**/*.txt

113+ libs/Makefile

114+ libs/base/Makefile

115+ libs/contrib/Makefile

116+ libs/effects/Makefile

117+ libs/prelude/Makefile

118+ libs/pruviloj/Makefile

119+

120+ scripts/generate-multi-ghc-travis-template

121+ scripts/runidris

122+ scripts/runidris-node

123+

124+ src/.ghci

125+

126+ test/*.md

127+ test/*.hs

128+ test/**/*.idr

129+ test/**/*.lidr

130+ test/**/*.ipkg

131+ test/**/*.out

132+ test/**/*.sh

133+ test/**/*.c

134+ test/**/*.h

135+ test/**/*.in

136+ test/**/*.txt

137+ test/**/*.js

138+ test/base001/Makefile

139+ test/ffi004/theOtherType

140+ test/ffi004/theType

141+ test/scripts/timeout

96142

97143source-repository head

98144 type: git

@@ -100,7 +146,7 @@ source-repository head

100146

101147custom-setup

102148 setup-depends:

103− Cabal >= 1.10 && <2.5,

149+ Cabal >= 2.4 && < 3.1,

104150 base >= 4 && <5,

105151 directory,

106152 filepath,

@@ -261,26 +307,29 @@ Library

261307 Util.Pretty

262308 , Util.Net

263309

264−

265−

266− -- Auto Generated

267310 , Paths_idris

268311 , Version_idris

269312 , Tools_idris

270313 , BuildFlags_idris

271314

315+ -- Auto Generated

316+ Autogen-modules: Paths_idris

317+ , Version_idris

318+ , Tools_idris

319+ , BuildFlags_idris

320+

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

273322 , aeson >= 0.6 && < 1.5

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

275− , ansi-terminal < 0.10

324+ , ansi-terminal < 0.11

276325 , ansi-wl-pprint < 0.7

277326 , array >= 0.4.0.1 && < 0.6

278327 , base64-bytestring < 1.1

279328 , binary >= 0.8.4.1 && < 0.9

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

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

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

282331 , bytestring < 0.11

283− , cheapskate >= 0.1.1 && < 0.2

332+ , cheapskate >= 0.1.1.2 && < 0.2

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

285334 , containers >= 0.5 && < 0.7

286335 , deepseq < 1.5

@@ -289,10 +338,10 @@ Library

289338 , fingertree >= 0.1.4.1 && < 0.2

290339 , haskeline >= 0.7 && < 0.8

291340 , ieee754 >= 0.7 && < 0.9

292− , megaparsec >= 7.0.4 && < 8

341+ , megaparsec >= 7.0.4 && < 9

293342 , mtl >= 2.1 && < 2.3

294− , network >= 2.7 && < 2.9

295− , optparse-applicative >= 0.13 && < 0.15

343+ , network >= 2.7 && < 3.1.2

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

296345 , parser-combinators >= 1.0.0

297346 , pretty < 1.2

298347 , process < 1.7

@@ -300,8 +349,8 @@ Library

300349 , safe >= 0.3.9

301350 , split < 0.3

302351 , terminal-size < 0.4

303− , text >=1.2.1.0 && < 1.3

304− , time >= 1.4 && < 1.9

352+ , text >=1.2.1.0 && < 1.4

353+ , time >= 1.4 && < 2.0

305354 , transformers >= 0.5 && < 0.6

306355 , uniplate >=1.6 && < 1.7

307356 , unordered-containers < 0.3

@@ -309,11 +358,12 @@ Library

309358 , vector < 0.13

310359 , vector-binary-instances < 0.3

311360 , zip-archive > 0.2.3.5 && < 0.5

312− , fsnotify >= 0.2 && < 2.2

361+ , fsnotify >= 0.2 && < 0.4

313362 , async < 2.3

314363

315364 if !impl(ghc >= 8.0)

316− Build-Depends: semigroups == 0.18.*

365+ Build-Depends: semigroups == 0.18.*

366+ , fail == 4.9.0.*

317367

318368 Default-Language: Haskell2010

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

@@ -332,6 +382,7 @@ Library

332382 cpp-options: -DIDRIS_GMP

333383 if flag(freestanding)

334384 other-modules: Target_idris

385+ autogen-modules: Target_idris

335386 cpp-options: -DFREESTANDING

336387 if flag(CI)

337388 ghc-options: -Werror

@@ -365,7 +416,7 @@ Test-suite regression-and-feature-tests

365416 , filepath

366417 , directory

367418 , haskeline >= 0.7

368− , optparse-applicative >= 0.13 && < 0.15

419+ , optparse-applicative >= 0.13 && < 0.16

369420 , tagged

370421 , tasty >= 0.8

371422 , tasty-golden >= 2.0

@@ -380,6 +431,7 @@ Test-suite regression-and-feature-tests

380431

381432Executable idris-codegen-c

382433 Main-is: Main.hs

434+ autogen-modules: Paths_idris

383435 other-modules: Paths_idris

384436 hs-source-dirs: codegen/idris-codegen-c

385437

@@ -395,6 +447,7 @@ Executable idris-codegen-c

395447

396448Executable idris-codegen-javascript

397449 Main-is: Main.hs

450+ autogen-modules: Paths_idris

398451 other-modules: Paths_idris

399452 hs-source-dirs: codegen/idris-codegen-javascript

400453

@@ -410,6 +463,7 @@ Executable idris-codegen-javascript

410463

411464Executable idris-codegen-node

412465 Main-is: Main.hs

466+ autogen-modules: Paths_idris

413467 other-modules: Paths_idris

414468 hs-source-dirs: codegen/idris-codegen-node

415469

libs/base/Control/Isomorphism.idr+20−23

@@ -17,21 +17,22 @@ record Iso a b where

1717

1818-- Isomorphism properties

1919

20−||| Isomorphism is Reflexive

20+||| Isomorphism is reflexive

2121isoRefl : Iso a a

22−isoRefl = MkIso id id (\x => Refl) (\x => Refl)

22+isoRefl = MkIso id id (\_ => Refl) (\_ => Refl)

2323

2424||| Isomorphism is transitive

2525isoTrans : Iso a b -> Iso b c -> Iso a c

2626isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =

27− MkIso (\x => to' (to x))

28− (\y => from (from' y))

29− (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=

30− (to' (from' y)) ={ toFrom' y }=

31− y QED)

32− (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=

33− (from (to x)) ={ fromTo x }=

34− x QED)

27+ MkIso xto xfrom xtoFrom xfromTo where

28+ xto : a -> c

29+ xto = to' . to

30+ xfrom : c -> a

31+ xfrom = from . from'

32+ xtoFrom : (z : c) -> xto (xfrom z) = z

33+ xtoFrom z = rewrite toFrom $ from' z in toFrom' z

34+ xfromTo : (x : a) -> xfrom (xto x) = x

35+ xfromTo x = rewrite fromTo' (to x) in fromTo x

3536

3637Category Iso where

3738 id = isoRefl

@@ -99,8 +100,7 @@ eitherBotRight = isoTrans eitherComm eitherBotLeft

99100

100101||| Isomorphism is a congruence with regards to disjunction

101102eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')

102−eitherCong {a = a} {a' = a'} {b = b} {b' = b'}

103− (MkIso to from toFrom fromTo)

103+eitherCong (MkIso to from toFrom fromTo)

104104 (MkIso to' from' toFrom' fromTo') =

105105 MkIso (eitherMap to to') (eitherMap from from') ok1 ok2

106106 where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'

@@ -143,9 +143,7 @@ pairAssoc = MkIso to from ok1 ok2

143143

144144||| Conjunction with truth is a no-op

145145pairUnitRight : Iso (a, ()) a

146−pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok

147− where ok : (x : (a, ())) -> (fst x, ()) = x

148− ok (x, ()) = Refl

146+pairUnitRight = MkIso fst (\x => (x, ())) (\_ => Refl) (\(_, ()) => Refl)

149147

150148||| Conjunction with truth is a no-op

151149pairUnitLeft : Iso ((), a) a

@@ -161,8 +159,7 @@ pairBotRight = isoTrans pairComm pairBotLeft

161159

162160||| Isomorphism is a congruence with regards to conjunction

163161pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')

164−pairCong {a = a} {a' = a'} {b = b} {b' = b'}

165− (MkIso to from toFrom fromTo)

162+pairCong (MkIso to from toFrom fromTo)

166163 (MkIso to' from' toFrom' fromTo') =

167164 MkIso to'' from'' iso1 iso2

168165 where to'' : (a, b) -> (a', b')

@@ -205,7 +202,7 @@ distribLeft = MkIso to from toFrom fromTo

205202

206203||| Products distribute over sums

207204distribRight : Iso (a, Either b c) (Either (a, b) (a, c))

208−distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm

205+distribRight = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm

209206

210207

211208-- Enable preorder reasoning syntax over isomorphisms

@@ -222,7 +219,7 @@ step a iso1 iso2 = isoTrans iso1 iso2

222219-- Isomorphisms over Maybe

223220||| Isomorphism is a congruence with respect to Maybe

224221maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)

225−maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2

222+maybeCong (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2

226223 where ok1 : (y : Maybe b) -> map to (map from y) = y

227224 ok1 Nothing = Refl

228225 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED

@@ -253,7 +250,7 @@ maybeVoidUnit = (Maybe Void) ={ maybeEither }=

253250 () QED

254251

255252eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))

256−eitherMaybeLeftMaybe {a} {b} =

253+eitherMaybeLeftMaybe =

257254 (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=

258255 (Either (Either a ()) b) ={ eitherAssoc }=

259256 (Either a (Either () b)) ={ eitherCongRight eitherComm }=

@@ -263,7 +260,7 @@ eitherMaybeLeftMaybe {a} {b} =

263260

264261

265262eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))

266−eitherMaybeRightMaybe {a} {b} =

263+eitherMaybeRightMaybe =

267264 (Either a (Maybe b)) ={ eitherComm }=

268265 (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=

269266 (Maybe (Either b a)) ={ maybeCong eitherComm }=

@@ -288,8 +285,8 @@ maybeIsoS = MkIso forth back fb bf

288285 fb (FS x) = Refl

289286

290287finZeroBot : Iso (Fin 0) Void

291−finZeroBot = MkIso (\x => void (uninhabited x))

292− (\x => void x)

288+finZeroBot = MkIso (void . uninhabited)

289+ void

293290 (\x => void x)

294291 (\x => void (uninhabited x))

295292

libs/contrib/Control/Algebra/Laws.idr+128−80

@@ -6,98 +6,146 @@ import Interfaces.Verified

77%access export

9−||| A prof that -0 = 0 in any verified group.

10−inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral

9+||| -(-x) = x in any verified group.

10+inverseSquaredIsIdentity : VerifiedGroup t => (x : t) ->

11+ inverse (inverse x) = x

12+inverseSquaredIsIdentity x =

13+ let

14+ ix = inverse x

15+ iix = inverse ix

16+ in

17+ rewrite sym $ monoidNeutralIsNeutralR iix in

18+ rewrite sym $ groupInverseIsInverseL x in

19+ rewrite sym $ semigroupOpIsAssociative x ix iix in

20+ rewrite groupInverseIsInverseL ix in

21+ monoidNeutralIsNeutralL x

22+

23+||| -0 = 0 in any verified group.

24+inverseNeutralIsNeutral : VerifiedGroup t =>

25+ inverse (the t A.neutral) = A.neutral

1126inverseNeutralIsNeutral {t} =

12− let zero = the t neutral

13− step1 = cong {f = (<+> inverse zero)} (the (zero = zero) Refl)

14− step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1

15− in

16− replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2

27+ let e = the t neutral in

28+ rewrite sym $ cong {f = inverse} (groupInverseIsInverseL e) in

29+ rewrite monoidNeutralIsNeutralR $ inverse e in

30+ inverseSquaredIsIdentity e

1731

18−||| A proof that -(-x) = x in any verified group.

19−inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x

20−inverseSquaredIsIdentity {t} x =

21− let zero = the t neutral

22− step1 = cong {f = (x <+>)} (groupInverseIsInverseL (inverse x))

23− step2 = replace {P = \r => r = x <+> neutral} (semigroupOpIsAssociative x (inverse x) (inverse $ inverse x)) step1

24− step3 = replace {P = \r => r <+> inverse (inverse x) = x <+> neutral} (groupInverseIsInverseL x) step2

25− step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3

26− in

27− replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4

32+||| -(x + y) = -y + -x in any verified group.

33+inverseOfSum : VerifiedGroup t => (l, r : t) ->

34+ inverse (l <+> r) = inverse r <+> inverse l

35+inverseOfSum {t} l r =

36+ let

37+ e = the t neutral

38+ il = inverse l

39+ ir = inverse r

40+ sum = l <+> r

41+ ilr = inverse sum

42+ iril = ir <+> il

43+ ile = il <+> e

44+ in

45+ -- expand

46+ rewrite sym $ monoidNeutralIsNeutralR ilr in

47+ rewrite sym $ groupInverseIsInverseR r in

48+ rewrite sym $ monoidNeutralIsNeutralL ir in

49+ rewrite sym $ groupInverseIsInverseR l in

50+ -- shuffle

51+ rewrite semigroupOpIsAssociative ir il l in

52+ rewrite sym $ semigroupOpIsAssociative iril l r in

53+ rewrite sym $ semigroupOpIsAssociative iril sum ilr in

54+ -- contract

55+ rewrite sym $ monoidNeutralIsNeutralL il in

56+ rewrite groupInverseIsInverseL sum in

57+ rewrite sym $ semigroupOpIsAssociative (ir <+> ile) l ile in

58+ rewrite semigroupOpIsAssociative l il e in

59+ rewrite groupInverseIsInverseL l in

60+ rewrite monoidNeutralIsNeutralL e in

61+ Refl

2862

29−||| A proof that -(x + y) = -x - y in any verified abelian group.

30−inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r

31−inverseDistributesOverGroupOp {t} l r =

32− let step1 = replace {P = \x => x = neutral} (sym $ groupInverseIsInverseL (l <+> r)) $ the (the t neutral = neutral) Refl

33− step2 = cong {f = ((inverse r) <+>) . ((inverse l) <+>)} step1

34− step3 = replace {P = \x => inverse r <+> (inverse l <+> (l <+> r <+> inverse (l <+> r))) = inverse r <+> x} (monoidNeutralIsNeutralL (inverse l)) step2

35− step4 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r) (inverse l) (l <+> r <+> inverse (l <+> r))) step3

36− step5 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse (l <+> r))) step4

37− step6 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) l r) step5

38− step7 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (sym $ semigroupOpIsAssociative (inverse r) (inverse l) l) step6

39− step8 = replace {P = \x => inverse r <+> x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR l) step7

40− step9 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (monoidNeutralIsNeutralL (inverse r)) step8

41− step10 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR r) step9

42− step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10

43− in

44− replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11

63+||| -(x + y) = -x + -y in any verified abelian group.

64+inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) ->

65+ inverse (l <+> r) = inverse l <+> inverse r

66+inverseDistributesOverGroupOp l r =

67+ rewrite abelianGroupOpIsCommutative (inverse l) (inverse r) in

68+ inverseOfSum l r

4569

46−||| A proof that anything multiplied by zero yields zero back.

47−multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral

48−multNeutralAbsorbingL r =

49− let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r)

50− step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1

51− step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2

52− step4 = replace {P = \x => neutral <.> r <+> x = r} (ringWithUnityIsUnityR r) step3

53− step5 = cong {f = \x => x <+> inverse r} step4

54− step6 = replace {P = \x => x = r <+> inverse r} (sym $ semigroupOpIsAssociative (neutral <.> r) r (inverse r)) step5

55− step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6

56− in

57− replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7

70+||| Anything multiplied by zero yields zero back in a verified ring.

71+multNeutralAbsorbingL : VerifiedRing t => (r : t) ->

72+ A.neutral <.> r = A.neutral

73+multNeutralAbsorbingL {t} r =

74+ let

75+ e = the t neutral

76+ ir = inverse r

77+ exr = e <.> r

78+ iexr = inverse exr

79+ in

80+ rewrite sym $ monoidNeutralIsNeutralR exr in

81+ rewrite sym $ groupInverseIsInverseR exr in

82+ rewrite sym $ semigroupOpIsAssociative iexr exr ((iexr <+> exr) <.> r) in

83+ rewrite groupInverseIsInverseR exr in

84+ rewrite sym $ ringOpIsDistributiveR e e r in

85+ rewrite monoidNeutralIsNeutralR e in

86+ groupInverseIsInverseR exr

5887

59−||| A proof that anything multiplied by zero yields zero back.

60−multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral

61−multNeutralAbsorbingR l =

62− let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l)

63− step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1

64− step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2

65− step4 = replace {P = \x => l <.> neutral <+> x = l} (ringWithUnityIsUnityL l) step3

66− step5 = cong {f = \x => x <+> inverse l} step4

67− step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5

68− step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6

69− in

70− replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7

88+||| Anything multiplied by zero yields zero back in a verified ring.

89+multNeutralAbsorbingR : VerifiedRing t => (l : t) ->

90+ l <.> A.neutral = A.neutral

91+multNeutralAbsorbingR {t} l =

92+ let

93+ e = the t neutral

94+ il = inverse l

95+ lxe = l <.> e

96+ ilxe = inverse lxe

97+ in

98+ rewrite sym $ monoidNeutralIsNeutralL lxe in

99+ rewrite sym $ groupInverseIsInverseL lxe in

100+ rewrite semigroupOpIsAssociative (l <.> (lxe <+> ilxe)) lxe ilxe in

101+ rewrite groupInverseIsInverseL lxe in

102+ rewrite sym $ ringOpIsDistributiveL l e e in

103+ rewrite monoidNeutralIsNeutralL e in

104+ groupInverseIsInverseL lxe

71105

72−||| A proof that inverse operator can be extracted before multiplication

106+||| Inverse operator can be extracted before multiplication.

73107||| (-x)y = -(xy)

74−multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)

108+multInverseInversesL : VerifiedRing t => (l, r : t) ->

109+ inverse l <.> r = inverse (l <.> r)

75110multInverseInversesL l r =

76− let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r)

77− step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveR l (inverse l) r) step1

78− step3 = cong {f = ((inverse (l <.> r)) <+>)} step2

79− step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> inverse l <.> r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3

80− step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (inverse l <.> r)) step4

81− step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5

82− in

83− replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6

111+ let

112+ il = inverse l

113+ lxr = l <.> r

114+ ilxr = il <.> r

115+ i_lxr = inverse lxr

116+ in

117+ rewrite sym $ monoidNeutralIsNeutralR ilxr in

118+ rewrite sym $ groupInverseIsInverseR lxr in

119+ rewrite sym $ semigroupOpIsAssociative i_lxr lxr ilxr in

120+ rewrite sym $ ringOpIsDistributiveR l il r in

121+ rewrite groupInverseIsInverseL l in

122+ rewrite multNeutralAbsorbingL r in

123+ monoidNeutralIsNeutralL i_lxr

84124

85−||| A proof that inverse operator can be extracted before multiplication

125+||| Inverse operator can be extracted before multiplication.

86126||| x(-y) = -(xy)

87−multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)

127+multInverseInversesR : VerifiedRing t => (l, r : t) ->

128+ l <.> inverse r = inverse (l <.> r)

88129multInverseInversesR l r =

89− let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l)

90− step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveL l r (inverse r)) step1

91− step3 = cong {f = ((inverse (l <.> r)) <+>)} step2

92− step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> l <.> inverse r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3

93− step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4

94− step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5

95− in

96− replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6

130+ let

131+ ir = inverse r

132+ lxr = l <.> r

133+ lxir = l <.> ir

134+ ilxr = inverse lxr

135+ in

136+ rewrite sym $ monoidNeutralIsNeutralL lxir in

137+ rewrite sym $ groupInverseIsInverseL lxr in

138+ rewrite semigroupOpIsAssociative lxir lxr ilxr in

139+ rewrite sym $ ringOpIsDistributiveL l ir r in

140+ rewrite groupInverseIsInverseR r in

141+ rewrite multNeutralAbsorbingR l in

142+ monoidNeutralIsNeutralR ilxr

97143

98−||| A proof that multiplication of inverses is the same as multiplication of original

99−||| elements. (-x)(-y) = xy

100−multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r

144+||| Multiplication of inverses is the same as multiplication of

145+||| original elements.

146+||| (-x)(-y) = xy

147+multNegativeByNegativeIsPositive : VerifiedRing t => (l, r : t) ->

148+ inverse l <.> inverse r = l <.> r

101149multNegativeByNegativeIsPositive l r =

102150 rewrite multInverseInversesR (inverse l) r in

103151 rewrite sym $ multInverseInversesL (inverse l) r in

libs/contrib/Data/List/Extra.idrdeleted−46

@@ -1,46 +0,0 @@

1−module Data.List.Extra

2−

3−%default total

4−%access export

5−

6−||| The final segment of the accumulator is the final segment of the result.

7−reverseOntoAcc : (xs, ys, zs : List a) ->

8− reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs

9−reverseOntoAcc [] _ _ = Refl

10−reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs

11−

12−||| Serves as a specification for reverseOnto.

13−reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs

14−reverseOntoSpec xs ys = reverseOntoAcc ys [] xs

15−

16−||| The reverse of an empty list is an empty list. Together with reverseCons,

17−||| serves as a specification for reverse.

18−reverseNil : reverse [] = []

19−reverseNil = Refl

20−

21−||| The reverse of a cons is the reverse of the tail followed by the head.

22−||| Together with reverseNil serves as a specification for reverse.

23−reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs ++ [x]

24−reverseCons x xs = reverseOntoSpec [x] xs

25−

26−||| Reversing an append is appending reversals backwards.

27−reverseAppend : (xs, ys : List a) ->

28− reverse (xs ++ ys) = reverse ys ++ reverse xs

29−reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))

30−reverseAppend (x :: xs) ys =

31− rewrite reverseCons x (xs ++ ys) in

32− rewrite reverseAppend xs ys in

33− rewrite reverseCons x xs in

34− sym $ appendAssociative (reverse ys) (reverse xs) [x]

35−

36−||| Reversing a singleton list is a no-op.

37−reverseSingletonId : (x : a) -> reverse [x] = [x]

38−reverseSingletonId _ = Refl

39−

40−||| Reversing a reverse gives the original.

41−reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs

42−reverseReverseId [] = Refl

43−reverseReverseId (x :: xs) =

44− rewrite reverseCons x xs in

45− rewrite reverseAppend (reverse xs) [x] in

46− cong $ reverseReverseId xs

libs/contrib/Data/List/Reverse.idrnew file+99

@@ -0,0 +1,99 @@

1+||| Properties of the reverse function.

2+module Data.List.Reverse

4+%default total

5+%access export

7+||| The final segment of the accumulator is the final segment of the result.

8+reverseOntoAcc : (xs, ys, zs : List a) ->

9+ reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs

10+reverseOntoAcc [] _ _ = Refl

11+reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs

12+

13+||| Serves as a specification for reverseOnto.

14+reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs

15+reverseOntoSpec xs ys = reverseOntoAcc ys [] xs

16+

17+||| The reverse of an empty list is an empty list. Together with reverseCons,

18+||| serves as a specification for reverse.

19+reverseNil : reverse [] = []

20+reverseNil = Refl

21+

22+||| The reverse of a cons is the reverse of the tail followed by the head.

23+||| Together with reverseNil serves as a specification for reverse.

24+reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs ++ [x]

25+reverseCons x xs = reverseOntoSpec [x] xs

26+

27+||| Reversing an append is appending reversals backwards.

28+reverseAppend : (xs, ys : List a) ->

29+ reverse (xs ++ ys) = reverse ys ++ reverse xs

30+reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))

31+reverseAppend (x :: xs) ys =

32+ rewrite reverseCons x (xs ++ ys) in

33+ rewrite reverseAppend xs ys in

34+ rewrite reverseCons x xs in

35+ sym $ appendAssociative (reverse ys) (reverse xs) [x]

36+

37+||| A recursive definition of reverse.

38+reverseRec : List a -> List a

39+reverseRec [] = []

40+reverseRec (x :: xs) = reverseRec xs ++ [x]

41+

42+||| The iterative and recursive defintions of reverse are the same.

43+reverseEquiv : (xs : List a) -> reverseRec xs = reverse xs

44+reverseEquiv [] = Refl

45+reverseEquiv (x :: xs) =

46+ rewrite reverseEquiv xs in

47+ rewrite reverseAppend [x] xs in

48+ Refl

49+

50+||| Reversing a singleton list is a no-op.

51+reverseSingletonId : (x : a) -> reverse [x] = [x]

52+reverseSingletonId _ = Refl

53+

54+||| Reversing a reverse gives the original.

55+reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs

56+reverseReverseId [] = Refl

57+reverseReverseId (x :: xs) =

58+ rewrite reverseCons x xs in

59+ rewrite reverseAppend (reverse xs) [x] in

60+ cong $ reverseReverseId xs

61+

62+||| Reversing onto preserves list length.

63+reverseOntoLength : (xs, acc : List a) ->

64+ length $ reverseOnto acc xs = length acc + length xs

65+reverseOntoLength [] acc = rewrite plusZeroRightNeutral (length acc) in Refl

66+reverseOntoLength (x :: xs) acc =

67+ rewrite reverseOntoLength xs (x :: acc) in

68+ plusSuccRightSucc (length acc) (length xs)

69+

70+||| Reversing preserves list length.

71+reverseLength : (xs : List a) -> length $ reverse xs = length xs

72+reverseLength xs = reverseOntoLength xs []

73+

74+||| Equal reversed lists are equal.

75+reverseEqual : (xs, ys : List a) -> reverse xs = reverse ys -> xs = ys

76+reverseEqual xs ys prf =

77+ rewrite sym $ reverseReverseId xs in

78+ rewrite prf in

79+ reverseReverseId ys

80+

81+||| Do geese see God?

82+data Palindrome : (xs : List a) -> Type where

83+ Empty : Palindrome []

84+ Single : Palindrome [_]

85+ Multi : Palindrome xs -> Palindrome $ [x] ++ xs ++ [x]

86+

87+||| A Palindrome reversed is itself.

88+palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs

89+palindromeReverse [] Empty = Refl

90+palindromeReverse [_] Single = Refl

91+palindromeReverse ([x] ++ ys ++ [x]) (Multi pf) =

92+ rewrite reverseAppend ([x] ++ ys) [x] in

93+ rewrite reverseAppend [x] ys in

94+ rewrite palindromeReverse ys pf in

95+ Refl

96+

97+||| Only Palindromes are equal to their own reverse.

98+postulate -- This is a tough one. Any takers?

99+reversePalindrome : (xs : List a) -> reverse xs = xs -> Palindrome xs

libs/contrib/Data/Nat/Fact.idrnew file+56

@@ -0,0 +1,56 @@

1+||| Properties of factorial functions.

2+module Data.Nat.Fact

4+%access public export

6+%default total

8+||| Recursive definition of factorial.

9+factRec : Nat -> Nat

10+factRec Z = 1

11+factRec (S k) = (S k) * factRec k

12+

13+||| Tail-recursive accumulator for factItr.

14+factAcc : Nat -> Nat -> Nat

15+factAcc Z acc = acc

16+factAcc (S k) acc = factAcc k $ (S k) * acc

17+

18+||| Iterative definition of factorial.

19+factItr : Nat -> Nat

20+factItr n = factAcc n 1

21+

22+----------------------------------------

23+

24+||| Multiplicand-shuffling lemma.

25+multShuffle : (a, b, c : Nat) -> a * (b * c) = b * (a * c)

26+multShuffle a b c =

27+ rewrite multAssociative a b c in

28+ rewrite multCommutative a b in

29+ sym $ multAssociative b a c

30+

31+||| Multiplication of the accumulator.

32+factAccMult : (a, b, c : Nat) ->

33+ a * factAcc b c = factAcc b (a * c)

34+factAccMult _ Z _ = Refl

35+factAccMult a (S k) c =

36+ rewrite factAccMult a k (S k * c) in

37+ rewrite multShuffle a (S k) c in

38+ Refl

39+

40+||| Addition of accumulators.

41+factAccPlus : (a, b, c : Nat) ->

42+ factAcc a b + factAcc a c = factAcc a (b + c)

43+factAccPlus Z _ _ = Refl

44+factAccPlus (S k) b c =

45+ rewrite factAccPlus k (S k * b) (S k * c) in

46+ rewrite sym $ multDistributesOverPlusRight (S k) b c in

47+ Refl

48+

49+||| The recursive and iterative definitions are the equivalent.

50+factRecItr : (n : Nat) -> factRec n = factItr n

51+factRecItr Z = Refl

52+factRecItr (S k) =

53+ rewrite factRecItr k in

54+ rewrite factAccMult k k 1 in

55+ rewrite multOneRightNeutral k in

56+ factAccPlus k 1 k

libs/contrib/Data/Nat/Parity.idr+155−29

@@ -2,18 +2,9 @@ module Data.Nat.Parity

33%access public export

5−--------------------------------------------------------------------------------

6−-- Parity

7−--------------------------------------------------------------------------------

5+----------------------------------------

9−mutual

10− even : Nat -> Bool

11− even Z = True

12− even (S k) = odd k

13−

14− odd : Nat -> Bool

15− odd Z = False

16− odd (S k) = even k

7+-- Type-level, constructive definitions of parity.

178

189||| A nat is Even when it is twice some other nat.

1910Even : Nat -> Type

@@ -23,6 +14,8 @@ Even n = (half : Nat ** n = half * 2)

2314Odd : Nat -> Type

2415Odd n = (haf : Nat ** n = S $ haf * 2)

2516

17+----------------------------------------

18+

2619||| Two more than an Even is Even.

2720add2Even : Even n -> Even (2 + n)

2821add2Even (half ** pf) = (S half ** cong {f = (+) 2} pf)

@@ -52,20 +45,73 @@ succDoublePredPred {k = S _} prf = cong {f = Nat.pred} prf

5245predEvenOdd : Even (S n) -> Odd n

5346predEvenOdd (half ** pf) = (pred half ** succDoublePredPred pf)

5447

48+----------------------------------------

49+

50+-- Boolean definitions of parity.

51+

52+mutual

53+ even : Nat -> Bool

54+ even Z = True

55+ even (S k) = odd k

56+

57+ odd : Nat -> Bool

58+ odd Z = False

59+ odd (S k) = even k

60+

61+----------------------------------------

62+

63+-- The boolean and type-level definitions are equivalent in the sense

64+-- that a proof of one can be gotten from a proof of the other.

65+

66+mutual

67+ ||| Evens are even.

68+ evenEven : Even n -> even n = True

69+ evenEven {n = Z} _ = Refl

70+ evenEven {n = S _} pf = oddOdd $ predEvenOdd pf

71+

72+ ||| Odds are odd.

73+ oddOdd : Odd n -> odd n = True

74+ oddOdd {n = Z} (_ ** pf) = absurd pf

75+ oddOdd {n = S _} pf = evenEven $ predOddEven pf

76+

77+mutual

78+ ||| If it's even, it's Even.

79+ evenEvenConverse : even n = True -> Even n

80+ evenEvenConverse {n = Z} prf = (0 ** Refl)

81+ evenEvenConverse {n = S k} prf =

82+ let (haf ** pf) = oddOddConverse prf in

83+ (S haf ** cong pf)

84+

85+ ||| If it's odd, it's Odd

86+ oddOddConverse : odd n = True -> Odd n

87+ oddOddConverse {n = Z} prf = absurd prf

88+ oddOddConverse {n = S k} prf =

89+ let (half ** pf) = evenEvenConverse prf in

90+ (half ** cong pf)

91+

92+----------------------------------------

93+

94+||| Every nat is either even or odd.

95+evenorodd : (n : Nat) -> Either (even n = True) (odd n = True)

96+evenorodd Z = Left Refl

97+evenorodd (S k) = case evenorodd k of

98+ Left l => Right l

99+ Right r => Left r

100+

55101||| Every nat is either Even or Odd.

56102evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)

57−evenOrOdd Z = Left (0 ** Refl)

58−evenOrOdd (S k) = case evenOrOdd k of

59− Left (half ** pf) => Right (half ** cong {f = S} pf)

60− Right (haf ** pf) => Left (S haf ** cong {f = S} pf)

103+evenOrOdd n = case evenorodd n of

104+ Left e => Left $ evenEvenConverse e

105+ Right o => Right $ oddOddConverse o

106+

107+||| No nat is both even and odd.

108+notevenandodd : even n = True -> odd n = True -> Void

109+notevenandodd {n = Z} en on = absurd on

110+notevenandodd {n = S _} en on = notevenandodd on en

61111

62112||| No nat is both Even and Odd.

63113notEvenAndOdd : Even n -> Odd n -> Void

64−notEvenAndOdd {n = Z} _ (_ ** odd) = absurd odd

65−notEvenAndOdd {n = (S k)} (half ** even) (haf ** odd) =

66− notEvenAndOdd {n = k}

67− (haf ** cong {f = Nat.pred} odd)

68− (pred half ** succDoublePredPred even)

114+notEvenAndOdd en on = notevenandodd (evenEven en) (oddOdd on)

69115

70116||| Evenness is decidable.

71117evenDec : (n : Nat) -> Dec $ Even n

@@ -79,13 +125,93 @@ oddDec n = case evenOrOdd n of

79125 Left even => No $ notEvenAndOdd even

80126 Right odd => Yes odd

81127

82−mutual

83− ||| Evens are even.

84− evenEven : Even n -> even n = True

85− evenEven {n = Z} _ = Refl

86− evenEven {n = S _} pf = oddOdd $ predEvenOdd pf

128+----------------------------------------

129+

130+||| An Odd is the successor of an Even.

131+oddSuccEven : Odd n -> (m : Nat ** (n = S m, Even m))

132+oddSuccEven (haf ** pf) = (haf * 2 ** (pf, (haf ** Refl)))

133+

134+||| Even plus Even is Even.

135+evenPlusEven : Even j -> Even k -> Even (j + k)

136+evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =

137+ (half_j + half_k **

138+ rewrite pf_j in

139+ rewrite pf_k in

140+ sym $ multDistributesOverPlusLeft half_j half_k 2)

141+

142+||| Odd plus Even is Odd.

143+oddPlusEven : Odd j -> Even k -> Odd (j + k)

144+oddPlusEven oj ek =

145+ let

146+ (i ** (ipj, ei)) = oddSuccEven oj

147+ (half_ik ** eik) = evenPlusEven ei ek

148+ in

149+ (half_ik **

150+ rewrite ipj in

151+ cong {f = S} eik)

152+

153+||| Even plus Odd is Odd.

154+evenPlusOdd : Even j -> Odd k -> Odd (j + k)

155+evenPlusOdd {j} {k} ej ok = rewrite plusCommutative j k in oddPlusEven ok ej

156+

157+||| Odd plus Odd is Even.

158+oddPlusOdd : Odd j -> Odd k -> Even (j + k)

159+oddPlusOdd oj ok =

160+ let

161+ (i ** (ipj, ei)) = oddSuccEven oj

162+ (haf_ik ** oik) = evenPlusOdd ei ok

163+ in

164+ (S haf_ik **

165+ rewrite ipj in

166+ rewrite oik in

167+ Refl)

87168

88− ||| Odds are odd.

89− oddOdd : Odd n -> odd n = True

90− oddOdd {n = Z} (_ ** pf) = absurd pf

91− oddOdd {n = S _} pf = evenEven $ predOddEven pf

169+||| A helper fact.

170+multShuffle : (a, b, c : Nat) ->

171+ (a * c) * (b * c) = ((a * b) * c) * c

172+multShuffle a b c =

173+ rewrite multAssociative (a * c) b c in

174+ rewrite multCommutative (a * c) b in

175+ rewrite multAssociative b a c in

176+ rewrite multCommutative b a in

177+ Refl

178+

179+||| Even times Even is Even.

180+evenMultEven : Even j -> Even k -> Even (j * k)

181+evenMultEven (half_j ** pf_j) (half_k ** pf_k) =

182+ (half_j * half_k * 2 **

183+ rewrite pf_j in

184+ rewrite pf_k in

185+ multShuffle half_j half_k 2)

186+

187+||| Odd times Even is Even.

188+oddMultEven : Odd j -> Even k -> Even (j * k)

189+oddMultEven oj (half_k ** pf_k) =

190+ let

191+ (i ** (ipj, ei)) = oddSuccEven oj

192+ (half_ik ** oik) = evenMultEven ei (half_k ** pf_k)

193+ in

194+ (half_k + half_ik **

195+ rewrite multDistributesOverPlusLeft half_k half_ik 2 in

196+ rewrite ipj in

197+ rewrite oik in

198+ rewrite pf_k in

199+ Refl)

200+

201+||| Even times Odd is Even.

202+evenMultOdd : Even j -> Odd k -> Even (j * k)

203+evenMultOdd {j} {k} ej ok = rewrite multCommutative j k in oddMultEven ok ej

204+

205+||| Odd times Odd is Odd.

206+oddMultOdd : Odd j -> Odd k -> Odd (j * k)

207+oddMultOdd oj (haf_k ** pf_k) =

208+ let

209+ (i ** (ipj, ei)) = oddSuccEven oj

210+ (half_ik ** eik) = evenMultOdd ei (haf_k ** pf_k)

211+ in

212+ (haf_k + half_ik **

213+ rewrite multDistributesOverPlusLeft haf_k half_ik 2 in

214+ rewrite ipj in

215+ rewrite eik in

216+ rewrite pf_k in

217+ Refl)

libs/contrib/contrib.ipkg+1−1

@@ -43,7 +43,7 @@ modules = CFFI

4343 , Data.Heap

4444 , Data.IOArray

4545 , Data.List.Zipper

46− , Data.List.Extra

46+ , Data.List.Reverse

4747

4848 , Data.Matrix

4949 , Data.Matrix.Algebraic

libs/prelude/Prelude/File.idr+3−2

@@ -150,7 +150,8 @@ do_getFileAccessTime h =

150150private

151151do_getFileModifiedTime : Ptr -> IO Integer

152152do_getFileModifiedTime h =

153− do MkRaw i <- foreign FFI_C "fileModifiedTime" (Ptr -> IO (Raw Integer)) h

153+ do vm <- getMyVM

154+ MkRaw i <- foreign FFI_C "fileModifiedTime" (Ptr -> Ptr -> IO (Raw Integer)) vm h

154155 pure i

155156

156157private

@@ -175,7 +176,7 @@ export

175176fileModifiedTime : File -> IO (Either FileError Integer)

176177fileModifiedTime (FHandle h)

177178 = do s <- do_getFileModifiedTime h

178− if (s < 0)

179+ if (s == -1)

179180 then Left <$> getFileError

180181 else pure (Right s)

181182

libs/prelude/Prelude/Nat.idr+32−61

@@ -512,19 +512,18 @@ plusLeftCancel (S left) right right' p =

512512

513513total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->

514514 (p : left + right = left' + right) -> left = left'

515−plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in

516− rewrite sym (plusZeroRightNeutral left') in

517− p

518−plusRightCancel left left' (S right) p =

519− plusRightCancel left left' right

520− (succInjective _ _ (rewrite plusSuccRightSucc left right in

521− rewrite plusSuccRightSucc left' right in p))

515+plusRightCancel left left' right p =

516+ plusLeftCancel right left left' $

517+ rewrite plusCommutative right left in

518+ rewrite plusCommutative right left' in

519+ p

522520

523521total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->

524522 (p : left + right = left) -> right = Z

525−plusLeftLeftRightZero Z right p = p

526−plusLeftLeftRightZero (S left) right p =

527− plusLeftLeftRightZero left right (succInjective _ _ p)

523+plusLeftLeftRightZero left right p =

524+ plusLeftCancel left right Z $

525+ rewrite plusZeroRightNeutral left in

526+ p

528527

529528-- Mult

530529total multZeroLeftZero : (right : Nat) -> Z * right = Z

@@ -558,27 +557,21 @@ multCommutative (S left) right =

558557 rewrite multRightSuccPlus right left in

559558 Refl

560559

561−total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

562− left * (centre + right) = (left * centre) + (left * right)

563−multDistributesOverPlusRight Z centre right = Refl

564−multDistributesOverPlusRight (S left) centre right =

565− let inductiveHypothesis = multDistributesOverPlusRight left centre right in

566− rewrite inductiveHypothesis in

567− rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in

568− rewrite sym (plusAssociative centre (mult left centre) right) in

569− rewrite plusCommutative (mult left centre) right in

570− rewrite plusAssociative centre right (mult left centre) in

571− rewrite plusAssociative (plus centre right) (mult left centre) (mult left right) in

572− Refl

573−

574560total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

575561 (left + centre) * right = (left * right) + (centre * right)

576−multDistributesOverPlusLeft Z centre right = Refl

577−multDistributesOverPlusLeft (S left) centre right =

578− let inductiveHypothesis = multDistributesOverPlusLeft left centre right in

579− rewrite inductiveHypothesis in

580− rewrite plusAssociative right (mult left right) (mult centre right) in

581− Refl

562+multDistributesOverPlusLeft Z centre right = Refl

563+multDistributesOverPlusLeft (S k) centre right =

564+ rewrite multDistributesOverPlusLeft k centre right in

565+ rewrite plusAssociative right (k * right) (centre * right) in

566+ Refl

567+

568+total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

569+ left * (centre + right) = (left * centre) + (left * right)

570+multDistributesOverPlusRight left centre right =

571+ rewrite multCommutative left (centre + right) in

572+ rewrite multCommutative left centre in

573+ rewrite multCommutative left right in

574+ multDistributesOverPlusLeft centre right left

582575

583576total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

584577 left * (centre * right) = (left * centre) * right

@@ -590,18 +583,10 @@ multAssociative (S left) centre right =

590583 Refl

591584

592585total multOneLeftNeutral : (right : Nat) -> 1 * right = right

593−multOneLeftNeutral Z = Refl

594−multOneLeftNeutral (S right) =

595− let inductiveHypothesis = multOneLeftNeutral right in

596− rewrite inductiveHypothesis in

597− Refl

586+multOneLeftNeutral right = plusZeroRightNeutral right

598587

599588total multOneRightNeutral : (left : Nat) -> left * 1 = left

600−multOneRightNeutral Z = Refl

601−multOneRightNeutral (S left) =

602− let inductiveHypothesis = multOneRightNeutral left in

603− rewrite inductiveHypothesis in

604− Refl

589+multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left

605590

606591-- Minus

607592total minusSuccSucc : (left : Nat) -> (right : Nat) ->

@@ -689,10 +674,7 @@ total powerZeroOne : (base : Nat) -> power base 0 = S Z

689674powerZeroOne base = Refl

690675

691676total powerOneNeutral : (base : Nat) -> power base 1 = base

692−powerOneNeutral Z = Refl

693−powerOneNeutral (S base) =

694− let inductiveHypothesis = powerOneNeutral base in

695− rewrite inductiveHypothesis in Refl

677+powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base

696678

697679total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z

698680powerOneSuccOne Z = Refl

@@ -701,8 +683,7 @@ powerOneSuccOne (S exp) =

701683 rewrite inductiveHypothesis in Refl

702684

703685total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base

704−powerSuccSuccMult Z = Refl

705−powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl

686+powerSuccSuccMult base = rewrite multOneRightNeutral base in Refl

706687

707688total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->

708689 power (power base exp) exp' = power base (exp * exp')

@@ -796,34 +777,24 @@ minimumIdempotent Z = Refl

796777minimumIdempotent (S k) = cong (minimumIdempotent k)

797778

798779total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z

799−minimumZeroZeroRight Z = Refl

800−minimumZeroZeroRight (S right) = minimumZeroZeroRight right

780+minimumZeroZeroRight right = Refl

801781

802782total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z

803−minimumZeroZeroLeft Z = Refl

804−minimumZeroZeroLeft (S left) = Refl

783+minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl

805784

806785total minimumSuccSucc : (left : Nat) -> (right : Nat) ->

807786 minimum (S left) (S right) = S (minimum left right)

808−minimumSuccSucc Z Z = Refl

809−minimumSuccSucc (S left) Z = Refl

810−minimumSuccSucc Z (S right) = Refl

811−minimumSuccSucc (S left) (S right) = Refl

787+minimumSuccSucc left right = Refl

812788

813789total maximumZeroNRight : (right : Nat) -> maximum Z right = right

814−maximumZeroNRight Z = Refl

815−maximumZeroNRight (S right) = Refl

790+maximumZeroNRight right = Refl

816791

817792total maximumZeroNLeft : (left : Nat) -> maximum left Z = left

818−maximumZeroNLeft Z = Refl

819−maximumZeroNLeft (S left) = Refl

793+maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl

820794

821795total maximumSuccSucc : (left : Nat) -> (right : Nat) ->

822796 S (maximum left right) = maximum (S left) (S right)

823−maximumSuccSucc Z Z = Refl

824−maximumSuccSucc (S left) Z = Refl

825−maximumSuccSucc Z (S right) = Refl

826−maximumSuccSucc (S left) (S right) = Refl

797+maximumSuccSucc left right = Refl

827798

828799total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)

829800sucMaxL Z = Refl

rts/idris_bitstring.c−2

@@ -1,5 +1,3 @@

1−#include <assert.h>

2−

31#include "idris_rts.h"

53VAL idris_b8const(VM *vm, uint8_t a) {

rts/idris_rts.c−10

@@ -1158,16 +1158,6 @@ void idris_disableBuffering(void) {

11581158 setvbuf(stdout, NULL, _IONBF, 0);

11591159}

11601160

1161−#ifndef SEL4

1162−int idris_usleep(int usec) {

1163− struct timespec t;

1164− t.tv_sec = usec / 1000000;

1165− t.tv_nsec = (usec % 1000000) * 1000;

1166−

1167− return nanosleep(&t, NULL);

1168−}

1169−#endif // SEL4

1170−

11711161void stackOverflow(void) {

11721162 fprintf(stderr, "Stack overflow");

11731163 exit(-1);

rts/idris_rts.h−4

@@ -507,10 +507,6 @@ const char *idris_getArg(int i);

507507// disable stdin/stdout buffering

508508void idris_disableBuffering(void);

509509

510−#ifndef SEL4

511−int idris_usleep(int usec);

512−#endif // SEL4

513−

514510// Handle stack overflow.

515511// Just reports an error and exits.

516512

rts/idris_stdfgn.c+12−2

@@ -74,13 +74,13 @@ VAL fileAccessTime(void* h) {

7474 }

7575}

7676

77−VAL fileModifiedTime(void* h) {

77+VAL fileModifiedTime(VM* vm, void* h) {

7878 FILE* f = (FILE*)h;

7979 int fd = fileno(f);

8080

8181 struct stat buf;

8282 if (fstat(fd, &buf) == 0) {

83− return MKBIGI(buf.st_mtime);

83+ return MKBIGUI(vm, buf.st_mtime);

8484 } else {

8585 return MKBIGI(-1);

8686 }

@@ -228,6 +228,16 @@ VAL idris_clock(VM* vm) {

228228 return result;

229229}

230230

231+#ifndef SEL4

232+int idris_usleep(int usec) {

233+ struct timespec t;

234+ t.tv_sec = usec / 1000000;

235+ t.tv_nsec = (usec % 1000000) * 1000;

236+

237+ return nanosleep(&t, NULL);

238+}

239+#endif // SEL4

240+

231241VAL idris_mkFileError(VM* vm) {

232242 VAL result;

233243 switch(errno) {

rts/idris_stdfgn.h+4−1

@@ -18,7 +18,7 @@ int fileSize(void* h);

1818

1919// Return a negative number if not a file (e.g. directory or device)

2020VAL fileAccessTime(void* h);

21−VAL fileModifiedTime(void* h);

21+VAL fileModifiedTime(VM* vm, void* h);

2222VAL fileStatusTime(void* h);

2323

2424void* idris_dirOpen(char* dname);

@@ -54,6 +54,9 @@ char* getEnvPair(int i);

5454

5555VAL idris_time();

5656VAL idris_clock(VM* vm);

57+#ifndef SEL4

58+int idris_usleep(int usec);

59+#endif // SEL4

5760

5861void idris_forceGC();

5962

rts/idris_utf8.c−1

@@ -1,5 +1,4 @@

11#include "idris_utf8.h"

2−#include <stdio.h>

32#include <string.h>

43#include <stdlib.h>

src/Idris/CmdOptions.hs+3−2

@@ -18,6 +18,7 @@ import Idris.Info (getIdrisVersion)

1818import Idris.Options

1919import IRTS.CodegenCommon

2020

21+import qualified Control.Monad.Fail as Fail

2122import Control.Monad.Trans (lift)

2223import Control.Monad.Trans.Except (throwE)

2324import Control.Monad.Trans.Reader (ask)

@@ -264,7 +265,7 @@ parseCodegen :: String -> Codegen

264265parseCodegen "bytecode" = Bytecode

265266parseCodegen cg = Via IBCFormat (map toLower cg)

266267

267−parseLogCats :: Monad m => String -> m [LogCat]

268+parseLogCats :: Fail.MonadFail m => String -> m [LogCat]

268269parseLogCats s =

269270 case lastMay (readP_to_S doParse s) of

270271 Just (xs, _) -> return xs

@@ -290,7 +291,7 @@ parseLogCats s =

290291 s <- look

291292 fail $ "Category: " ++ s ++ " is not recognised."

292293

293−parseConsoleWidth :: Monad m => String -> m ConsoleWidth

294+parseConsoleWidth :: Fail.MonadFail m => String -> m ConsoleWidth

294295parseConsoleWidth "auto" = return AutomaticWidth

295296parseConsoleWidth "infinite" = return InfinitelyWide

296297parseConsoleWidth s =

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

@@ -627,7 +627,7 @@ groupCons cs = gc [] cs

627627 PConst cval -> return $ addConG cval (ps, res) acc

628628 PSuc n -> return $ addg False CSuc [n] (ps, res) acc

629629 PReflected fn args -> return $ addg False (CFn fn) args (ps, res) acc

630− pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"

630+ pat -> error $ show pat ++ " is not a constructor or constant (can't happen)"

631631

632632 addg uniq c conargs res []

633633 = [ConGroup uniq c [(conargs, res)]]

src/Idris/Core/TT.hs+6

@@ -70,6 +70,7 @@ import qualified Prelude as S (Semigroup(..))

7070import Control.Applicative (Alternative, Applicative(..))

7171import qualified Control.Applicative as A (Alternative(..))

7272import Control.DeepSeq (($!!))

73+import qualified Control.Monad.Fail as Fail

7374import Control.Monad.State.Strict

7475import Data.Binary hiding (get, put)

7576import Data.Char

@@ -324,6 +325,11 @@ bindTC x k = case x of

324325instance Monad TC where

325326 return x = OK x

326327 x >>= k = bindTC x k

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

329+ fail = Fail.fail

330+#endif

331+

332+instance Fail.MonadFail TC where

327333 fail e = Error (InternalMsg e)

328334

329335instance MonadPlus TC where

src/Idris/Parser/Stack.hs+16−2

@@ -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(..)

@@ -36,6 +36,7 @@ import Idris.Core.TT (FC(..))

3636import Idris.Output (Message(..))

3737

3838import Control.Arrow (app)

39+import qualified Control.Monad.Fail as Fail

3940import Control.Monad.State.Strict (StateT(..), evalStateT)

4041import Control.Monad.Writer.Strict (MonadWriter(..), WriterT(..), listen,

4142 runWriterT, tell)

@@ -51,7 +52,7 @@ import qualified Util.Pretty as PP

5152type Parser s = StateT s (WriterT FC (P.Parsec Void String))

5253

5354-- | A constraint for parsing without state

54−type Parsing m = (P.MonadParsec Void String m, MonadWriter FC m)

55+type Parsing m = (Fail.MonadFail m, P.MonadParsec Void String m, MonadWriter FC m)

5556

5657-- | Run the Idris parser stack

5758runparser :: Parser st res -> st -> String -> String -> Either ParseError res

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

7677instance Message ParseError where

7778 messageExtent err = sourcePositionFC pos

7879 where

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

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

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

83+#else

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

85+#endif

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

8187 messageSource err = Just sline

8288 where

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

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

91+#else

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

93+#endif

8494

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

8696prettyError :: ParseError -> String

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

8898

8999{- * Mark and restore -}

90100

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

102+type Mark = P.State String Void

103+#else

91104type Mark = P.State String

105+#endif

92106

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

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

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

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

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

4+extra-deps:

5+- cheapskate-0.1.1.2

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

4+extra-deps:

5+- cheapskate-0.1.1.2

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−24

@@ -1,24 +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−

14−flags:

15− idris:

16− FFI: true

17− GMP: true

18−

19−ghc-options:

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

21−

22−nix:

23− enable: false

24− shell-file: stack-shell.nix

@@ -0,0 +1 @@

1+stack-15.4.yaml

test/README.md+5−5

@@ -113,18 +113,18 @@ and somewhat self-explanatory.

113113

1141141. Choose the family your test shall belong to and remember its identifier.

1151152. Pick the next available integer in the test family. It will be the index.

116−3. Say the family's identifier is `foo` and the index is `42`. You should call `./mktest.pl foo042` ; this will create the directory and a simple `run` script.

116+3. Say the family's identifier is `foo` and the index is `42`. You should call `./mktest.pl foo042` ; this will create the directory and a simple `run.sh` script.

1171174. Modify the `run` script to your liking. If you want to call the idris executable, write `${IDRIS:-idris} $@`.

1181185. Add any file you may need in the directory. If they don't end in `.idr`, you should remember them for the next step.

1191196. Add your test in `TestData.hs`. Each family has a list of `(Index, CompatCodegen)`. See the next section for the available values in `CompatCodegen`. In most cases, you should write `( 42, ANY)`.

120−7. Generate the `expected` file by doing:

120+7. Generate the `expected.out` file by doing:

121121 ```

122122 # Using cabal

123123 cabal test --test-options="--pattern foo042 --accept"

124124 # Using stack

125125 stack test --test-arguments="--pattern foo042 --accept"

126126 ```

127−8. Check the content of `expected`. Maybe the test didn't do what you thought it would. Fix and go back to 7 until it's ok.

127+8. Check the content of `expected.out`. Maybe the test didn't do what you thought it would. Fix and go back to 7 until it's ok.

128128

129129### Specifying compatible backends

130130

@@ -146,7 +146,7 @@ Currently, `NONE` has the same effect as `ANY`, but this will change.

146146

147147### Updating golden files

148148

149−To update the `expected` file for every test, do one of the following:

149+To update the `expected.out` file for every test, do one of the following:

150150

151151```

152152# Using make

@@ -157,4 +157,4 @@ cabal test --test-options="--accept"

157157stack test --test-arguments="--accept"

158158```

159159

160−"Accepted" tests are the ones that update the golden file. A test can still fail if the `run` script itself crashes.

160+"Accepted" tests are the ones that update the golden file. A test can still fail if the `run.sh` script itself crashes.

test/TestRun.hs+2−2

@@ -62,7 +62,7 @@ ingredients = defaultIngredients ++

6262test :: String -> String -> IO () -> TestTree

6363test testName path = goldenVsFileDiff testName diff ref output

6464 where

65− ref = path </> "expected"

65+ ref = path </> "expected.out"

6666 output = path </> "output"

6767 diff ref new | os == "openbsd" = ["diff", "-u", new, ref]

6868 | otherwise = ["diff", "--strip-trailing-cr", "-u", new, ref]

@@ -92,7 +92,7 @@ mkGoldenTests testFamilies flags =

9292-- this thing.

9393runTest :: String -> Flags -> IO ()

9494runTest path flags = do

95− let run = (proc "bash" ("run" : flags)) {cwd = Just path}

95+ let run = (proc "bash" ("run.sh" : flags)) {cwd = Just path}

9696 (_, output, error_out) <- readCreateProcessWithExitCode run ""

9797 writeFile (path </> "output") (normalise output)

9898 when (error_out /= "") $ hPutStrLn stderr ("\nError: " ++ path ++ "\n" ++ error_out)

test/base001/expected → test/base001/expected.outrenamed

The content is the same.

test/base001/run → test/base001/run.shrenamed+1−1

@@ -3,7 +3,7 @@

33set -u

55if [[ ${OSTYPE} = 'msys' ]]; then

6− cat expected # skip this test on Windows

6+ cat expected.out # skip this test on Windows

77else

88 ${IDRIS:-idris} "$@" --build base001.ipkg | grep -v 'make.*:'

99 ./base001 2>&1 | grep -v '^sh:.*\./does-not-exist:'

test/basic001/expected → test/basic001/expected.outrenamed

The content is the same.

test/basic001/run → test/basic001/run.shrenamed

Only the mode changed.

test/basic002/expected → test/basic002/expected.outrenamed

The content is the same.

test/basic002/run → test/basic002/run.shrenamed

Only the mode changed.

test/basic003/expected → test/basic003/expected.outrenamed

The content is the same.

test/basic003/run → test/basic003/run.shrenamed

Only the mode changed.

test/basic004/expected → test/basic004/expected.outrenamed

The content is the same.

test/basic004/run → test/basic004/run.shrenamed

Only the mode changed.

test/basic005/expected → test/basic005/expected.outrenamed

The content is the same.

test/basic005/run → test/basic005/run.shrenamed

Only the mode changed.

test/basic006/expected → test/basic006/expected.outrenamed

The content is the same.

test/basic006/run → test/basic006/run.shrenamed

Only the mode changed.

test/basic007/expected → test/basic007/expected.outrenamed

The content is the same.

test/basic007/run → test/basic007/run.shrenamed

Only the mode changed.

test/basic008/expected → test/basic008/expected.outrenamed

The content is the same.

test/basic008/run → test/basic008/run.shrenamed

Only the mode changed.

test/basic009/expected → test/basic009/expected.outrenamed

The content is the same.

test/basic009/run → test/basic009/run.shrenamed

Only the mode changed.

test/basic010/expected → test/basic010/expected.outrenamed

The content is the same.

test/basic010/run → test/basic010/run.shrenamed

Only the mode changed.

test/basic011/expected → test/basic011/expected.outrenamed

The content is the same.

test/basic011/run → test/basic011/run.shrenamed

Only the mode changed.

test/basic012/expected → test/basic012/expected.outrenamed

The content is the same.

test/basic012/run → test/basic012/run.shrenamed

Only the mode changed.

test/basic013/expected → test/basic013/expected.outrenamed

The content is the same.

test/basic013/run → test/basic013/run.shrenamed

Only the mode changed.

test/basic014/expected → test/basic014/expected.outrenamed

The content is the same.

test/basic014/run → test/basic014/run.shrenamed

Only the mode changed.

test/basic015/expected → test/basic015/expected.outrenamed

The content is the same.

test/basic015/run → test/basic015/run.shrenamed

Only the mode changed.

test/basic016/expected → test/basic016/expected.outrenamed

The content is the same.

test/basic016/run → test/basic016/run.shrenamed

Only the mode changed.

test/basic017/expected → test/basic017/expected.outrenamed

The content is the same.

test/basic017/run → test/basic017/run.shrenamed

Only the mode changed.

test/basic018/expected → test/basic018/expected.outrenamed

The content is the same.

test/basic018/run → test/basic018/run.shrenamed

Only the mode changed.

test/basic019/expected → test/basic019/expected.outrenamed

The content is the same.

test/basic019/run → test/basic019/run.shrenamed

Only the mode changed.

test/basic020/expected → test/basic020/expected.outrenamed

The content is the same.

test/basic020/run → test/basic020/run.shrenamed

Only the mode changed.

test/basic021/expected → test/basic021/expected.outrenamed

The content is the same.

test/basic021/run → test/basic021/run.shrenamed

Only the mode changed.

test/basic022/expected → test/basic022/expected.outrenamed

The content is the same.

test/basic022/run → test/basic022/run.shrenamed

Only the mode changed.

test/basic023/expected → test/basic023/expected.outrenamed

The content is the same.

test/basic023/run → test/basic023/run.shrenamed

Only the mode changed.

test/basic024/expected → test/basic024/expected.outrenamed

The content is the same.

test/basic024/input → test/basic024/input.inrenamed

The content is the same.

test/basic024/run → test/basic024/run.shrenamed+1−1

@@ -1,6 +1,6 @@

11#!/usr/bin/env bash

3−${IDRIS:-idris} $@ --quiet --port none < input

3+${IDRIS:-idris} $@ --quiet --port none < input.in

44${IDRIS:-idris} $@ basic024.idr -o basic024

66./basic024

test/basic025/expected → test/basic025/expected.outrenamed

The content is the same.

test/basic025/input → test/basic025/input.inrenamed

The content is the same.

test/basic025/run → test/basic025/run.shrenamed+2−2

@@ -1,7 +1,7 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none < input

2+${IDRIS:-idris} $@ --quiet --port none < input.in

33${IDRIS:-idris} $@ -o basic025 basic025.idr

5−./basic025 input

5+./basic025 input.in

77rm -f basic025 *.ibc

test/basic026/expected → test/basic026/expected.outrenamed

The content is the same.

test/basic026/run → test/basic026/run.shrenamed

The content is the same.

test/bignum001/expected → test/bignum001/expected.outrenamed

The content is the same.

test/bignum001/run → test/bignum001/run.shrenamed

Only the mode changed.

test/bignum002/expected → test/bignum002/expected.outrenamed

The content is the same.

test/bignum002/run → test/bignum002/run.shrenamed

Only the mode changed.

test/bignum003/expected → test/bignum003/expected.outrenamed

The content is the same.

test/bignum003/run → test/bignum003/run.shrenamed

Only the mode changed.

test/bounded001/expected → test/bounded001/expected.outrenamed

The content is the same.

test/bounded001/run → test/bounded001/run.shrenamed

Only the mode changed.

test/buffer001/expected → test/buffer001/expected.outrenamed

The content is the same.

test/buffer001/run → test/buffer001/run.shrenamed

Only the mode changed.

test/buffer002/expected → test/buffer002/expected.outrenamed

The content is the same.

test/buffer002/run → test/buffer002/run.shrenamed

Only the mode changed.

test/contrib001/expected → test/contrib001/expected.outrenamed

The content is the same.

test/contrib001/run → test/contrib001/run.shrenamed

Only the mode changed.

test/corecords001/expected → test/corecords001/expected.outrenamed

The content is the same.

test/corecords001/run → test/corecords001/run.shrenamed

Only the mode changed.

test/corecords002/expected → test/corecords002/expected.outrenamed

The content is the same.

test/corecords002/run → test/corecords002/run.shrenamed

Only the mode changed.

test/delab001/expected → test/delab001/expected.outrenamed

The content is the same.

test/delab001/input → test/delab001/input.inrenamed

The content is the same.

test/delab001/run → test/delab001/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor delab001.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor delab001.idr < input.in

33rm -f *.ibc

test/directives001/expected → test/directives001/expected.outrenamed

The content is the same.

test/directives001/run → test/directives001/run.shrenamed

Only the mode changed.

test/directives002/expected → test/directives002/expected.outrenamed

The content is the same.

test/directives002/run → test/directives002/run.shrenamed

The content is the same.

test/directives003/expected → test/directives003/expected.outrenamed

The content is the same.

test/directives003/run → test/directives003/run.shrenamed

Only the mode changed.

test/disambig002/expected → test/disambig002/expected.outrenamed

The content is the same.

test/disambig002/run → test/disambig002/run.shrenamed

Only the mode changed.

test/docs001/expected → test/docs001/expected.outrenamed

The content is the same.

test/docs001/input → test/docs001/input.inrenamed

The content is the same.

test/docs001/run → test/docs001/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs001.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs001.idr < input.in

33rm *.ibc

test/docs002/expected → test/docs002/expected.outrenamed

The content is the same.

test/docs002/input → test/docs002/input.inrenamed

The content is the same.

test/docs002/run → test/docs002/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nobanner --nocolor --quiet --port none docs002.idr < input

2+${IDRIS:-idris} $@ --nobanner --nocolor --quiet --port none docs002.idr < input.in

33rm *.ibc

test/docs003/expected → test/docs003/expected.outrenamed

The content is the same.

test/docs003/input → test/docs003/input.inrenamed

The content is the same.

test/docs003/run → test/docs003/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs003.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs003.idr < input.in

33rm *.ibc

test/docs004/expected → test/docs004/expected.outrenamed

The content is the same.

test/docs004/input → test/docs004/input.inrenamed

The content is the same.

test/docs004/run → test/docs004/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs004.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs004.idr < input.in

33rm *.ibc

test/docs005/expected → test/docs005/expected.outrenamed

The content is the same.

test/docs005/input → test/docs005/input.inrenamed

The content is the same.

test/docs005/run → test/docs005/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs005.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs005.idr < input.in

33rm *.ibc

test/docs006/expected → test/docs006/expected.outrenamed

The content is the same.

test/docs006/input → test/docs006/input.inrenamed

The content is the same.

test/docs006/run → test/docs006/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs006.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs006.idr < input.in

33rm *.ibc

test/dsl001/expected → test/dsl001/expected.outrenamed

The content is the same.

test/dsl001/input → test/dsl001/input.inrenamed

The content is the same.

test/dsl001/run → test/dsl001/run.shrenamed+1−1

@@ -1,5 +1,5 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ test001.idr -o test001 --partial-eval

33./test001

4−${IDRIS:-idris} $@ test001.idr --partial-eval --quiet --port none < input

4+${IDRIS:-idris} $@ test001.idr --partial-eval --quiet --port none < input.in

55rm -f test001 test001.ibc

test/dsl002/expected → test/dsl002/expected.outrenamed

The content is the same.

test/dsl002/run → test/dsl002/run.shrenamed

Only the mode changed.

test/dsl002/test → test/dsl002/test.inrenamed

The content is the same.

test/dsl002/test014.idr+1−1

@@ -64,6 +64,6 @@ readH fn = res (do let x = open fn Reading

6464 else rputStrLn "Error")

6565

6666main : IO ()

67−main = run (readH "test")

67+main = run (readH "test.in")

6868

6969

test/dsl003/expected → test/dsl003/expected.outrenamed

The content is the same.

test/dsl003/run → test/dsl003/run.shrenamed

Only the mode changed.

test/dsl004/expected → test/dsl004/expected.outrenamed

The content is the same.

test/dsl004/run → test/dsl004/run.shrenamed

Only the mode changed.

test/effects001/expected → test/effects001/expected.outrenamed

The content is the same.

test/effects001/run → test/effects001/run.shrenamed

Only the mode changed.

test/effects001/test021.idr+1−1

@@ -31,7 +31,7 @@ readFileCount = readAcc []

3131

3232testFile : TestFileIO () ()

3333testFile = do

34− Success <- open "testFile" Read

34+ Success <- open "testFile.in" Read

3535 | (FError err) => do

3636 putStrLn "Error!"

3737 pure ()

test/effects001/testFile → test/effects001/testFile.inrenamed

The content is the same.

test/effects002/expected → test/effects002/expected.outrenamed

The content is the same.

test/effects002/run → test/effects002/run.shrenamed

Only the mode changed.

test/effects003/expected → test/effects003/expected.outrenamed

The content is the same.

test/effects003/input → test/effects003/input.inrenamed

The content is the same.

test/effects003/run → test/effects003/run.shrenamed+1−1

@@ -1,4 +1,4 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ hangman.idr --nocolour -p effects -o hangman

3−./hangman < input

3+./hangman < input.in

44rm -f hangman *.ibc

test/effects004/expected → test/effects004/expected.outrenamed

The content is the same.

test/effects004/input → test/effects004/input.inrenamed

The content is the same.

test/effects004/run → test/effects004/run.shrenamed+1−1

@@ -1,4 +1,4 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ effects004.idr -o effects004 -p effects

3−./effects004 < input

3+./effects004 < input.in

44rm -f effects004 *.ibc

test/effects005/expected → test/effects005/expected.outrenamed

The content is the same.

test/effects005/run → test/effects005/run.shrenamed

Only the mode changed.

test/error001/expected → test/error001/expected.outrenamed

The content is the same.

test/error001/run → test/error001/run.shrenamed

Only the mode changed.

test/error002/expected → test/error002/expected.outrenamed

The content is the same.

test/error002/run → test/error002/run.shrenamed

Only the mode changed.

test/error003/expected → test/error003/expected.outrenamed

The content is the same.

test/error003/run → test/error003/run.shrenamed

Only the mode changed.

test/error004/expected → test/error004/expected.outrenamed

The content is the same.

test/error004/run → test/error004/run.shrenamed

Only the mode changed.

test/error005/expected → test/error005/expected.outrenamed

The content is the same.

test/error005/run → test/error005/run.shrenamed

Only the mode changed.

test/error006/expected → test/error006/expected.outrenamed

The content is the same.

test/error006/run → test/error006/run.shrenamed

Only the mode changed.

test/error007/expected → test/error007/expected.outrenamed

The content is the same.

test/error007/run → test/error007/run.shrenamed

Only the mode changed.

test/error008/expected → test/error008/expected.outrenamed

The content is the same.

test/error008/run → test/error008/run.shrenamed

Only the mode changed.

test/error009/expected → test/error009/expected.outrenamed

The content is the same.

test/error009/run → test/error009/run.shrenamed

Only the mode changed.

test/ffi001/expected → test/ffi001/expected.outrenamed

The content is the same.

test/ffi001/run → test/ffi001/run.shrenamed

Only the mode changed.

test/ffi002/expected → test/ffi002/expected.outrenamed

The content is the same.

test/ffi002/run → test/ffi002/run.shrenamed

Only the mode changed.

test/ffi003/expected → test/ffi003/expected.outrenamed

The content is the same.

test/ffi003/input → test/ffi003/input.inrenamed

The content is the same.

test/ffi003/run → test/ffi003/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour test024.idr --exec main < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour test024.idr --exec main < input.in

33rm -f *.ibc

test/ffi004/expected → test/ffi004/expected.outrenamed

The content is the same.

test/ffi004/run → test/ffi004/run.shrenamed

Only the mode changed.

test/ffi005/expected → test/ffi005/expected.outrenamed

The content is the same.

test/ffi005/run → test/ffi005/run.shrenamed

Only the mode changed.

test/ffi006/expected → test/ffi006/expected.outrenamed

The content is the same.

test/ffi006/run → test/ffi006/run.shrenamed

Only the mode changed.

test/ffi007/expected → test/ffi007/expected.outrenamed

The content is the same.

test/ffi007/run → test/ffi007/run.shrenamed

The content is the same.

test/ffi008/expected → test/ffi008/expected.outrenamed

The content is the same.

test/ffi008/run → test/ffi008/run.shrenamed

The content is the same.

test/ffi009/expected → test/ffi009/expected.outrenamed

The content is the same.

test/ffi009/run → test/ffi009/run.shrenamed

Only the mode changed.

test/ffi010/expected → test/ffi010/expected.outrenamed

The content is the same.

test/ffi010/run → test/ffi010/run.shrenamed

Only the mode changed.

test/ffi011/expected → test/ffi011/expected.outrenamed

The content is the same.

test/ffi011/ffi011 → test/ffi011/ffi011.jsrenamed

The content is the same.

test/ffi011/run → test/ffi011/run.shrenamed+1−1

@@ -1,4 +1,4 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ ffi011.idr --interface -o lib.js

3−node ./ffi011

3+node ./ffi011.js

44rm -f *.ibc lib.js

test/ffi012/expected → test/ffi012/expected.outrenamed

The content is the same.

test/ffi012/ffi012 → test/ffi012/ffi012.jsrenamed

The content is the same.

test/ffi012/run → test/ffi012/run.shrenamed

Only the mode changed.

test/ffi013/expected → test/ffi013/expected.outrenamed

The content is the same.

test/ffi013/run → test/ffi013/run.shrenamed

Only the mode changed.

test/folding001/expected → test/folding001/expected.outrenamed

The content is the same.

test/folding001/run → test/folding001/run.shrenamed

Only the mode changed.

test/idrisdoc001/expected → test/idrisdoc001/expected.outrenamed

The content is the same.

test/idrisdoc001/run → test/idrisdoc001/run.shrenamed

Only the mode changed.

test/idrisdoc002/expected → test/idrisdoc002/expected.outrenamed

The content is the same.

test/idrisdoc002/run → test/idrisdoc002/run.shrenamed

Only the mode changed.

test/idrisdoc003/expected → test/idrisdoc003/expected.outrenamed

The content is the same.

test/idrisdoc003/run → test/idrisdoc003/run.shrenamed

Only the mode changed.

test/idrisdoc004/expected → test/idrisdoc004/expected.outrenamed

The content is the same.

test/idrisdoc004/run → test/idrisdoc004/run.shrenamed

Only the mode changed.

test/idrisdoc005/expected → test/idrisdoc005/expected.outrenamed

The content is the same.

test/idrisdoc005/run → test/idrisdoc005/run.shrenamed

Only the mode changed.

test/idrisdoc006/expected → test/idrisdoc006/expected.outrenamed

The content is the same.

test/idrisdoc006/run → test/idrisdoc006/run.shrenamed

Only the mode changed.

test/idrisdoc007/expected → test/idrisdoc007/expected.outrenamed

The content is the same.

test/idrisdoc007/run → test/idrisdoc007/run.shrenamed

Only the mode changed.

test/idrisdoc008/expected → test/idrisdoc008/expected.outrenamed

The content is the same.

test/idrisdoc008/run → test/idrisdoc008/run.shrenamed

Only the mode changed.

test/idrisdoc009/expected → test/idrisdoc009/expected.outrenamed

The content is the same.

test/idrisdoc009/input → test/idrisdoc009/input.inrenamed

The content is the same.

test/idrisdoc009/run → test/idrisdoc009/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --quiet --port none Test.idr < input

2+${IDRIS:-idris} $@ --nocolour --quiet --port none Test.idr < input.in

33rm -f *.ibc

test/interactive001/expected → test/interactive001/expected.outrenamed

The content is the same.

test/interactive001/input → test/interactive001/input.inrenamed

The content is the same.

test/interactive001/run → test/interactive001/run.shrenamed+1−1

@@ -1,5 +1,5 @@

11#!/usr/bin/env bash

3−${IDRIS:-idris} $@ --quiet --port none --indent-with 8 interactive001.idr < input

3+${IDRIS:-idris} $@ --quiet --port none --indent-with 8 interactive001.idr < input.in

55rm -f *.ibc

test/interactive002/expected → test/interactive002/expected.outrenamed

The content is the same.

test/interactive002/input → test/interactive002/input.inrenamed

The content is the same.

test/interactive002/run → test/interactive002/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive002.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive002.idr < input.in

33rm -f *.ibc

test/interactive003/expected → test/interactive003/expected.outrenamed

The content is the same.

test/interactive003/input → test/interactive003/input.inrenamed

The content is the same.

test/interactive003/run → test/interactive003/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive003.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive003.idr < input.in

33rm -f *.ibc

test/interactive004/expected → test/interactive004/expected.outrenamed

The content is the same.

test/interactive004/input → test/interactive004/input.inrenamed

The content is the same.

test/interactive004/run → test/interactive004/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive004.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive004.idr < input.in

33rm -f *.ibc

test/interactive005/expected → test/interactive005/expected.outrenamed

The content is the same.

test/interactive005/input → test/interactive005/input.inrenamed

The content is the same.

test/interactive005/run → test/interactive005/run.shrenamed+1−1

@@ -1,5 +1,5 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --quiet --port none interactive005.idr --consolewidth 70 < input

2+${IDRIS:-idris} $@ --nocolour --quiet --port none interactive005.idr --consolewidth 70 < input.in

33rm -f *.ibc

44rm -f hello.bytecode

55rm -f hello

test/interactive006/expected → test/interactive006/expected.outrenamed

The content is the same.

test/interactive006/input → test/interactive006/input.inrenamed

The content is the same.

test/interactive006/run → test/interactive006/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --port 5000 interactive006.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --port 5000 interactive006.idr < input.in

33rm -f *.ibc

test/interactive007/expected → test/interactive007/expected.outrenamed

The content is the same.

test/interactive007/input → test/interactive007/input.inrenamed

The content is the same.

test/interactive007/run → test/interactive007/run.shrenamed+1−1

@@ -1,2 +1,2 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ -p contrib --nobanner --nocolor --port none < input | perl -pe 's-Data\\Z-Data/Z-g'

2+${IDRIS:-idris} $@ -p contrib --nobanner --nocolor --port none < input.in | perl -pe 's-Data\\Z-Data/Z-g'

test/interactive008/expected → test/interactive008/expected.outrenamed

The content is the same.

test/interactive008/input → test/interactive008/input.inrenamed

The content is the same.

test/interactive008/rundeleted−2

@@ -1,2 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nobanner --nocolor --port none < input

test/interactive008/run.shnew file+2

@@ -0,0 +1,2 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --nobanner --nocolor --port none < input.in

test/interactive009/expected → test/interactive009/expected.outrenamed

The content is the same.

test/interactive009/input → test/interactive009/input.inrenamed

The content is the same.

test/interactive009/run → test/interactive009/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive009.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive009.idr < input.in

33rm -f *.ibc

test/interactive010/expected → test/interactive010/expected.outrenamed

The content is the same.

test/interactive010/input → test/interactive010/input.inrenamed

The content is the same.

test/interactive010/run → test/interactive010/run.shrenamed+1−1

@@ -1,2 +1,2 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nobanner --nocolor < input

2+${IDRIS:-idris} $@ --quiet --port none --nobanner --nocolor < input.in

test/interactive011/expected → test/interactive011/expected.outrenamed

The content is the same.

test/interactive011/input → test/interactive011/input.inrenamed

The content is the same.

test/interactive011/run → test/interactive011/run.shrenamed+1−1

@@ -1,6 +1,6 @@

11#!/usr/bin/env bash

33cd src

4−${IDRIS:-idris} "$@" --quiet --port none --indent-clause 4 Main.idr <../input

4+${IDRIS:-idris} "$@" --quiet --port none --indent-clause 4 Main.idr <../input.in

66rm -f *.ibc

test/interactive012/expected → test/interactive012/expected.outrenamed

The content is the same.

test/interactive012/input → test/interactive012/input.inrenamed

The content is the same.

test/interactive012/run → test/interactive012/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --consolewidth 70 --quiet --port none interactive012.idr < input

2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 --quiet --port none interactive012.idr < input.in

33rm -f *.ibc

test/interactive013/expected → test/interactive013/expected.outrenamed

The content is the same.

test/interactive013/input → test/interactive013/input.inrenamed

The content is the same.

test/interactive013/run → test/interactive013/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive013.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive013.idr < input.in

33rm -f *.ibc

test/interactive014/expected → test/interactive014/expected.outrenamed

The content is the same.

test/interactive014/input → test/interactive014/input.inrenamed

The content is the same.

test/interactive014/run → test/interactive014/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive014.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive014.idr < input.in

33rm -f *.ibc

test/interactive015/expected → test/interactive015/expected.outrenamed

The content is the same.

test/interactive015/input → test/interactive015/input.inrenamed

The content is the same.

test/interactive015/run → test/interactive015/run.shrenamed+1−1

@@ -1,7 +1,7 @@

11#!/usr/bin/env bash

33cp src/interactive015.idr .

4−${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input

4+${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input.in

66cat interactive015.idr

test/interactive016/expected → test/interactive016/expected.outrenamed

The content is the same.

test/interactive016/input → test/interactive016/input.inrenamed

The content is the same.

test/interactive016/run → test/interactive016/run.shrenamed+1−1

@@ -1,7 +1,7 @@

11#!/usr/bin/env bash

33cp src/interactive016.idr .

4−${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input

4+${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input.in

66cat interactive016.idr

test/interactive017/expected → test/interactive017/expected.outrenamed

The content is the same.

test/interactive017/run → test/interactive017/run.shrenamed

Only the mode changed.

test/interactive018/expected → test/interactive018/expected.outrenamed

The content is the same.

test/interactive018/input → test/interactive018/input.inrenamed

The content is the same.

test/interactive018/rundeleted−3

@@ -1,3 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none Top.idr < input

3−rm -f *.ibc

test/interactive018/run.shnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none Top.idr < input.in

3+rm -f *.ibc

test/interfaces001/expected → test/interfaces001/expected.outrenamed

The content is the same.

test/interfaces001/input → test/interfaces001/input.inrenamed

The content is the same.

test/interfaces001/run → test/interfaces001/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour --consolewidth 70 InterfaceName.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour --consolewidth 70 InterfaceName.idr < input.in

33rm -f *.ibc

test/interfaces002/expected → test/interfaces002/expected.outrenamed

The content is the same.

test/interfaces002/run → test/interfaces002/run.shrenamed

Only the mode changed.

test/interfaces003/expected → test/interfaces003/expected.outrenamed

The content is the same.

test/interfaces003/run → test/interfaces003/run.shrenamed

Only the mode changed.

test/interfaces004/expected → test/interfaces004/expected.outrenamed

The content is the same.

test/interfaces004/run → test/interfaces004/run.shrenamed

Only the mode changed.

test/interfaces005/expected → test/interfaces005/expected.outrenamed

The content is the same.

test/interfaces005/run → test/interfaces005/run.shrenamed

Only the mode changed.

test/interfaces006/expected → test/interfaces006/expected.outrenamed

The content is the same.

test/interfaces006/run → test/interfaces006/run.shrenamed

Only the mode changed.

test/interfaces007/expected → test/interfaces007/expected.outrenamed

The content is the same.

test/interfaces007/run → test/interfaces007/run.shrenamed

Only the mode changed.

test/interfaces008/expected → test/interfaces008/expected.outrenamed

The content is the same.

test/interfaces008/run → test/interfaces008/run.shrenamed

Only the mode changed.

test/interfaces009/expected → test/interfaces009/expected.outrenamed

The content is the same.

test/interfaces009/run → test/interfaces009/run.shrenamed

Only the mode changed.

test/interfaces010/expected → test/interfaces010/expected.outrenamed

The content is the same.

test/interfaces010/run → test/interfaces010/run.shrenamed

Only the mode changed.

test/interpret001/expected → test/interpret001/expected.outrenamed

The content is the same.

test/interpret001/input → test/interpret001/input.inrenamed

The content is the same.

test/interpret001/run → test/interpret001/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour double-echo.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour double-echo.idr < input.in

33rm -f *.ibc

test/interpret002/expected → test/interpret002/expected.outrenamed

The content is the same.

test/interpret002/input → test/interpret002/input.inrenamed

The content is the same.

test/interpret002/run → test/interpret002/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour file-error.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour file-error.idr < input.in

33rm -f *.ibc

test/interpret003/expected → test/interpret003/expected.outrenamed

The content is the same.

test/interpret003/input → test/interpret003/input.inrenamed

The content is the same.

test/interpret003/run → test/interpret003/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour interpret003.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour interpret003.idr < input.in

33rm -f *.ibc

test/io001/expected → test/io001/expected.outrenamed

The content is the same.

test/io001/run → test/io001/run.shrenamed

Only the mode changed.

test/io002/expected → test/io002/expected.outrenamed

The content is the same.

test/io002/run → test/io002/run.shrenamed

Only the mode changed.

test/io003/expected → test/io003/expected.outrenamed

The content is the same.

test/io003/run → test/io003/run.shrenamed

Only the mode changed.

test/layout001/expected → test/layout001/expected.outrenamed

The content is the same.

test/layout001/run → test/layout001/run.shrenamed

Only the mode changed.

test/literate001/expected → test/literate001/expected.outrenamed

The content is the same.

test/literate001/run → test/literate001/run.shrenamed

Only the mode changed.

test/meta001/expected → test/meta001/expected.outrenamed

The content is the same.

test/meta001/run → test/meta001/run.shrenamed

Only the mode changed.

test/meta002/expected → test/meta002/expected.outrenamed

The content is the same.

test/meta002/run → test/meta002/run.shrenamed

Only the mode changed.

test/meta003/expected → test/meta003/expected.outrenamed

The content is the same.

test/meta003/run → test/meta003/run.shrenamed

Only the mode changed.

test/meta004/expected → test/meta004/expected.outrenamed

The content is the same.

test/meta004/run → test/meta004/run.shrenamed

Only the mode changed.

test/pkg001/expected → test/pkg001/expected.outrenamed

The content is the same.

test/pkg001/run → test/pkg001/run.shrenamed

Only the mode changed.

test/pkg002/expected → test/pkg002/expected.outrenamed

The content is the same.

test/pkg002/run → test/pkg002/run.shrenamed

Only the mode changed.

test/pkg003/expected → test/pkg003/expected.outrenamed

The content is the same.

test/pkg003/run → test/pkg003/run.shrenamed

Only the mode changed.

test/pkg004/expected → test/pkg004/expected.outrenamed

The content is the same.

test/pkg004/run → test/pkg004/run.shrenamed

Only the mode changed.

test/pkg005/expected → test/pkg005/expected.outrenamed

The content is the same.

test/pkg005/run → test/pkg005/run.shrenamed

Only the mode changed.

test/pkg006/expected → test/pkg006/expected.outrenamed

The content is the same.

test/pkg006/run → test/pkg006/run.shrenamed

Only the mode changed.

test/pkg007/expected → test/pkg007/expected.outrenamed

The content is the same.

test/pkg007/input → test/pkg007/input.inrenamed

The content is the same.

test/pkg007/run → test/pkg007/run.shrenamed+1−1

@@ -2,6 +2,6 @@

22cd toy

33${IDRIS:-idris} $@ --build toy.ipkg --ibcsubdir ../ibcout

44cd ../ibcout

5−${IDRIS:-idris} $@ --quiet < ../input

5+${IDRIS:-idris} $@ --quiet < ../input.in

66cd ..

77rm -rf ibcout

test/pkg008/expected → test/pkg008/expected.outrenamed

The content is the same.

test/pkg008/run → test/pkg008/run.shrenamed

Only the mode changed.

test/pkg009/expected → test/pkg009/expected.outrenamed

The content is the same.

test/pkg009/run → test/pkg009/run.shrenamed

Only the mode changed.

test/pkg010/expecteddeleted−31

@@ -1,31 +0,0 @@

1−Uncaught error: user error (wrongopts.ipkg:4:1:

2− |

3−4 | <empty line>

4− | ^

5−Invalid option `-total'

6−

8− [--client ARG] | [--log LEVEL] | [--logging-categories CATS] |

9− [--nobasepkgs] | [--noprelude] | [--nobuiltins] | [--check] |

11− [--partial] | [--warnpartial] | [--warnreach] | [--warnipkg] |

12− [--nocoverage] | [--errorcontext] | [--info] | [--listlogcats] |

14− | [--V1] | [-V|--V0|--verbose] | [--ibcsubdir FILE] |

15− [-i|--idrispath ARG] | [--sourcepath ARG] | [--warn] |

17− [--repl IPKG] | [--clean IPKG] | [--mkdoc IPKG] | [--installdoc IPKG] |

18− [--checkpkg IPKG] | [--testpkg IPKG] | [--indent-with INDENT] |

19− [--indent-clause INDENT] | [--bytecode ARG] | [-S|--codegenonly] |

20− [-c|--compileonly] | [--dumpdefuns ARG] | [--dumpcases ARG] |

21− [--codegen TARGET] | [--portable-codegen TARGET] | [--cg-opt ARG] |

23− [--O3] | [--O2] | [--O1] | [--O0] | [--partial-eval] |

24− [--no-partial-eval] |

25− [--optimise-nat-like-types|--optimize-nat-like-types] |

26− [--no-optimise-nat-like-types|--no-optimize-nat-like-types] |

29− [--no-tactic-deprecation-warnings] |

30− [--allow-capitalized-pattern-variables]) [FILES] [-v|--version]

31−)

test/pkg010/expected.outnew file+29

@@ -0,0 +1,29 @@

1+Uncaught error: user error (wrongopts.ipkg:4:1:

2+ |

3+4 | <empty line>

4+ | ^

5+Invalid option `-total'

8+ --client ARG | --log LEVEL | --logging-categories CATS |

9+ --nobasepkgs | --noprelude | --nobuiltins | --check |

13+ --libdir | --docdir | --include | --V2 | --V1 | (-V|--V0|--verbose) |

16+ --repl IPKG | --clean IPKG | --mkdoc IPKG | --installdoc IPKG |

17+ --checkpkg IPKG | --testpkg IPKG | --indent-with INDENT |

18+ --indent-clause INDENT | --bytecode ARG | (-S|--codegenonly) |

19+ (-c|--compileonly) | --dumpdefuns ARG | --dumpcases ARG |

20+ --codegen TARGET | --portable-codegen TARGET | --cg-opt ARG |

22+ --O3 | --O2 | --O1 | --O0 | --partial-eval | --no-partial-eval |

23+ (--optimise-nat-like-types|--optimize-nat-like-types) |

24+ (--no-optimise-nat-like-types|--no-optimize-nat-like-types) |

26+ (--nocolor|--nocolour) | --consolewidth WIDTH | --highlight |

27+ --no-tactic-deprecation-warnings |

28+ --allow-capitalized-pattern-variables] [FILES] [-v|--version]

29+)

test/pkg010/run → test/pkg010/run.shrenamed

Only the mode changed.

test/prelude001/expected → test/prelude001/expected.outrenamed

The content is the same.

test/prelude001/run → test/prelude001/run.shrenamed

Only the mode changed.

test/primitives001/expected → test/primitives001/expected.outrenamed

The content is the same.

test/primitives001/input → test/primitives001/input.inrenamed

The content is the same.

test/primitives001/run → test/primitives001/run.shrenamed+1−1

@@ -2,5 +2,5 @@

22${IDRIS:-idris} $@ test005.idr -o test005

33./test005

44${IDRIS:-idris} $@ substring.idr -o substring

5−./substring < input

5+./substring < input.in

66rm -f test005 substring *.ibc

test/primitives002/expected → test/primitives002/expected.outrenamed

The content is the same.

test/primitives002/run → test/primitives002/run.shrenamed

Only the mode changed.

test/primitives003/expected → test/primitives003/expected.outrenamed

The content is the same.

test/primitives003/run → test/primitives003/run.shrenamed

Only the mode changed.

test/primitives004-disabled/expected → test/primitives004-disabled/expected.outrenamed

The content is the same.

test/primitives004-disabled/run → test/primitives004-disabled/run.shrenamed

Only the mode changed.

test/primitives005/expected → test/primitives005/expected.outrenamed

The content is the same.

test/primitives005/run → test/primitives005/run.shrenamed

The content is the same.

test/primitives006/expected → test/primitives006/expected.outrenamed

The content is the same.

test/primitives006/run → test/primitives006/run.shrenamed

Only the mode changed.

test/proof001/expected → test/proof001/expected.outrenamed

The content is the same.

test/proof001/run → test/proof001/run.shrenamed

Only the mode changed.

test/proof002/expected → test/proof002/expected.outrenamed

The content is the same.

test/proof002/run → test/proof002/run.shrenamed

Only the mode changed.

test/proof003/expected → test/proof003/expected.outrenamed

The content is the same.

test/proof003/run → test/proof003/run.shrenamed

Only the mode changed.

test/proof004/expected → test/proof004/expected.outrenamed

The content is the same.

test/proof004/run → test/proof004/run.shrenamed

Only the mode changed.

test/proof005/expected → test/proof005/expected.outrenamed

The content is the same.

test/proof005/run → test/proof005/run.shrenamed

Only the mode changed.

test/proof006/expected → test/proof006/expected.outrenamed

The content is the same.

test/proof006/run → test/proof006/run.shrenamed

Only the mode changed.

test/proof007/expected → test/proof007/expected.outrenamed

The content is the same.

test/proof007/run → test/proof007/run.shrenamed

Only the mode changed.

test/proof008/expected → test/proof008/expected.outrenamed

The content is the same.

test/proof008/run → test/proof008/run.shrenamed

Only the mode changed.

test/proof009/expected → test/proof009/expected.outrenamed

The content is the same.

test/proof009/input → test/proof009/input.inrenamed

The content is the same.

test/proof009/run → test/proof009/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --consolewidth 70 --quiet --port none proof009.idr < input

2+${IDRIS:-idris} $@ --consolewidth 70 --quiet --port none proof009.idr < input.in

33rm -f *.ibc

test/proof010/expected → test/proof010/expected.outrenamed

The content is the same.

test/proof010/run → test/proof010/run.shrenamed

Only the mode changed.

test/proof011/expected → test/proof011/expected.outrenamed

The content is the same.

test/proof011/run → test/proof011/run.shrenamed

Only the mode changed.

test/proofsearch001/expected → test/proofsearch001/expected.outrenamed

The content is the same.

test/proofsearch001/run → test/proofsearch001/run.shrenamed

Only the mode changed.

test/proofsearch002/expected → test/proofsearch002/expected.outrenamed

The content is the same.

test/proofsearch002/run → test/proofsearch002/run.shrenamed

Only the mode changed.

test/proofsearch003/expected → test/proofsearch003/expected.outrenamed

The content is the same.

test/proofsearch003/run → test/proofsearch003/run.shrenamed

Only the mode changed.

test/pruviloj001/expected → test/pruviloj001/expected.outrenamed

The content is the same.

test/pruviloj001/run → test/pruviloj001/run.shrenamed

Only the mode changed.

test/quasiquote001/expected → test/quasiquote001/expected.outrenamed

The content is the same.

test/quasiquote001/run → test/quasiquote001/run.shrenamed

Only the mode changed.

test/quasiquote002/expected → test/quasiquote002/expected.outrenamed

The content is the same.

test/quasiquote002/run → test/quasiquote002/run.shrenamed

Only the mode changed.

test/quasiquote003/expected → test/quasiquote003/expected.outrenamed

The content is the same.

test/quasiquote003/run → test/quasiquote003/run.shrenamed

Only the mode changed.

test/quasiquote004/expected → test/quasiquote004/expected.outrenamed

The content is the same.

test/quasiquote004/run → test/quasiquote004/run.shrenamed

Only the mode changed.

test/quasiquote005/expected → test/quasiquote005/expected.outrenamed

The content is the same.

test/quasiquote005/run → test/quasiquote005/run.shrenamed

Only the mode changed.

test/quasiquote006/expected → test/quasiquote006/expected.outrenamed

The content is the same.

test/quasiquote006/run → test/quasiquote006/run.shrenamed

Only the mode changed.

test/records001/expected → test/records001/expected.outrenamed

The content is the same.

test/records001/run → test/records001/run.shrenamed

Only the mode changed.

test/records002/expected → test/records002/expected.outrenamed

The content is the same.

test/records002/run → test/records002/run.shrenamed

Only the mode changed.

test/records003/expected → test/records003/expected.outrenamed

The content is the same.

test/records003/run → test/records003/run.shrenamed

Only the mode changed.

test/records004/expected → test/records004/expected.outrenamed

The content is the same.

test/records004/run → test/records004/run.shrenamed

Only the mode changed.

test/records005/expected → test/records005/expected.outrenamed

The content is the same.

test/records005/run → test/records005/run.shrenamed

Only the mode changed.

test/reg001/expected → test/reg001/expected.outrenamed

The content is the same.

test/reg001/run → test/reg001/run.shrenamed

Only the mode changed.

test/reg002/expected → test/reg002/expected.outrenamed

The content is the same.

test/reg002/run → test/reg002/run.shrenamed

Only the mode changed.

test/reg004/expected → test/reg004/expected.outrenamed

The content is the same.

test/reg004/run → test/reg004/run.shrenamed

Only the mode changed.

test/reg005/expected → test/reg005/expected.outrenamed

The content is the same.

test/reg005/run → test/reg005/run.shrenamed

Only the mode changed.

test/reg007/expected → test/reg007/expected.outrenamed

The content is the same.

test/reg007/run → test/reg007/run.shrenamed

Only the mode changed.

test/reg013/expected → test/reg013/expected.outrenamed

The content is the same.

test/reg013/run → test/reg013/run.shrenamed

Only the mode changed.

test/reg016/expected → test/reg016/expected.outrenamed

The content is the same.

test/reg016/run → test/reg016/run.shrenamed

Only the mode changed.

test/reg017/expected → test/reg017/expected.outrenamed

The content is the same.

test/reg017/run → test/reg017/run.shrenamed

Only the mode changed.

test/reg020/expected → test/reg020/expected.outrenamed

The content is the same.

test/reg020/run → test/reg020/run.shrenamed

Only the mode changed.

test/reg024/expected → test/reg024/expected.outrenamed

The content is the same.

test/reg024/run → test/reg024/run.shrenamed

Only the mode changed.

test/reg025/expected → test/reg025/expected.outrenamed

The content is the same.

test/reg025/run → test/reg025/run.shrenamed

Only the mode changed.

test/reg027/expected → test/reg027/expected.outrenamed

The content is the same.

test/reg027/run → test/reg027/run.shrenamed

Only the mode changed.

test/reg029/expected → test/reg029/expected.outrenamed

The content is the same.

test/reg029/run → test/reg029/run.shrenamed

Only the mode changed.

test/reg031/expected → test/reg031/expected.outrenamed

The content is the same.

test/reg031/run → test/reg031/run.shrenamed

Only the mode changed.

test/reg032/expected → test/reg032/expected.outrenamed

The content is the same.

test/reg032/run → test/reg032/run.shrenamed

Only the mode changed.

test/reg039/expected → test/reg039/expected.outrenamed

The content is the same.

test/reg039/run → test/reg039/run.shrenamed

Only the mode changed.

test/reg040/expected → test/reg040/expected.outrenamed

The content is the same.

test/reg040/run → test/reg040/run.shrenamed

Only the mode changed.

test/reg041/expected → test/reg041/expected.outrenamed

The content is the same.

test/reg041/run → test/reg041/run.shrenamed

Only the mode changed.

test/reg042/expected → test/reg042/expected.outrenamed

The content is the same.

test/reg042/run → test/reg042/run.shrenamed

Only the mode changed.

test/reg045/expected → test/reg045/expected.outrenamed

The content is the same.

test/reg045/run → test/reg045/run.shrenamed

Only the mode changed.

test/reg048/expected → test/reg048/expected.outrenamed

The content is the same.

test/reg048/run → test/reg048/run.shrenamed

Only the mode changed.

test/reg051-disabled/expected → test/reg051-disabled/expected.outrenamed

The content is the same.

test/reg051-disabled/run → test/reg051-disabled/run.shrenamed

Only the mode changed.

test/reg052/expected → test/reg052/expected.outrenamed

The content is the same.

test/reg052/run → test/reg052/run.shrenamed

Only the mode changed.

test/reg067/expected → test/reg067/expected.outrenamed

The content is the same.

test/reg067/run → test/reg067/run.shrenamed

Only the mode changed.

test/reg075/expected → test/reg075/expected.outrenamed

The content is the same.

test/reg075/input → test/reg075/input.inrenamed

The content is the same.

test/reg075/rundeleted−3

@@ -1,3 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none reg075.idr < input

3−rm -f *.ibc

test/reg075/run.shnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none reg075.idr < input.in

3+rm -f *.ibc

test/reg076/expected → test/reg076/expected.outrenamed

The content is the same.

test/reg076/input → test/reg076/input.inrenamed

The content is the same.

test/reg076/run → test/reg076/run.shrenamed

Only the mode changed.

test/reg077/expected → test/reg077/expected.outrenamed

The content is the same.

test/reg077/run → test/reg077/run.shrenamed

Only the mode changed.

test/regression001/expected → test/regression001/expected.outrenamed

The content is the same.

test/regression001/run → test/regression001/run.shrenamed

Only the mode changed.

test/regression002/expected → test/regression002/expected.outrenamed

The content is the same.

test/regression002/run → test/regression002/run.shrenamed

Only the mode changed.

test/regression003/expected → test/regression003/expected.outrenamed

The content is the same.

test/regression003/run → test/regression003/run.shrenamed

Only the mode changed.

test/sourceLocation001/expected → test/sourceLocation001/expected.outrenamed

The content is the same.

test/sourceLocation001/run → test/sourceLocation001/run.shrenamed

Only the mode changed.

test/st001/expected → test/st001/expected.outrenamed

The content is the same.

test/st001/run → test/st001/run.shrenamed

Only the mode changed.

test/st001/test001.idr+1−1

@@ -40,7 +40,7 @@ readFileCount fh cnt =

4040

4141testFile : (ConsoleIO m, File m) => ST m () []

4242testFile = with ST do

43− Right fileHandle <- open "testFile" Read

43+ Right fileHandle <- open "testFile.in" Read

4444 | Left ferr => do putStrLn (show ferr)

4545 pure ()

4646 count <- new 0

test/st001/testFile → test/st001/testFile.inrenamed

The content is the same.

test/st002/expected → test/st002/expected.outrenamed

The content is the same.

test/st002/run → test/st002/run.shrenamed

Only the mode changed.

test/st002/test002.idr+1−1

@@ -40,7 +40,7 @@ readFileCount fh cnt =

4040

4141testFile : (ConsoleIO m, File m) => ST m () []

4242testFile = with ST do

43− Right fileHandle <- open "testFile" Read

43+ Right fileHandle <- open "testFile.in" Read

4444 | Left ferr => do putStrLn (show ferr)

4545 pure ()

4646 count <- new 0

test/st002/testFile → test/st002/testFile.inrenamed

The content is the same.

test/st003/expected → test/st003/expected.outrenamed

The content is the same.

test/st003/run → test/st003/run.shrenamed

Only the mode changed.

test/st003/test003.idr+1−1

@@ -7,7 +7,7 @@ import Control.ST.ImplicitCall

88testFile : (ConsoleIO m, File m) => ST m () []

99testFile = with ST do

10− Right str <- readFile "testFile"

10+ Right str <- readFile "testFile.in"

1111 | Left ferr => do putStrLn (show ferr)

1212 pure ()

1313 putStrLn str

test/st003/testFile → test/st003/testFile.inrenamed

The content is the same.

test/st004/expected → test/st004/expected.outrenamed

The content is the same.

test/st004/run → test/st004/run.shrenamed

Only the mode changed.

test/st005/expected → test/st005/expected.outrenamed

The content is the same.

test/st005/run → test/st005/run.shrenamed

Only the mode changed.

test/st006/expected → test/st006/expected.outrenamed

The content is the same.

test/st006/run → test/st006/run.shrenamed

Only the mode changed.

test/st007/expected → test/st007/expected.outrenamed

The content is the same.

test/st007/run → test/st007/run.shrenamed

Only the mode changed.

test/sugar001/expected → test/sugar001/expected.outrenamed

The content is the same.

test/sugar001/run → test/sugar001/run.shrenamed

Only the mode changed.

test/sugar002/expected → test/sugar002/expected.outrenamed

The content is the same.

test/sugar002/run → test/sugar002/run.shrenamed

Only the mode changed.

test/sugar003/expected → test/sugar003/expected.outrenamed

The content is the same.

test/sugar003/run → test/sugar003/run.shrenamed

Only the mode changed.

test/sugar004/expected → test/sugar004/expected.outrenamed

The content is the same.

test/sugar004/run → test/sugar004/run.shrenamed

Only the mode changed.

test/sugar005/expected → test/sugar005/expected.outrenamed

The content is the same.

test/sugar005/run → test/sugar005/run.shrenamed

Only the mode changed.

test/syntax001/expected → test/syntax001/expected.outrenamed

The content is the same.

test/syntax001/run → test/syntax001/run.shrenamed

Only the mode changed.

test/syntax002/expected → test/syntax002/expected.outrenamed

The content is the same.

test/syntax002/run → test/syntax002/run.shrenamed

Only the mode changed.

test/tactics001/expected → test/tactics001/expected.outrenamed

The content is the same.

test/tactics001/run → test/tactics001/run.shrenamed

Only the mode changed.

test/totality001/expected → test/totality001/expected.outrenamed

The content is the same.

test/totality001/run → test/totality001/run.shrenamed

Only the mode changed.

test/totality002/expected → test/totality002/expected.outrenamed

The content is the same.

test/totality002/run → test/totality002/run.shrenamed

Only the mode changed.

test/totality003/expected → test/totality003/expected.outrenamed

The content is the same.

test/totality003/run → test/totality003/run.shrenamed

Only the mode changed.

test/totality004/expected → test/totality004/expected.outrenamed

The content is the same.

test/totality004/run → test/totality004/run.shrenamed

Only the mode changed.

test/totality005/expected → test/totality005/expected.outrenamed

The content is the same.

test/totality005/run → test/totality005/run.shrenamed

Only the mode changed.

test/totality006/expected → test/totality006/expected.outrenamed

The content is the same.

test/totality006/run → test/totality006/run.shrenamed

Only the mode changed.

test/totality007/expected → test/totality007/expected.outrenamed

The content is the same.

test/totality007/run → test/totality007/run.shrenamed

Only the mode changed.

test/totality008/expected → test/totality008/expected.outrenamed

The content is the same.

test/totality008/run → test/totality008/run.shrenamed

Only the mode changed.

test/totality009/expected → test/totality009/expected.outrenamed

The content is the same.

test/totality009/run → test/totality009/run.shrenamed

Only the mode changed.

test/totality010/expected → test/totality010/expected.outrenamed

The content is the same.

test/totality010/run → test/totality010/run.shrenamed

Only the mode changed.

test/totality011/expected → test/totality011/expected.outrenamed

The content is the same.

test/totality011/run → test/totality011/run.shrenamed

Only the mode changed.

test/totality012/expected → test/totality012/expected.outrenamed

The content is the same.

test/totality012/run → test/totality012/run.shrenamed

Only the mode changed.

test/totality013/expected → test/totality013/expected.outrenamed

The content is the same.

test/totality013/run → test/totality013/run.shrenamed

Only the mode changed.

test/totality014/expected → test/totality014/expected.outrenamed

The content is the same.

test/totality014/run → test/totality014/run.shrenamed

Only the mode changed.

test/totality015/expected → test/totality015/expected.outrenamed

The content is the same.

test/totality015/run → test/totality015/run.shrenamed

Only the mode changed.

test/totality016/expected → test/totality016/expected.outrenamed

The content is the same.

test/totality016/run → test/totality016/run.shrenamed

Only the mode changed.

test/totality017/expected → test/totality017/expected.outrenamed

The content is the same.

test/totality017/run → test/totality017/run.shrenamed

Only the mode changed.

test/totality018/expected → test/totality018/expected.outrenamed

The content is the same.

test/totality018/run → test/totality018/run.shrenamed

Only the mode changed.

test/totality019/expected → test/totality019/expected.outrenamed

The content is the same.

test/totality019/run → test/totality019/run.shrenamed

Only the mode changed.

test/totality020/expected → test/totality020/expected.outrenamed

The content is the same.

test/totality020/run → test/totality020/run.shrenamed

Only the mode changed.

test/totality021/expected → test/totality021/expected.outrenamed

The content is the same.

test/totality021/run → test/totality021/run.shrenamed

Only the mode changed.

test/totality022/expected → test/totality022/expected.outrenamed

The content is the same.

test/totality022/run → test/totality022/run.shrenamed

Only the mode changed.

test/totality023/expected → test/totality023/expected.outrenamed

The content is the same.

test/totality023/run → test/totality023/run.shrenamed

Only the mode changed.

test/totality024/expected → test/totality024/expected.outrenamed

The content is the same.

test/totality024/run → test/totality024/run.shrenamed

Only the mode changed.

test/totality025/expected → test/totality025/expected.outrenamed

The content is the same.

test/totality025/run → test/totality025/run.shrenamed

Only the mode changed.

test/totality026/expected → test/totality026/expected.outrenamed

The content is the same.

test/totality026/run → test/totality026/run.shrenamed

Only the mode changed.

test/tutorial001/expected → test/tutorial001/expected.outrenamed

The content is the same.

test/tutorial001/run → test/tutorial001/run.shrenamed

Only the mode changed.

test/tutorial002/expected → test/tutorial002/expected.outrenamed

The content is the same.

test/tutorial002/run → test/tutorial002/run.shrenamed

Only the mode changed.

test/tutorial003/expected → test/tutorial003/expected.outrenamed

The content is the same.

test/tutorial003/run → test/tutorial003/run.shrenamed

Only the mode changed.

test/tutorial004/expected → test/tutorial004/expected.outrenamed

The content is the same.

test/tutorial004/run → test/tutorial004/run.shrenamed

Only the mode changed.

test/tutorial005/expected → test/tutorial005/expected.outrenamed

The content is the same.

test/tutorial005/run → test/tutorial005/run.shrenamed

Only the mode changed.

test/tutorial006/expected → test/tutorial006/expected.outrenamed

The content is the same.

test/tutorial006/run → test/tutorial006/run.shrenamed

Only the mode changed.

test/tutorial007/expected → test/tutorial007/expected.outrenamed

The content is the same.

test/tutorial007/run → test/tutorial007/run.shrenamed

Only the mode changed.

test/unique001/expected → test/unique001/expected.outrenamed

The content is the same.

test/unique001/run → test/unique001/run.shrenamed

Only the mode changed.

test/unique004/expected → test/unique004/expected.outrenamed

The content is the same.

test/unique004/run → test/unique004/run.shrenamed

Only the mode changed.

test/universes001/expected → test/universes001/expected.outrenamed

The content is the same.

test/universes001/run → test/universes001/run.shrenamed

Only the mode changed.

test/universes002/expected → test/universes002/expected.outrenamed

The content is the same.

test/universes002/run → test/universes002/run.shrenamed

Only the mode changed.

test/views001/expected → test/views001/expected.outrenamed

The content is the same.

test/views001/run → test/views001/run.shrenamed

Only the mode changed.

test/views002/expected → test/views002/expected.outrenamed

The content is the same.

test/views002/run → test/views002/run.shrenamed

Only the mode changed.

test/views003/expected → test/views003/expected.outrenamed

The content is the same.

test/views003/run → test/views003/run.shrenamed

Only the mode changed.