Update tests for proof deprecation
commit752a2fcc77f555148d404a7ee496edb898f20d31
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateThu 10 Sep 2015, 12:01 (11 years ago)
parentf4bcbbc
src/Idris/ParseHelpers.hs+2−1
@@ -100,7 +100,8 @@ reportParserWarnings = do ist <- getIState
100100 mapM_ (uncurry iWarn)
101101 (map (\ (fc, err) -> (fc, pprintErr ist err)) .
102102 reverse .
103− nub $
103+ nubBy (\(fc, err) (fc', err') ->
104+ FC' fc == FC' fc' && err == err') $
104105 parserWarnings ist)
105106 clearParserWarnings
106107
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.
15[False, True, False, True, False, True]
test/basic002/run+1−1
@@ -1,4 +1,4 @@
11#!/usr/bin/env bash
2−idris $@ test006.idr -o test006
2+idris $@ --nocolour --consolewidth 80 test006.idr -o test006
33./test006
44rm -f test006 test006.ibc
test/docs003/expected+1
@@ -15,6 +15,7 @@ Instances:
1515 Functor Stream
1616 Functor Provider
1717 Functor Binder
18+ Functor Elab
1819 Functor PrimIO
1920 Functor Maybe
2021 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.
13------------
24
356 guesses left
test/effects003/hangman.idr+4
@@ -223,3 +223,7 @@ were caught by the type checker:
223223
224224main : IO ()
225225main = run runGame
226+
227+-- Local Variables:
228+-- idris-load-packages: ("effects")
229+-- End:
test/effects003/run+1−1
@@ -1,4 +1,4 @@
11#!/usr/bin/env bash
2−idris $@ hangman.idr -p effects -o hangman
2+idris $@ hangman.idr --consolewidth 80 --nocolour -p effects -o hangman
33./hangman < input
44rm -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 @@
11#!/usr/bin/env bash
2−idris $@ test029.idr --check test029
2+idris $@ test029.idr --consolewidth 80 --nocolour --check test029
33rm -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.
17test030a.idr:12:26-14:1:
28When checking right hand side of testReflect1:
39When 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.
11300101010
21401011001
315010000011
test/proof003/run+1−1
@@ -1,4 +1,4 @@
11#!/usr/bin/env bash
2−idris $@ test015.idr -o test015
2+idris $@ test015.idr --nocolour --consolewidth 80 -o test015
33./test015
44rm -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 @@
11#!/usr/bin/env bash
2−idris --check $@ ClaimAndUnfocus.idr
2+idris --nocolour --consolewidth 80 --check $@ ClaimAndUnfocus.idr
33rm -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.
12
23
34---------- 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.
17Quasiquote004.idr:50:25:
28When checking right hand side of Quasiquote004.getMeNat':
39Not 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.
154
test/reg017/run+1−1
@@ -1,4 +1,4 @@
11#!/usr/bin/env bash
2−idris $@ reg017.idr -o reg017
2+idris $@ --nocolour --consolewidth 80 reg017.idr -o reg017
33./reg017
44rm -f reg017 *.ibc
test/reg028/expected+2
@@ -1,4 +1,6 @@
11reg028.idr:5:1:
22tbad.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.
35reg028a.idr:11:1:
46tbad.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.
13reg044.idr:4:4:When checking right hand side of Main.pf:
24Type mismatch between
35 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.
19Testing using definition
210FileLoc "SourceLoc.idr" (16, 11) (16, 17)
311Testing using inline tactics
test/sourceLocation001/run+1−1
@@ -1,4 +1,4 @@
11#!/usr/bin/env bash
2−idris $@ SourceLoc.idr -o sourceLocation001
2+idris $@ --nocolour --consolewidth 80 SourceLoc.idr -o sourceLocation001
33./sourceLocation001
44rm -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.
13test017a.idr:7:1:
24scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans
35test017b.idr:4:1:
test/totality003/run+2−2
@@ -1,4 +1,4 @@
11#!/usr/bin/env bash
2−idris --consolewidth 80 $@ totality003.idr --check
3−idris --consolewidth 80 $@ totality003a.idr --check
2+idris --nocolour --consolewidth 80 $@ totality003.idr --check
3+idris --nocolour --consolewidth 80 $@ totality003a.idr --check
44rm -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 @@
11#!/usr/bin/env bash
2−idris $@ tutorial002.idr --check
2+idris $@ --nocolour --consolewidth 80 tutorial002.idr --check
33rm -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 @@
11#!/usr/bin/env bash
2−idris $@ tutorial004.idr --check
2+idris $@ tutorial004.idr --check --nocolour --consolewidth 80
33rm -f *.ibc