Fix a few tests

Author: augustepoiroux

test/all_tactics-20250622.expected.out

@@ -3,6 +3,7 @@
    "tactic": "exact hp",
    "proofState": 0,
    "pos": {"line": 2, "column": 2},
+   "parentDecl": "_example",
    "goals": "P : Prop\nhp : P\n⊢ P",
    "endPos": {"line": 2, "column": 10}}],
  "env": 0}

test/app_type_mismatch2.expected.out

@@ -42,6 +42,8 @@
  "proofState": 5,
  "goals": ["case succ\nn✝ : Nat\n⊢ true = true"]}
 
-{"message":
- "Lean error:\ntactic 'apply' failed, could not unify the type of `?succ`\n  n✝ + 1 = 0\nwith the goal\n  true = true\nn✝ : Nat\n⊢ true = true"}
+{"proofStatus":
+ "Error: kernel type check failed: (kernel) application type mismatch\n  @Eq.ndrec Nat (n✝ + 1) (fun x => x = 0)\n    (have this := of_decide_eq_true (id (Eq.refl true));\n    of_decide_eq_true (id (Eq.refl true)))\nargument has type\n  true = true\nbut function has type\n  (fun x => x = 0) (n✝ + 1) → ∀ {b : Nat}, n✝ + 1 = b → (fun x => x = 0) b",
+ "proofState": 6,
+ "goals": []}
 

test/by_cases.expected.out

@@ -23,5 +23,5 @@
 
 {"proofStatus": "Incomplete: open goals remain",
  "proofState": 3,
- "goals": ["x : Int\nh : ¬x < 0\n⊢ x = x", "x : Int\nh : x < 0\n⊢ x = x"]}
+ "goals": ["x : Int\nh : x < 0\n⊢ x = x", "x : Int\nh : ¬x < 0\n⊢ x = x"]}
 

test/file2.expected.out

@@ -17,6 +17,7 @@
    "tactic": "rw [Nat.add_assoc, Nat.add_comm y, h1]",
    "proofState": 0,
    "pos": {"line": 7, "column": 2},
+   "parentDecl": "h",
    "goals": "x y z : Nat\n⊢ x + y + (z + a) = x + (z + b + y)",
    "endPos": {"line": 7, "column": 40}}],
  "env": 0}

test/line_breaks.expected.out

@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 2, "column": 0},
-   "goal": "⊢ 1 = 1",
+   "parentDecl": "foo",
+   "goals": ["⊢ 1 = 1"],
    "endPos": {"line": 2, "column": 5}}],
  "messages":
  [{"severity": "warning",

test/line_breaks.in

@@ -1,5 +1,5 @@
 {"cmd": "theorem foo : 1 = 1 := by\n
-sorry"}
+sorry", "sorries": "individual"}
 
 {"cmd": "theorem bar : 1 = 1 := by\n
 /- Some long comment here -/\n

test/sketch_file.expected.out

@@ -3,10 +3,10 @@
    "pos": {"line": 1, "column": 70},
    "parentDecl": "add_comm_proved_formal_sketch",
    "goals":
-   ["m : Nat\n⊢ 0 + m = m",
+   ["m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m",
     "m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0",
     "m n : Nat\nih : n + m = m + n\n⊢ n + 1 + m = m + (n + 1)",
-    "m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m"],
+    "m : Nat\n⊢ 0 + m = m"],
    "endPos": {"line": 8, "column": 24}},
   {"proofState": 1,
    "pos": {"line": 11, "column": 49},
@@ -18,10 +18,6 @@
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 37},
    "data": "declaration uses 'sorry'"},
-  {"severity": "info",
-   "pos": {"line": 10, "column": 0},
-   "endPos": {"line": 10, "column": 62},
-   "data": "Goals accomplished!"},
   {"severity": "warning",
    "pos": {"line": 11, "column": 8},
    "endPos": {"line": 11, "column": 16},
@@ -33,17 +29,17 @@
  "goals":
  ["m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0",
   "m n : Nat\nih : n + m = m + n\n⊢ n + 1 + m = m + (n + 1)",
-  "m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m"]}
+  "m : Nat\n⊢ 0 + m = m"]}
 
 {"proofStatus": "Incomplete: open goals remain",
  "proofState": 3,
  "goals":
  ["m n : Nat\nih : n + m = m + n\n⊢ n + 1 + m = m + (n + 1)",
-  "m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m"]}
+  "m : Nat\n⊢ 0 + m = m"]}
 
 {"proofStatus": "Incomplete: open goals remain",
  "proofState": 4,
- "goals": ["m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m"]}
+ "goals": ["m : Nat\n⊢ 0 + m = m"]}
 
 {"proofStatus": "Completed", "proofState": 5, "goals": []}
 

test/sketch_file.in

@@ -1,11 +1,11 @@
 {"path": "test/sketch_file.lean", "sorries": "grouped"}
 
-{"tactic": "apply Nat.zero_add", "proofState": 0}
+{"tactic": "apply Nat.add_zero", "proofState": 0}
 
 {"tactic": "rw [h_base, h_symm]", "proofState": 2}
 
 {"tactic": "rw [Nat.succ_add, Nat.add_succ, ih]", "proofState": 3}
 
-{"tactic": "apply Nat.add_zero", "proofState": 4}
+{"tactic": "apply Nat.zero_add", "proofState": 4}
 
 {"tactic": "(\nintros; rfl)", "proofState": 1}

test/sketch_tactic.expected.out

@@ -14,25 +14,27 @@
 {"proofStatus": "Incomplete: open goals remain",
  "proofState": 1,
  "goals":
- ["m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0",
-  "m n : Nat\nih : n + m = m + n\n⊢ n + 1 + m = m + (n + 1)",
+ ["m n : Nat\nih : n + m = m + n\n⊢ n + 1 + m = m + (n + 1)",
+  "m : Nat\n⊢ 0 + m = m",
   "m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m",
-  "m : Nat\n⊢ 0 + m = m"]}
+  "m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0"]}
 
 {"proofStatus": "Incomplete: open goals remain",
  "proofState": 2,
  "goals":
- ["m n : Nat\nih : n + m = m + n\n⊢ n + 1 + m = m + (n + 1)",
+ ["m : Nat\n⊢ 0 + m = m",
   "m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m",
-  "m : Nat\n⊢ 0 + m = m"]}
+  "m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0"]}
 
 {"proofStatus": "Incomplete: open goals remain",
  "proofState": 3,
- "goals": ["m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m", "m : Nat\n⊢ 0 + m = m"]}
+ "goals":
+ ["m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m",
+  "m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0"]}
 
 {"proofStatus": "Incomplete: open goals remain",
  "proofState": 4,
- "goals": ["m : Nat\n⊢ 0 + m = m"]}
+ "goals": ["m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0"]}
 
 {"proofStatus": "Completed", "proofState": 5, "goals": []}
 

test/sketch_tactic.in

@@ -2,11 +2,10 @@
 
 {"tactic": "(\n   intros n m\n   induction n with\n   | zero =>\n     have h_base: 0 + m = m := sorry\n     have h_symm: m + 0 = m := sorry\n     sorry\n   | succ n ih => sorry)", "proofState": 0}
 
-{"tactic": "rw [h_base, h_symm]", "proofState": 1}
+{"tactic": "rw [Nat.succ_add, Nat.add_succ, ih]", "proofState": 1}
 
-{"tactic": "rw [Nat.succ_add, Nat.add_succ, ih]", "proofState": 2}
+{"tactic": "apply Nat.zero_add", "proofState": 2}
 
 {"tactic": "apply Nat.add_zero", "proofState": 3}
 
-{"tactic": "apply Nat.zero_add", "proofState": 4}
-
+{"tactic": "rw [h_base, h_symm]", "proofState": 4}