09263c1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't query width when not a tty

This causes trouble when running non-interactively. Also reinstate the stderr output now that that problem is solved.

commit09263c19398a4718c53b768dde8fff877a3c3f78 authorNiklas Larsson <niklas@mm.st> dateThu 4 Aug 2016, 22:12 (10 years ago) parentb4c661a

30 files changed+58−88

compare with master

unifiedsplit

src/Idris/Output.hs+3−1

@@ -21,6 +21,7 @@ import Idris.IdeMode

2121

2222import Util.Pretty

2323import Util.ScreenSize (getScreenWidth)

24+import Util.System (isATTY)

2425

2526import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)

2627

@@ -67,13 +68,14 @@ iRender d = do w <- getWidth

6768 let ideMode = case idris_outputmode ist of

6869 IdeMode _ _ -> True

6970 _ -> False

71+ tty <- runIO isATTY

7072 case w of

7173 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

7274 ColsWide n -> return $

7375 if n < 1

7476 then renderPretty 1.0 1000000000 d

7577 else renderPretty 0.8 n d

76− AutomaticWidth | ideMode -> return $ renderPretty 1.0 80 d

78+ AutomaticWidth | ideMode || not tty -> return $ renderPretty 1.0 80 d

7779 | otherwise -> do width <- runIO getScreenWidth

7880 return $ renderPretty 0.8 width d

7981

test/TestRun.hs+4−3

@@ -9,6 +9,7 @@ import qualified Data.IntMap as IMap

1010import System.Directory

1111import System.Environment

12+import System.Exit

1213import System.Process

1314import System.Info

1415import System.IO

@@ -90,10 +91,10 @@ mkGoldenTests testFamilies flags =

9091-- this thing.

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

9293runTest path flags = do

93− let run = (proc "bash" ("run" : flags)) {cwd = Just path,

94− std_out = CreatePipe}

95− (_, output, _) <- readCreateProcessWithExitCode run ""

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

95+ (_, output, error_out) <- readCreateProcessWithExitCode run ""

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

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

9798 where

9899 -- Normalise paths e.g. '.\foo.idr' to './foo.idr'.

99100 -- Also embedded paths e.g. ".\\Prelude\\List.idr" to "./Prelude/List.idr".

test/basic006/expected+1−2

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

1−test020a.idr:16:18:

2−When checking right hand side of foo with expected type

1+test020a.idr:16:18:When checking right hand side of foo with expected type

32 List a

54When checking an application of function Prelude.List.reverse:

test/basic009/expected+1−2

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

11MAIN-PASS

22Faulty.idr:6:9-12:WARNING: num is bound as an implicit

33 Did you mean to refer to A.num?

4−Faulty.idr:7:7:

5−When checking right hand side of fault with expected type

4+Faulty.idr:7:7:When checking right hand side of fault with expected type

65 num = 0

87Type mismatch between

test/basic018/expected+1−2

@@ -2,8 +2,7 @@ basic018.idr:7:12-17:WARNING: thing is bound as an implicit

22 Did you mean to refer to Main.thing?

33basic018.idr:12:8-13:WARNING: thing is bound as an implicit

44 Did you mean to refer to Main.thing?

5−basic018.idr:13:6:

6−When checking right hand side of test with expected type

5+basic018.idr:13:6:When checking right hand side of test with expected type

76 thing = S 41

98Type mismatch between

test/directives001/expected+2−4

@@ -6,9 +6,7 @@ directives001.idr:15:7:Use of deprecated name directives001.Foo

66To be replaced with `Bar`.

77directives001.idr:15:7:Use of deprecated name directives001.Foo

88To be replaced with `Bar`.

9−directives001.idr:26:8:

10−Use of a fragile construct directives001.mkBar

9+directives001.idr:26:8:Use of a fragile construct directives001.mkBar

1110How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

12−directives001.idr:26:8:

13−Use of a fragile construct directives001.mkBar

11+directives001.idr:26:8:Use of a fragile construct directives001.mkBar

1412How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

test/docs003/expected+1−2

@@ -6,8 +6,7 @@ Parameters:

77Methods:

88 map : Functor f => (func : a -> b) -> f a -> f b

9− Apply a function across everything of type 'a' in a

10− parameterised type

9+ Apply a function across everything of type 'a' in a parameterised type

1110

1211 The function is Total

1312Implementations:

test/error003/expected+1−2

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

1−ErrorReflection.idr:68:5:

2−When checking right hand side of bad with expected type

1+ErrorReflection.idr:68:5:When checking right hand side of bad with expected type

32 Tm [] TUnit

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

test/error005/expected+5−10

@@ -1,34 +1,29 @@

1−error005.idr:13:1:

2−When checking right hand side of two with expected type

1+error005.idr:13:1:When checking right hand side of two with expected type

32 Fin 2

54When checking argument prf to function Data.Fin.fromInteger:

65 When using 2 as a literal for a Fin 2

76 2 is not strictly less than 2

8−error005.idr:16:1:

9−When checking right hand side of hahaha with expected type

7+error005.idr:16:1:When checking right hand side of hahaha with expected type

108 Fin n

119

1210When checking argument prf to function Data.Fin.fromInteger:

1311 When using 0 as a literal for a Fin n

1412 0 is not strictly less than n

15−error005.idr:22:1:

16−When checking right hand side of notOk with expected type

13+error005.idr:22:1:When checking right hand side of notOk with expected type

1714 Fin (plus 2 n)

1815

1916When checking argument prf to function Data.Fin.fromInteger:

2017 When using 2 as a literal for a Fin (S (S n))

2118 2 is not strictly less than S (S n)

22−error005.idr:23:24:

23−When checking right hand side of b0rken with expected type

19+error005.idr:23:24:When checking right hand side of b0rken with expected type

2420 Fin 3

2521

2622When checking argument prf to function Data.Fin.fromInteger:

2723 When using n as a literal for a Fin 3

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

2925 variable instead of a constant Integer

30−error005.idr:28:1:

31−When checking right hand side of x with expected type

26+error005.idr:28:1:When checking right hand side of x with expected type

3227 Fin 4

3328

3429When checking argument prf to function Data.Fin.fromInteger:

test/layout001/expected+1−2

@@ -72,8 +72,7 @@ y

7272^

7373Checking layout001n.idr

7474Checking mplus1.idr

75−mplus1.idr:13:31:

76−When checking right hand side of term with expected type

75+mplus1.idr:13:31:When checking right hand side of term with expected type

7776 Maybe Int

7877

7978When checking an application of function Prelude.Applicative.pure:

test/proof011/expected+14−10

@@ -1,14 +1,18 @@

1−proof011.idr:19:9:

2−When checking right hand side of vassoc' with expected type

1+proof011.idr:19:9:When checking right hand side of vassoc' with expected type

32 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

5−rewriting xs ++ ys ++ xs to (xs ++ ys) ++

6− xs did not change type x :: xs ++ ys ++ zs =

7− x :: (xs ++ ys) ++ zs

8−proof011a.idr:13:9:

9−When checking right hand side of vassoc' with expected type

4+rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

5+ xs ++

6+ ys ++ zs =

7+ x ::

8+ (xs ++ ys) ++

9+ zs

10+proof011a.idr:13:9:When checking right hand side of vassoc' with expected type

1011 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

1112

12−rewriting xs ++ ys ++ xs to (xs ++ ys) ++

13− xs did not change type x :: xs ++ ys ++ zs =

14− x :: (xs ++ ys) ++ zs

13+rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

14+ xs ++

15+ ys ++ zs =

16+ x ::

17+ (xs ++ ys) ++

18+ zs

test/quasiquote003/expected+1−2

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

1−NoInfer.idr:11:5:

2−When checking right hand side of zzz with expected type

1+NoInfer.idr:11:5:When checking right hand side of zzz with expected type

32 TT

54No such variable k

test/reg007/expected+1−2

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

11reg007.lidr:8:1:A.n is already defined

2−reg007.lidr:12:11-17:

3−When checking right hand side of hurrah with expected type

2+reg007.lidr:12:11-17:When checking right hand side of hurrah with expected type

43 0 = 1

65Type mismatch between

test/reg018/expected+1−2

@@ -8,5 +8,4 @@ reg018b.idr:11:1:

88A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB

99reg018c.idr:21:1:

1010CodataTest.inf is possibly not total due to: with block in CodataTest.inf

11−reg018d.idr:8:1:

12−Main.pull is not total as there are missing cases

11+reg018d.idr:8:1:Main.pull is not total as there are missing cases

test/reg023/expected+1−2

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

1−reg023.idr:7:5:

2−When checking right hand side of bad with expected type

1+reg023.idr:7:5:When checking right hand side of bad with expected type

32 f Nat

54Type mismatch between

test/reg027/expected+1−2

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

11<<int fn>>

226

3−reg027a.idr:9:16:

4−Overlapping implementation: Show (Int -> a) already defined

3+reg027a.idr:9:16:Overlapping implementation: Show (Int -> a) already defined

test/reg028/expected+1−2

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

1−reg028.idr:5:1:

2−tbad.bad is possibly not total due to: with block in tbad.bad

1+reg028.idr:5:1:tbad.bad is possibly not total due to: with block in tbad.bad

32reg028a.idr:17:14-19:

43This style of tactic proof is deprecated. See %runElab for the replacement.

54reg028a.idr:11:1:

test/reg044/expected+1−2

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

11reg044.idr:4:6-11:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−reg044.idr:4:4:

4−When checking right hand side of Main.pf with expected type

3+reg044.idr:4:4:When checking right hand side of Main.pf with expected type

54 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

76Type mismatch between

test/reg049/expected+1−2

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

11reg049.idr:2:9:When checking constructor Main.Bogus:

22Void is not Main.Foo

3−reg049.idr:5:6:

4−When checking right hand side of uhOh with expected type

3+reg049.idr:5:6:When checking right hand side of uhOh with expected type

54 Void

76No such variable Bogus

test/reg068/expected+1−2

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

1−reg068.idr:1:6:

2−Main.nat has a name which may be implicitly bound.

1+reg068.idr:1:6:Main.nat has a name which may be implicitly bound.

32This is likely to lead to problems!

43reg068.idr:2:6:Main.ze has a name which may be implicitly bound.

54This is likely to lead to problems!

test/reg069/expected+1−2

@@ -1,2 +1 @@

1−Mod.idr:11:1:

2−public export Mod.natexp can't refer to export Mod.natfn

1+Mod.idr:11:1:public export Mod.natexp can't refer to export Mod.natfn

test/reg072/expected+1−2

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

1−DoubleEquality.idr:4:87:

2−When checking right hand side of oops with expected type

1+DoubleEquality.idr:4:87:When checking right hand side of oops with expected type

32 Void

54When checking argument value to function Prelude.Basics.the:

test/syntax001/expected+2−4

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

1−Syntax.idr:6:7-9:1:

2−When checking right hand side of foo with expected type

1+Syntax.idr:6:7-9:1:When checking right hand side of foo with expected type

32 Nat

54When checking an application of function Prelude.Interfaces.+:

@@ -7,8 +6,7 @@ When checking an application of function Prelude.Interfaces.+:

76 String (Type of "argh")

87 and

98 Nat (Expected type)

10−SyntaxTest.idr:5:7-6:1:

11−When checking right hand side of foo with expected type

9+SyntaxTest.idr:5:7-6:1:When checking right hand side of foo with expected type

1210 Nat

1311

1412When checking an application of function Prelude.Interfaces.+:

test/totality001/expected+3−6

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

1−test010.idr:15:1:

2−Main.foo is possibly not total due to: Main.MkBad

3−test010a.idr:9:1:

4−main.bar is possibly not total due to: main.MkBad

5−test010b.idr:9:1:

6−main.bar is possibly not total due to: main.MkBad

1+test010.idr:15:1:Main.foo is possibly not total due to: Main.MkBad

2+test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad

3+test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad

test/totality002/expected+1−2

@@ -2,5 +2,4 @@ test017.idr:94:26-31:

22This style of tactic proof is deprecated. See %runElab for the replacement.

33test017a.idr:7:1:

44scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

5−test017b.idr:4:1:

6−foo.foo is possibly not total due to recursive path foo.foo

5+test017b.idr:4:1:foo.foo is possibly not total due to recursive path foo.foo

test/totality004/expected+1−2

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

11[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]

22totality004a.idr:13:1:

33Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

4−totality004a.idr:24:1:

5−Main.main is possibly not total due to: Main.process

4+totality004a.idr:24:1:Main.main is possibly not total due to: Main.process

test/totality006/expected+1−2

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

1−totality006.idr:8:1:

2−Main.prf is not total as there are missing cases

1+totality006.idr:8:1:Main.prf is not total as there are missing cases

32totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case

43totality006b.idr:10:1:

54totality006b.blargh is not total as there are missing cases

test/totality008/expected+1−2

@@ -1,2 +1 @@

1−totality008.idr:7:1:

2−Main.ElimT is possibly not total due to: Main.C2

1+totality008.idr:7:1:Main.ElimT is possibly not total due to: Main.C2

test/totality010/expected+2−4

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

1−totality010.idr:27:1:

2−Main.evenNotS is not total as there are missing cases

3−totality010.idr:30:1:

4−Main.bad is possibly not total due to: Main.evenNotS

1+totality010.idr:27:1:Main.evenNotS is not total as there are missing cases

2+totality010.idr:30:1:Main.bad is possibly not total due to: Main.evenNotS

test/totality015/expected+2−4

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

11totality015a.idr:52:3:

22Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz

3−totality015a.idr:42:3:

4−Main.correct is possibly not total due to: Main.quiz

5−totality015a.idr:47:3:

6−Main.wrong is possibly not total due to: Main.quiz

3+totality015a.idr:42:3:Main.correct is possibly not total due to: Main.quiz

4+totality015a.idr:47:3:Main.wrong is possibly not total due to: Main.quiz