62419f4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

set console width / adjust tests by using --consolewidth to make them work with the curses flag

commit62419f47ad09b79b5ac293a020b0c3ce9a0aeb92 authorAndreas Reuleaux <arx@a-rx.info> dateThu 19 Mar 2015, 11:50 (12 years ago) parentb989e36

18 files changed+39−26

compare with master

unifiedsplit

src/Idris/REPL.hs+4−2 test/basic006/run+3−2 test/basic009/run+6−3 test/docs001/expected+1−1 test/docs001/run+1−1 test/docs002/run+1−1 test/error003/expected+2−1 test/error003/run+1−1 test/error004/expected+6−3 test/error004/run+1−1 test/error005/expected+2−1 test/error005/run+1−1 test/ffi002/run+1−1 test/literate001/run+2−2 test/proof002/expected+2−1 test/proof002/run+2−2 test/proof007/expected+2−1 test/proof007/run+1−1

src/Idris/REPL.hs+4−2

@@ -1518,7 +1518,8 @@ loadInputs inputs toline -- furthest line to read in input source files

15181518

15191519idrisMain :: [Opt] -> Idris ()

15201520idrisMain opts =

1521− do let inputs = opt getFile opts

1521+ do mapM_ setWidth (opt getConsoleWidth opts)

1522+ let inputs = opt getFile opts

15221523 let quiet = Quiet `elem` opts

15231524 let nobanner = NoBanner `elem` opts

15241525 let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts

@@ -1533,6 +1534,7 @@ idrisMain opts =

15331534 let optimise = case opt getOptLevel opts of

15341535 [] -> 2

15351536 xs -> last xs

1537+

15361538 setOptLevel optimise

15371539 let outty = case opt getOutputTy opts of

15381540 [] -> if Interface `elem` opts then

@@ -1555,7 +1557,7 @@ idrisMain opts =

15551557 putIState (i { default_total = True })

15561558 setColourise $ not quiet && last (True : opt getColour opts)

15571559

1558− when (not runrepl) $ mapM_ setWidth (opt getConsoleWidth opts)

1560+

15591561

15601562 mapM_ addLangExt (opt getLanguageExt opts)

15611563 setREPL runrepl

test/basic006/run+3−2

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

11#!/usr/bin/env bash

2−idris $@ test020.idr -o test020

3−idris $@ test020a.idr --check --nocolor

3+idris --consolewidth 80 $@ test020.idr -o test020

4+idris --consolewidth 80 $@ test020a.idr --check --nocolor

45./test020

56rm -f test020 *.ibc

test/basic009/run+6−3

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

11#!/usr/bin/env bash

2−idris $@ Main.idr --nocolour --check && echo MAIN-PASS

3−idris $@ Faulty.idr --nocolour --check && echo FAULTY-PASS

4−idris $@ Multiple.idr --nocolour --check && echo MULTIPLE-PASS

3+idris --consolewidth 80 $@ Main.idr --nocolour --check && echo MAIN-PASS

4+idris --consolewidth 80 $@ Faulty.idr --nocolour --check && echo FAULTY-PASS

5+idris --consolewidth 80 $@ Multiple.idr --nocolour --check && echo MULTIPLE-PASS

58rm -f *.ibc B/*.ibc

test/docs001/expected+1−1

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

11Type checking ./docs001.idr

2−[?1049h[1;29r[m(B[4l[?7h[H[2J[29;1H[r[?1049l >Type class C

2+Type class C

33 class

55Parameters:

test/docs001/run+1−1

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

11#!/usr/bin/env bash

2−idris --nobanner --nocolor --consolewidth 80 docs001.idr < input

2+idris --quiet --nocolor --consolewidth 80 docs001.idr < input

33rm *.ibc

test/docs002/run+1−1

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

11#!/usr/bin/env bash

2−idris --nobanner --nocolor docs002.idr < input

2+idris --consolewidth 80 --nobanner --nocolor docs002.idr < input

33rm *.ibc

test/error003/expected+2−1

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

1−ErrorReflection.idr:68:5:When elaborating right hand side of bad:

1+ErrorReflection.idr:68:5:

2+When elaborating right hand side of bad:

23DSL type error: (t(503) => t'(504)) doesn't match ()

test/error003/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ ErrorReflection.idr --nocolour --check

2+idris --consolewidth 80 $@ ErrorReflection.idr --nocolour --check

33rm -f *.ibc

test/error004/expected+6−3

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

1−FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:

1+FunErrTest.idr:35:10:

2+When elaborating right hand side of badCadr1:

23When elaborating argument cons1 to function FunErrTest.cadr:

34 Could not prove that [] has at least two elements.

4−FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:

5+FunErrTest.idr:38:10:

6+When elaborating right hand side of badCadr2:

57When elaborating argument cons2 to function FunErrTest.cadr:

6− Could not prove that tail [(fromInteger 1)] has at least two elements.

8+ Could not prove that tail [(fromInteger 1)] has at least two

9+ elements.

test/error004/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ FunErrTest.idr --nocolour --check

2+idris --consolewidth 80 $@ FunErrTest.idr --nocolour --check

33rm -f *.ibc

test/error005/expected+2−1

@@ -13,7 +13,8 @@ When elaborating argument prf to function Data.Fin.fromInteger:

1313error005.idr:23:24:When elaborating right hand side of b0rken:

1414When elaborating argument prf to function Data.Fin.fromInteger:

1515 When using n as a literal for a Fin 3

16− Could not show that n is less than 3 because n is a bound variable instead of a constant Integer

16+ Could not show that n is less than 3 because n is a bound

17+ variable instead of a constant Integer

1718error005.idr:28:1:When elaborating right hand side of x:

1819When elaborating argument prf to function Data.Fin.fromInteger:

1920 When using 5 as a literal for a Fin 4

test/error005/run+1−1

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

11#!/usr/bin/env bash

2−idris $@ --check --nocolour error005.idr

2+idris --consolewidth 80 $@ --check --nocolour error005.idr

33rm -f *.ibc

test/ffi002/run+1−1

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

11#!/usr/bin/env bash

2−idris --quiet test023.idr -o test023

2+idris --consolewidth 80 --quiet test023.idr -o test023

33rm -f test023 *.ibc

test/literate001/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ test003a.lidr --check

3−idris $@ test003.lidr -o test003

2+idris --consolewidth 80 $@ test003a.lidr --check

3+idris --consolewidth 80 $@ test003.lidr -o test003

44./test003

55rm -f test003 test003.ibc Lit.ibc

test/proof002/expected+2−1

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

1−Reflect.idr:208:38:When elaborating right hand side of testReflect1:

1+Reflect.idr:208:38:

2+When elaborating right hand side of testReflect1:

23When elaborating an application of function Reflect.getJust:

34 Can't unify

45 IsJust (Just x1) (Type of ItIsJust)

test/proof002/run+2−2

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

11#!/usr/bin/env bash

2−idris $@ test030.idr --check --nocolour

3−idris $@ test030a.idr --check --nocolour

2+idris --consolewidth 80 $@ test030.idr --check --nocolour

3+idris --consolewidth 80 $@ test030a.idr --check --nocolour

44rm -f *.ibc

test/proof007/expected+2−1

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

1−DefaultArgUnknownName.idr:9:6:When elaborating right hand side of test:

1+DefaultArgUnknownName.idr:9:6:

2+When elaborating right hand side of test:

23When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:

34 No such variable sadgjhsag

test/proof007/run+1−1

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

11#!/usr/bin/env bash

2−idris --check $@ DefaultArgUnknownName.idr

2+idris --consolewidth 80 --check $@ DefaultArgUnknownName.idr

33rm -f *.ibc