Skip to content

Commit 92bc0f9

Browse files
RexWzhRexWzh
committed
add tests for tactic mode
1 parent 656cb12 commit 92bc0f9

File tree

8 files changed

+167
-0
lines changed

8 files changed

+167
-0
lines changed

‎test/Mathlib/test/discardCmd.expected.out‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
{"env": 0}
2+
3+
{"sorries":
4+
[{"proofState": 0,
5+
"pos": {"line": 1, "column": 93},
6+
"goal": "⊢ (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0",
7+
"endPos": {"line": 1, "column": 98}}],
8+
"messages":
9+
[{"severity": "warning",
10+
"pos": {"line": 1, "column": 8},
11+
"endPos": {"line": 1, "column": 30},
12+
"data": "declaration uses 'sorry'"}],
13+
"env": 1}
14+
15+
{"proofStatus": "Completed", "proofState": 1, "goals": []}
16+
17+
{"sorries":
18+
[{"proofState": 2,
19+
"pos": {"line": 1, "column": 93},
20+
"goal": "⊢ (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0",
21+
"endPos": {"line": 1, "column": 98}}],
22+
"messages":
23+
[{"severity": "warning",
24+
"pos": {"line": 1, "column": 8},
25+
"endPos": {"line": 1, "column": 30},
26+
"data": "declaration uses 'sorry'"}]}
27+
28+
{"proofStatus": "Completed", "proofState": 3, "goals": []}
29+

‎test/Mathlib/test/discardCmd.in‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
{"cmd": "import Mathlib"}
2+
3+
{"cmd": "theorem mathd_numbertheory_345 : (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0 := sorry", "env":0}
4+
5+
{"tactic": "norm_num", "proofState": 0}
6+
7+
{"cmd": "theorem mathd_numbertheory_345 : (2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) % 7 = 0 := sorry", "env":0, "discardCmd": true}
8+
9+
{"tactic": "norm_num", "proofState": 2}

‎test/discardCmd.expected.out‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
{"env": 0}
2+
3+
{"messages":
4+
[{"severity": "info",
5+
"pos": {"line": 1, "column": 0},
6+
"endPos": {"line": 1, "column": 5},
7+
"data": "true"}]}
8+
9+
{"message": "Unknown environment."}
10+
11+
{"messages":
12+
[{"severity": "info",
13+
"pos": {"line": 1, "column": 0},
14+
"endPos": {"line": 1, "column": 5},
15+
"data": "37"}],
16+
"env": 1}
17+

‎test/discardCmd.in‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
{"cmd": "def f := 37"}
2+
3+
{"cmd": "#eval true", "discardCmd": true}
4+
5+
{"cmd": "#eval false", "env":1}
6+
7+
{"cmd": "#eval f", "env":0}

‎test/discardCmd2.expected.out‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
{"messages":
2+
[{"severity": "error",
3+
"pos": {"line": 1, "column": 20},
4+
"endPos": null,
5+
"data": "unexpected end of input; expected '{'"},
6+
{"severity": "error",
7+
"pos": {"line": 1, "column": 18},
8+
"endPos": {"line": 1, "column": 20},
9+
"data": "unsolved goals\n⊢ 2 = 2"}],
10+
"env": 0}
11+
12+
{"messages":
13+
[{"severity": "info",
14+
"pos": {"line": 1, "column": 0},
15+
"endPos": {"line": 2, "column": 3},
16+
"data": "Goals accomplished!"}],
17+
"env": 1}
18+
19+
{"messages":
20+
[{"severity": "error",
21+
"pos": {"line": 1, "column": 66},
22+
"endPos": null,
23+
"data": "unexpected end of input; expected '{'"},
24+
{"severity": "error",
25+
"pos": {"line": 1, "column": 64},
26+
"endPos": {"line": 1, "column": 66},
27+
"data": "unsolved goals\nP Q R : Prop\n⊢ (P → Q) → (Q → R) → P → R"}]}
28+
29+
{"messages":
30+
[{"severity": "error",
31+
"pos": {"line": 1, "column": 64},
32+
"endPos": {"line": 2, "column": 13},
33+
"data": "unsolved goals\nP Q R : Prop\nh1 : P → Q\nh2 : Q → R\np : P\n⊢ R"}]}
34+
35+
{"messages":
36+
[{"severity": "info",
37+
"pos": {"line": 3, "column": 0},
38+
"endPos": {"line": 3, "column": 6},
39+
"data": "Try this: exact h2 (h1 p)"},
40+
{"severity": "info",
41+
"pos": {"line": 1, "column": 0},
42+
"endPos": {"line": 3, "column": 6},
43+
"data": "Goals accomplished!"}]}
44+

‎test/discardCmd2.in‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
{"cmd": "example : 2=2 := by"}
2+
3+
{"cmd": "example : 2=2 := by\nrfl"}
4+
5+
{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by", "discardCmd": true}
6+
7+
{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by\nintro h1 h2 p", "discardCmd": true}
8+
9+
{"cmd": "theorem gc_demo (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by\nintro h1 h2 p\napply?", "discardCmd": true}

‎test/discardCmd_proof.expected.out‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
{"sorries":
2+
[{"proofState": 0,
3+
"pos": {"line": 1, "column": 20},
4+
"goal": "⊢ 1 = 1",
5+
"endPos": {"line": 1, "column": 25}}],
6+
"messages":
7+
[{"severity": "warning",
8+
"pos": {"line": 1, "column": 0},
9+
"endPos": {"line": 1, "column": 7},
10+
"data": "declaration uses 'sorry'"}]}
11+
12+
{"sorries":
13+
[{"proofState": 1,
14+
"pos": {"line": 1, "column": 20},
15+
"goal": "⊢ 1 = 1",
16+
"endPos": {"line": 1, "column": 25}}],
17+
"messages":
18+
[{"severity": "warning",
19+
"pos": {"line": 1, "column": 0},
20+
"endPos": {"line": 1, "column": 7},
21+
"data": "declaration uses 'sorry'"}],
22+
"env": 0}
23+
24+
{"sorries":
25+
[{"proofState": 2,
26+
"pos": {"line": 1, "column": 20},
27+
"goal": "⊢ 1 = 1",
28+
"endPos": {"line": 1, "column": 25}}],
29+
"messages":
30+
[{"severity": "warning",
31+
"pos": {"line": 1, "column": 0},
32+
"endPos": {"line": 1, "column": 7},
33+
"data": "declaration uses 'sorry'"}],
34+
"env": 1}
35+
36+
{"proofStatus": "Completed", "proofState": 3, "goals": []}
37+
38+
{"proofStatus": "Completed", "proofState": 4, "goals": []}
39+
40+
{"proofStatus": "Completed", "proofState": 5, "goals": []}
41+

‎test/discardCmd_proof.in‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{"cmd": "example : 1=1 := by sorry", "discardCmd": true}
2+
3+
{"cmd": "example : 1=1 := by sorry", "discardCmd": false}
4+
5+
{"cmd": "example : 1=1 := by sorry"}
6+
7+
{"tactic": "rfl", "proofState": 0}
8+
9+
{"tactic": "rfl", "proofState": 1}
10+
11+
{"tactic": "rfl", "proofState": 2}

0 commit comments

Comments
 (0)