8cc2312 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't let tests depend on colouring.

commit8cc23127151274d5a64b22898aabdaf0861752e4 authorNiklas Larsson <niklas@mm.st> dateWed 1 Apr 2015, 20:50 (12 years ago) parent663c401

22 files changed+58−58

compare with master

unifiedsplit

test/proof007/expected+1−1

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

11DefaultArgUnknownName.idr:9:6:

22When elaborating right hand side of test:

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

3+When elaborating argument arg to function DefaultArgUnknownName.funWithBadDefArg:

44 No such variable sadgjhsag

test/proof007/run+1−1

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

11#!/usr/bin/env bash

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

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

33rm -f *.ibc

test/reg023/expected+2−2

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

11reg023.idr:7:5:When elaborating right hand side of bad:

22Can't unify

3− [94mNat[0m (Type of [91m0[0m)

3+ Nat (Type of 0)

44with

5− [92mf[0m [94mNat[0m (Expected type)

5+ f Nat (Expected type)

test/reg023/run+1−1

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

11#!/usr/bin/env bash

2−idris --consolewidth 80 $@ reg023.idr --check

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

33rm -f *.ibc

test/reg034/expected+2−2

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

11reg034.idr:6:5:When elaborating left hand side of bar:

2−Can't match on bar xs xs [91mRefl[0m

2+Can't match on bar xs xs Refl

33reg034.idr:9:5:When elaborating left hand side of foo:

4−Can't match on foo f x x [91mRefl[0m

4+Can't match on foo f x x Refl

test/reg034/run+1−1

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

11#!/usr/bin/env bash

2−idris --consolewidth 80 --check reg034.idr

2+idris --nocolour --consolewidth 80 --check reg034.idr

33rm -f reg034 *.ibc

test/reg035/expected+2−2

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

11reg035b.idr:8:6:Can't convert

2− [94mAdditive[0m -> [94mNat[0m

2+ Additive -> Nat

33with

4− [94mFin[0m [91m0[0m

4+ Fin 0

test/reg035/run+3−3

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

11#!/usr/bin/env bash

2−idris --consolewidth 80 --check reg035.idr

3−idris --consolewidth 80 --check reg035a.lidr

4−idris --consolewidth 80 --check reg035b.idr

2+idris --nocolour --consolewidth 80 --check reg035.idr

3+idris --nocolour --consolewidth 80 --check reg035a.lidr

4+idris --nocolour --consolewidth 80 --check reg035b.idr

55rm -f *.ibc

test/reg044/expected+4−4

@@ -1,11 +1,11 @@

11reg044.idr:4:4:When elaborating right hand side of Main.pf:

22Can't unify

3− [95mb[0m [94m=[0m [95mb[0m (Type of [91mRefl[0m)

3+ b = b (Type of Refl)

44with

5− [95ma[0m [94m=[0m [95mb[0m (Expected type)

5+ a = b (Expected type)

77Specifically:

88 Can't unify

9− [95mb[0m

9+ b

1010 with

11− [95ma[0m

11+ a

test/reg044/run+1−1

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

11#!/usr/bin/env bash

2−idris --consolewidth 80 reg044.idr --check

2+idris --nocolour --consolewidth 80 reg044.idr --check

33rm -f *.ibc

test/reg054/expected+4−4

@@ -1,10 +1,10 @@

11reg054.idr:18:5:When elaborating left hand side of inf:

2−When elaborating an application of constructor [91mMain.MkInfer[0m:

2+When elaborating an application of constructor Main.MkInfer:

33 Attempting concrete match on polymorphic argument: 0

44reg054.idr:34:7:When elaborating left hand side of weird:

5−When elaborating argument [95mx[0m to Main.weird:

5+When elaborating argument x to Main.weird:

66 No explicit types on left hand side: Char

77reg054.idr:37:9:Can't convert

8− [94mMaybe[0m a1

8+ Maybe a1

99with

10− [95ma[0m

10+ a

test/reg054/run+1−1

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

11#!/usr/bin/env bash

2−idris --consolewidth 80 $@ reg054.idr --check

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

test/reg055/expected+3−3

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

11reg055.idr:5:3:When elaborating left hand side of g:

2−Can't match on g ([92mf[0m [91m0[0m)

2+Can't match on g (f 0)

33reg055.idr:8:3:When elaborating left hand side of h:

44Can't match on h x x

55reg055a.idr:8:5:When elaborating left hand side of foo:

6−When elaborating an application of constructor [91mFoo.CAny[0m:

6+When elaborating an application of constructor Foo.CAny:

77 Attempting concrete match on polymorphic argument: Nothing

88reg055a.idr:13:7:When elaborating left hand side of Foo.apply:

9−Can't match on apply (\[95mx[0m => \[95my[0m => [95mx[0m) a

9+Can't match on apply (\x => \y => x) a

test/reg055/run+2−2

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

11#!/usr/bin/env bash

2−idris --consolewidth 80 $@ reg055.idr --check

3−idris --consolewidth 80 $@ reg055a.idr --check

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

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

44rm -f *.ibc

test/tutorial006/expected+9−9

@@ -1,24 +1,24 @@

11tutorial006a.idr:5:23:When elaborating right hand side of vapp:

2−When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::[0m:

2+When elaborating argument xs to constructor Data.VectType.Vect.:::

33 Can't unify

4− [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m (Type of vapp [95mxs[0m [95mxs[0m)

4+ Vect (n + n) a (Type of vapp xs xs)

55 with

6− [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m (Expected type)

6+ Vect (plus n m) a (Expected type)

88 Specifically:

99 Can't unify

10− [92mplus[0m [95mn[0m [95mn[0m

10+ plus n n

1111 with

12− [92mplus[0m [95mn[0m [95mm[0m

12+ plus n m

1313tutorial006b.idr:10:10:

1414When elaborating right hand side of with block in Main.parity:

1515Can't unify

16− [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)) (Type of [91meven[0m)

16+ Parity (plus (S j) (S j)) (Type of even)

1717with

18− [94mParity[0m ([91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))) (Expected type)

18+ Parity (S (S (plus j j))) (Expected type)

1919

2020Specifically:

2121 Can't unify

22− [92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)

22+ plus (S j) (S j)

2323 with

24− [91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))

24+ S (S (plus j j))

test/tutorial006/run+2−2

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

11#!/usr/bin/env bash

2−idris --consolewidth 80 $@ tutorial006a.idr --check

3−idris --consolewidth 80 $@ tutorial006b.idr --check

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

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

44rm -f *.ibc

test/unique001/expected+6−6

@@ -3,17 +3,17 @@

3338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

4438,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

55unique001a.idr:33:11:Can't convert

6− [94mInt[0m -> [94mString[0m

6+ Int -> String

77with

8− UniqueType ([94mInt[0m -> [94mString[0m)

8+ UniqueType (Int -> String)

99unique001a.idr:44:12:Can't convert

10− [94mInt[0m -> [94mString[0m

10+ Int -> String

1111with

12− UniqueType ([94mInt[0m -> [94mString[0m)

12+ UniqueType (Int -> String)

1313unique001a.idr:55:12:Can't convert

14− UniqueType ([94mInt[0m -> [94mString[0m)

14+ UniqueType (Int -> String)

1515with

16− [94mInt[0m -> [94mString[0m

16+ Int -> String

1717unique001b.idr:16:7:Borrowed name xs must not be used on RHS

1818unique001c.idr:46:6:Unique name f is used more than once

1919unique001d.idr:3:7:Borrowed name x must not be used on RHS

test/unique001/run+6−6

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

11#!/usr/bin/env bash

2−idris --consolewidth 80 $@ unique001.idr -o unique001

2+idris --nocolour --consolewidth 80 $@ unique001.idr -o unique001

33./unique001

4−idris --consolewidth 80 $@ unique001a.idr --check

5−idris --consolewidth 80 $@ unique001b.idr --check

6−idris --consolewidth 80 $@ unique001c.idr --check

7−idris --consolewidth 80 $@ unique001d.idr --check

8−idris --consolewidth 80 $@ unique001e.idr --check

4+idris --nocolour --consolewidth 80 $@ unique001a.idr --check

5+idris --nocolour --consolewidth 80 $@ unique001b.idr --check

6+idris --nocolour --consolewidth 80 $@ unique001c.idr --check

7+idris --nocolour --consolewidth 80 $@ unique001d.idr --check

8+idris --nocolour --consolewidth 80 $@ unique001e.idr --check

99rm -f unique001 *.ibc

test/unique002/expected+2−2

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

11unique002.idr:15:5:Unique name xs is used more than once

22unique002a.idr:15:5:Can't convert

3− [94mInt[0m -> [94mString[0m

3+ Int -> String

44with

5− UniqueType ([94mInt[0m -> [94mString[0m)

5+ UniqueType (Int -> String)

test/unique002/run+2−2

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

11#!/usr/bin/env bash

2−idris --consolewidth 80 $@ unique002.idr --check

3−idris --consolewidth 80 $@ unique002a.idr --check

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

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

44rm -f *.ibc

test/unique003/expected+2−2

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

11unique003.idr:18:5:Can't convert

2− [94mInt[0m -> [94mString[0m

2+ Int -> String

33with

4− UniqueType ([94mInt[0m -> [94mString[0m)

4+ UniqueType (Int -> String)

test/unique003/run+1−1

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

11#!/usr/bin/env bash

2−idris --consolewidth 80 $@ unique003.idr --check

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

33rm -f *.ibc