752a2fc · Idris-dev · git.iko.soy

src/Idris/ParseHelpers.hs+2−1

compare with master

unifiedsplit

@@ -100,7 +100,8 @@ reportParserWarnings = do ist <- getIState

100 mapM_ (uncurry iWarn)

101 (map (\ (fc, err) -> (fc, pprintErr ist err)) .

102 reverse .

103− nub $

103+ nubBy (\(fc, err) (fc', err') ->

104+ FC' fc == FC' fc' && err == err') $

104 parserWarnings ist)

105 parserWarnings ist)

105 clearParserWarnings

106 clearParserWarnings

106

107

test/basic002/expected+4

@@ -1 +1,5 @@

1+test006.idr:25:23-28:

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

3+test006.idr:32:23-28:

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

1[False, True, False, True, False, True]

5[False, True, False, True, False, True]

test/basic002/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ test006.idr -o test006

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

3./test006

4rm -f test006 test006.ibc

test/docs003/expected+1

@@ -15,6 +15,7 @@ Instances:

15 Functor Stream

16 Functor Provider

17 Functor Binder

18+ Functor Elab

18 Functor PrimIO

19 Functor PrimIO

19 Functor Maybe

20 Functor Maybe

20 Functor (Either e)

21 Functor (Either e)

test/effects003/expected+2

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

1+hangman.idr:204:8-13:

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

1------------

3------------

2

4

36 guesses left

56 guesses left

test/effects003/hangman.idr+4

@@ -223,3 +223,7 @@ were caught by the type checker:

223

224main : IO ()

225main = run runGame

226+

227+-- Local Variables:

228+-- idris-load-packages: ("effects")

229+-- End:

test/effects003/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ hangman.idr -p effects -o hangman

2+idris $@ hangman.idr --consolewidth 80 --nocolour -p effects -o hangman

3./hangman < input

4rm -f hangman *.ibc

test/proof001/expected+4

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

1+test029.idr:29:25-30:

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

3+test029.idr:36:25-30:

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

test/proof001/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ test029.idr --check test029

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

3rm -f *.ibc

test/proof002/expected+6

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

1+Reflect.idr:173:21-26:

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

3+Reflect.idr:182:21-26:

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

5+Reflect.idr:190:15-20:

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

1test030a.idr:12:26-14:1:

7test030a.idr:12:26-14:1:

2When checking right hand side of testReflect1:

8When checking right hand side of testReflect1:

3When checking an application of function Reflect.getJust:

9When checking an application of function Reflect.getJust:

test/proof003/expected+12

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

1+Parity.idr:15:18-23:

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

3+Parity.idr:22:18-23:

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

5+test015.idr:88:15-20:

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

7+test015.idr:97:16-21:

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

9+test015.idr:108:20-25:

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

11+test015.idr:136:20-25:

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

100101010

1300101010

201011001

1401011001

3010000011

15010000011

test/proof003/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ test015.idr -o test015

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

3./test015

4rm -f test015 Parity.ibc test015.ibc

test/proof008/expected+2

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

1+ClaimAndUnfocus.idr:8:27-32:

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

test/proof008/run+1−1

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

1#!/usr/bin/env bash

2−idris --check $@ ClaimAndUnfocus.idr

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

3rm -f *.ibc

test/proof009/expected+1

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

1+Warning: this interactive prover is deprecated and will be removed in a future release. Please see :elab for a similar feature that will replace it.

1

2

3

3---------- Goal: ----------

4---------- Goal: ----------

test/quasiquote004/expected+6

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

1+Quasiquote004.idr:39:26-31:

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

3+Quasiquote004.idr:42:28-33:

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

5+Quasiquote004.idr:50:27-32:

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

1Quasiquote004.idr:50:25:

7Quasiquote004.idr:50:25:

2When checking right hand side of Quasiquote004.getMeNat':

8When checking right hand side of Quasiquote004.getMeNat':

3Not a Nat goal

9Not a Nat goal

test/reg017/expected+4

@@ -1 +1,5 @@

1+reg017.idr:5:17-24:

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

3+reg017.idr:8:17-24:

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

14

54

test/reg017/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ reg017.idr -o reg017

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

3./reg017

4rm -f reg017 *.ibc

test/reg028/expected+2

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

1reg028.idr:5:1:

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

3+reg028a.idr:17:14-19:

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

3reg028a.idr:11:1:

5reg028a.idr:11:1:

4tbad.qsort' is possibly not total due to: with block in tbad.qsort'

6tbad.qsort' is possibly not total due to: with block in tbad.qsort'

test/reg044/expected+2

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

1+reg044.idr:4:6-11:

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

1reg044.idr:4:4:When checking right hand side of Main.pf:

3reg044.idr:4:4:When checking right hand side of Main.pf:

2Type mismatch between

4Type mismatch between

3 b = b (Type of Refl)

5 b = b (Type of Refl)

test/sourceLocation001/expected+8

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

1+SourceLoc.idr:11:19-26:

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

3+SourceLoc.idr:20:19-24:

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

5+SourceLoc.idr:40:20-27:

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

7+SourceLoc.idr:98:18-23:

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

1Testing using definition

9Testing using definition

2FileLoc "SourceLoc.idr" (16, 11) (16, 17)

10FileLoc "SourceLoc.idr" (16, 11) (16, 17)

3Testing using inline tactics

11Testing using inline tactics

test/sourceLocation001/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ SourceLoc.idr -o sourceLocation001

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

3./sourceLocation001

4rm -f sourceLocation001 *.ibc

test/totality002/expected+2

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

1+test017.idr:94:26-31:

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

1test017a.idr:7:1:

3test017a.idr:7:1:

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

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

3test017b.idr:4:1:

5test017b.idr:4:1:

test/totality003/run+2−2

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

1#!/usr/bin/env bash

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

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

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

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

4rm -f *.ibc

test/tutorial002/expected+6

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

1+tutorial002.idr:41:25-30:

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

3+tutorial002.idr:48:18-23:

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

5+tutorial002.idr:54:18-23:

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

test/tutorial002/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ tutorial002.idr --check

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

3rm -f *.ibc

test/tutorial004/expected+4

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

1+tutorial004.idr:46:14-19:

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

3+tutorial004.idr:53:14-19:

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

test/tutorial004/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ tutorial004.idr --check

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

3rm -f *.ibc