From 89de2e6b6fc47c99fb52ad3ef4c69daaa09792b9 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 4 Jul 2025 12:19:45 +0200 Subject: [PATCH 1/8] Initial implementation --- REPL/JSON.lean | 2 -- REPL/Main.lean | 17 ++++------------- REPL/Snapshots.lean | 35 ++++++++++++++++++++++++++++++++++- 3 files changed, 38 insertions(+), 16 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index ebec4c56..5e7270f4 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -150,7 +150,6 @@ structure ProofStepResponse where proofState : Nat goals : List String messages : List Message := [] - sorries : List Sorry := [] traces : List String proofStatus : String deriving ToJson, FromJson @@ -160,7 +159,6 @@ instance : ToJson ProofStepResponse where [("proofState", r.proofState)], [("goals", toJson r.goals)], Json.nonemptyList "messages" r.messages, - Json.nonemptyList "sorries" r.sorries, Json.nonemptyList "traces" r.traces, [("proofStatus", r.proofStatus)] ] diff --git a/REPL/Main.lean b/REPL/Main.lean index d181080f..39bb3a0d 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -236,22 +236,11 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap let messages := proofState.newMessages old? let messages ← messages.mapM fun m => Message.of m let traces ← proofState.newTraces old? - let trees := proofState.newInfoTrees old? - let trees ← match old? with - | some old => do - let (ctx, _) ← old.runMetaM do return { ← CommandContextInfo.save with } - let ctx := PartialContextInfo.commandCtx ctx - pure <| trees.map fun t => InfoTree.context ctx t - | none => pure trees - -- For debugging purposes, sometimes we print out the trees here: - -- trees.forM fun t => do IO.println (← t.format) - let sorries ← sorries trees none (some proofState.rootGoals) let id ← recordProofSnapshot proofState return { proofState := id - goals := (← proofState.ppGoals).map fun s => s!"{s}" + goals := (← proofState.ppGoals).map (s!"{·}") messages - sorries traces proofStatus := (← getProofStatus proofState) } @@ -350,8 +339,10 @@ def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do /-- Run a single tactic, returning the id of the new proof statement, and the new goals. +This implementation supports branching in tactic proofs. +When a tactic generates new goals, each goal is properly tracked to allow subsequent tactics to be +applied. -/ --- TODO detect sorries? def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error) := do match (← get).proofStates[s.proofState]? with | none => return .inr ⟨"Unknown proof state."⟩ diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index f6936245..8df8b32f 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -114,6 +114,20 @@ namespace ProofSnapshot open Lean Elab Tactic +/-- Transform `sorry` expressions into fresh opaque metavariables, collecting their IDs. -/ +def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := + Meta.transform src λ expr => + if expr.isSorry then do + -- extract the proof type from `sorry` (the first binder argument) + let type ← instantiateMVars (expr.getArg! 0 |>.bindingBody!) + if type.hasSorry then + throwError s!"Nested sorry in type not supported: {← Meta.ppExpr type}" + let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type + modify (mvar.mvarId! :: ·) + pure $ .done mvar + else + pure .continue + /-- New messages in a `ProofSnapshot`, relative to an optional previous `ProofSnapshot`. -/ def newMessages (new : ProofSnapshot) (old? : Option ProofSnapshot := none) : List Lean.Message := match old? with @@ -180,7 +194,26 @@ and run it in the current `ProofSnapshot`. def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot := match Parser.runParserCategory p.coreState.env `tactic t with | .error e => throw (IO.userError e) - | .ok stx => p.runSyntax stx + | .ok stx => do + let result ← p.runSyntax stx + + -- Process all goals after tactic execution to find and transform any sorries + let (newGoals, result') ← result.runMetaM do + let processExpr (acc : List MVarId) (mvarId : MVarId) (expr : Expr) : MetaM (List MVarId) := do + if expr.hasSorry then + let (newExpr, exprHoles) ← sorryToHole expr |>.run [] + mvarId.assign newExpr + pure (acc ++ exprHoles) + else + pure acc + + -- Process all expressions in the metavariable context + let mctx := result.metaState.mctx + let exprHoles ← mctx.eAssignment.foldlM processExpr [] + pure exprHoles + + let combinedGoals := result'.tacticState.goals ++ newGoals + return { result' with tacticState := { goals := combinedGoals } } /-- Pretty print the current goals in the `ProofSnapshot`. -/ def ppGoals (p : ProofSnapshot) : IO (List Format) := From abd91e8f1210b92db65354c260e9ded52c3bc1b7 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 4 Jul 2025 12:19:45 +0200 Subject: [PATCH 2/8] Add missing local context --- REPL/Snapshots.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index 8df8b32f..15eb1679 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -201,9 +201,10 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot := let (newGoals, result') ← result.runMetaM do let processExpr (acc : List MVarId) (mvarId : MVarId) (expr : Expr) : MetaM (List MVarId) := do if expr.hasSorry then - let (newExpr, exprHoles) ← sorryToHole expr |>.run [] - mvarId.assign newExpr - pure (acc ++ exprHoles) + mvarId.withContext do + let (newExpr, exprHoles) ← sorryToHole expr |>.run [] + mvarId.assign newExpr + pure (acc ++ exprHoles) else pure acc From fcfc83ea6ff20fad621563780b3c52d170a9bb5c Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 4 Jul 2025 12:19:46 +0200 Subject: [PATCH 3/8] Update tests --- test/Mathlib/test/20240209.expected.out | 4 +- test/Mathlib/test/induction.expected.out | 9 +-- test/Mathlib/test/on_goal.expected.out | 11 ++-- test/app_type_mismatch2.expected.out | 11 +++- test/app_type_mismatch2.in | 2 + test/auxiliary_declaration.expected.out | 23 ++++++++ test/auxiliary_declaration.in | 8 +++ test/by_cases.expected.out | 9 +-- test/goal_branching.expected.out | 30 ++++++++++ test/goal_branching.in | 11 ++++ test/have_by_sorry.expected.out | 7 +-- test/invalid_tactic.expected.out | 4 +- test/name_generator.expected.out | 71 ++++++++++++------------ test/sorry_hypotheses.expected.out | 7 +-- test/tactic_have_branching.expected.out | 33 +++++++++++ test/tactic_have_branching.in | 12 ++++ test/tactic_mode_sorry.expected.out | 7 +-- 17 files changed, 186 insertions(+), 73 deletions(-) create mode 100644 test/auxiliary_declaration.expected.out create mode 100644 test/auxiliary_declaration.in create mode 100644 test/goal_branching.expected.out create mode 100644 test/goal_branching.in create mode 100644 test/tactic_have_branching.expected.out create mode 100644 test/tactic_have_branching.in diff --git a/test/Mathlib/test/20240209.expected.out b/test/Mathlib/test/20240209.expected.out index b7cfc2da..521f9c7e 100644 --- a/test/Mathlib/test/20240209.expected.out +++ b/test/Mathlib/test/20240209.expected.out @@ -10,12 +10,12 @@ "data": "declaration uses 'sorry'"}], "env": 0} -{"proofStatus": "Incomplete: contains sorry", +{"proofStatus": "Incomplete: open goals remain", "proofState": 1, "messages": [{"severity": "error", "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, "data": "unsolved goals\n⊢ False"}], - "goals": []} + "goals": ["⊢ False"]} diff --git a/test/Mathlib/test/induction.expected.out b/test/Mathlib/test/induction.expected.out index 7f80087a..9b2ca0d0 100644 --- a/test/Mathlib/test/induction.expected.out +++ b/test/Mathlib/test/induction.expected.out @@ -21,10 +21,7 @@ "proofState": 2, "goals": ["case succ\nn✝ : ℕ\na✝ : n✝ = n✝\n⊢ n✝ + 1 = n✝ + 1"]} -{"sorries": - [{"proofState": 3, "goal": "case zero\n⊢ 0 = 0"}, - {"proofState": 4, "goal": "case succ\nx : ℕ\na✝ : x = x\n⊢ x + 1 = x + 1"}], - "proofStatus": "Incomplete: contains sorry", - "proofState": 5, - "goals": []} +{"proofStatus": "Incomplete: open goals remain", + "proofState": 3, + "goals": ["⊢ 0 = 0", "x : ℕ\na✝ : x = x\n⊢ x + 1 = x + 1"]} diff --git a/test/Mathlib/test/on_goal.expected.out b/test/Mathlib/test/on_goal.expected.out index 510cfe1b..108dd0bd 100644 --- a/test/Mathlib/test/on_goal.expected.out +++ b/test/Mathlib/test/on_goal.expected.out @@ -12,12 +12,11 @@ "data": "declaration uses 'sorry'"}], "env": 1} -{"sorries": - [{"proofState": 1, "goal": "x : ℝ\nh0 : |x| > 1\n⊢ x = x"}, - {"proofState": 2, "goal": "x : ℝ\nh0 : |x| > 1\nh1 : x = x\n⊢ x = x"}], - "proofStatus": "Incomplete: open goals remain", - "proofState": 3, +{"proofStatus": "Incomplete: open goals remain", + "proofState": 1, "goals": ["case pos\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : x < 0\n⊢ x < 0 ∨ 2 * x > 2", - "case neg\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : ¬x < 0\n⊢ x < 0 ∨ 2 * x > 2"]} + "case neg\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : ¬x < 0\n⊢ x < 0 ∨ 2 * x > 2", + "x : ℝ\nh0 : |x| > 1\n⊢ x = x", + "x : ℝ\nh0 : |x| > 1\nh1 : x = x\n⊢ x = x"]} diff --git a/test/app_type_mismatch2.expected.out b/test/app_type_mismatch2.expected.out index 23d93247..8cd7c6be 100644 --- a/test/app_type_mismatch2.expected.out +++ b/test/app_type_mismatch2.expected.out @@ -31,10 +31,15 @@ "proofState": 3, "goals": []} -{"sorries": [{"proofState": 4, "goal": "n✝ : Nat\n⊢ true = true"}], - "proofStatus": "Incomplete: open goals remain", +{"proofStatus": "Incomplete: open goals remain", + "proofState": 4, + "goals": + ["case succ\nn✝ : Nat\nthis : true = true\n⊢ n✝ + 1 = 0", + "n✝ : Nat\n⊢ true = true"]} + +{"proofStatus": "Incomplete: open goals remain", "proofState": 5, - "goals": ["case succ\nn✝ : Nat\nthis : true = true\n⊢ n✝ + 1 = 0"]} + "goals": ["n✝ : 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"} diff --git a/test/app_type_mismatch2.in b/test/app_type_mismatch2.in index 2e85827b..47300014 100644 --- a/test/app_type_mismatch2.in +++ b/test/app_type_mismatch2.in @@ -12,3 +12,5 @@ {"tactic": "apply ?succ", "proofState": 4} +{"tactic": "rfl", "proofState": 5} + diff --git a/test/auxiliary_declaration.expected.out b/test/auxiliary_declaration.expected.out new file mode 100644 index 00000000..4fb06d00 --- /dev/null +++ b/test/auxiliary_declaration.expected.out @@ -0,0 +1,23 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 21}, + "goal": "⊢ true = true", + "endPos": {"line": 1, "column": 26}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 0}, + "endPos": {"line": 1, "column": 7}, + "data": "declaration uses 'sorry'"}], + "env": 0} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 1, + "goals": ["p : ∃ x, x > 0 := Exists.intro 1 Nat.one_pos\n⊢ true = true"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 2, + "goals": + ["p : ∃ x, x > 0 := Exists.intro 1 Nat.one_pos\nn : Nat\nhn : n > 0\n⊢ true = true"]} + +{"proofStatus": "Completed", "proofState": 3, "goals": []} + diff --git a/test/auxiliary_declaration.in b/test/auxiliary_declaration.in new file mode 100644 index 00000000..6b26b301 --- /dev/null +++ b/test/auxiliary_declaration.in @@ -0,0 +1,8 @@ +{"cmd": "example : true := by sorry"} + +{"tactic": "let p : ∃ x : Nat, x > 0 := ⟨1, Nat.one_pos⟩", "proofState": 0} + +{"tactic": "let ⟨n, hn⟩ := p", "proofState": 1} + +{"tactic": "rfl", "proofState": 2} + diff --git a/test/by_cases.expected.out b/test/by_cases.expected.out index 978df508..f7b19de6 100644 --- a/test/by_cases.expected.out +++ b/test/by_cases.expected.out @@ -20,10 +20,7 @@ "proofState": 2, "goals": ["case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]} -{"sorries": - [{"proofState": 3, "goal": "case pos\nx : Int\nh : x < 0\n⊢ x = x"}, - {"proofState": 4, "goal": "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"}], - "proofStatus": "Incomplete: contains sorry", - "proofState": 5, - "goals": []} +{"proofStatus": "Incomplete: open goals remain", + "proofState": 3, + "goals": ["x : Int\nh : ¬x < 0\n⊢ x = x", "x : Int\nh : x < 0\n⊢ x = x"]} diff --git a/test/goal_branching.expected.out b/test/goal_branching.expected.out new file mode 100644 index 00000000..cfebf5cf --- /dev/null +++ b/test/goal_branching.expected.out @@ -0,0 +1,30 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 53}, + "goal": "⊢ 1 = 1 ∧ 2 = 2 ∧ 3 = 3", + "endPos": {"line": 1, "column": 58}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 22}, + "data": "declaration uses 'sorry'"}], + "env": 0} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 1, + "goals": ["case left\n⊢ 1 = 1", "case right\n⊢ 2 = 2 ∧ 3 = 3"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 2, + "goals": ["case right\n⊢ 2 = 2 ∧ 3 = 3"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 3, + "goals": ["case right.left\n⊢ 2 = 2", "case right.right\n⊢ 3 = 3"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 4, + "goals": ["case right.right\n⊢ 3 = 3"]} + +{"proofStatus": "Completed", "proofState": 5, "goals": []} + diff --git a/test/goal_branching.in b/test/goal_branching.in new file mode 100644 index 00000000..b6389527 --- /dev/null +++ b/test/goal_branching.in @@ -0,0 +1,11 @@ +{"cmd" : "theorem branching_test : 1 = 1 ∧ 2 = 2 ∧ 3 = 3 := by sorry"} + +{"tactic": "constructor", "proofState": 0} + +{"tactic": "exact rfl", "proofState": 1} + +{"tactic": "constructor", "proofState": 2} + +{"tactic": "exact rfl", "proofState": 3} + +{"tactic": "exact rfl", "proofState": 4} diff --git a/test/have_by_sorry.expected.out b/test/have_by_sorry.expected.out index 03c79017..23f1987e 100644 --- a/test/have_by_sorry.expected.out +++ b/test/have_by_sorry.expected.out @@ -22,8 +22,7 @@ "data": "declaration uses 'sorry'"}], "env": 1} -{"sorries": [{"proofState": 2, "goal": "x : Int\n⊢ x = 1"}], - "proofStatus": "Incomplete: open goals remain", - "proofState": 3, - "goals": ["x : Int\nh : x = 1\n⊢ x = 1"]} +{"proofStatus": "Incomplete: open goals remain", + "proofState": 2, + "goals": ["x : Int\nh : x = 1\n⊢ x = 1", "x : Int\n⊢ x = 1"]} diff --git a/test/invalid_tactic.expected.out b/test/invalid_tactic.expected.out index 3ba2c50f..d22e4698 100644 --- a/test/invalid_tactic.expected.out +++ b/test/invalid_tactic.expected.out @@ -10,12 +10,12 @@ "data": "declaration uses 'sorry'"}], "env": 0} -{"proofStatus": "Incomplete: contains sorry", +{"proofStatus": "Incomplete: open goals remain", "proofState": 1, "messages": [{"severity": "error", "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, "data": "unknown identifier 'my_fake_premise'"}], - "goals": []} + "goals": ["x : Nat\n⊢ x = x"]} diff --git a/test/name_generator.expected.out b/test/name_generator.expected.out index 987d0593..99c81b85 100644 --- a/test/name_generator.expected.out +++ b/test/name_generator.expected.out @@ -10,54 +10,53 @@ "data": "declaration uses 'sorry'"}], "env": 0} -{"sorries": [{"proofState": 1, "goal": "x : Int\nh0 : x > 0\n⊢ x > 0"}], - "proofStatus": "Incomplete: open goals remain", +{"proofStatus": "Incomplete: open goals remain", + "proofState": 1, + "goals": ["x : Int\nh0 h : x > 0\n⊢ False", "x : Int\nh0 : x > 0\n⊢ x > 0"]} + +{"message": + "Lean error:\ntype mismatch\n h0\nhas type\n x > 0 : Prop\nbut is expected to have type\n False : Prop"} + +{"message": + "Lean error:\ntactic 'assumption' failed\nx : Int\nh0 h : x > 0\n⊢ False"} + +{"message": "Lean error:\nsimp made no progress"} + +{"proofStatus": "Incomplete: open goals remain", "proofState": 2, - "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]} + "messages": + [{"severity": "error", + "pos": {"line": 0, "column": 0}, + "endPos": {"line": 0, "column": 0}, + "data": "simp made no progress"}], + "goals": ["x : Int\nh0 : x > 0\n⊢ x > 0", "x : Int\nh0 h : x > 0\n⊢ False"]} -{"proofStatus": "Incomplete: contains metavariable(s)", +{"proofStatus": "Incomplete: open goals remain", "proofState": 3, - "goals": []} + "messages": + [{"severity": "error", + "pos": {"line": 0, "column": 0}, + "endPos": {"line": 0, "column": 0}, + "data": "simp made no progress"}], + "goals": ["x : Int\nh0 : x > 0\n⊢ x > 0", "x : Int\nh0 h : x > 0\n⊢ False"]} -{"proofStatus": "Incomplete: contains metavariable(s)", +{"proofStatus": "Incomplete: open goals remain", "proofState": 4, - "goals": []} - -{"traces": - ["[Meta.Tactic.simp.rewrite] of_eq_true (eq_true h0):1000:\n x > 0\n ==>\n True"], - "proofStatus": "Incomplete: contains metavariable(s)", - "proofState": 5, - "goals": []} - -{"traces": - ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000:\n x > 0\n ==>\n 0 < x", - "[Meta.Tactic.simp.rewrite] h0:1000:\n 0 < x\n ==>\n True"], - "proofStatus": "Incomplete: contains metavariable(s)", - "proofState": 6, - "goals": []} - -{"traces": - ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000:\n x > 0\n ==>\n 0 < x", - "[Meta.Tactic.simp.rewrite] h0:1000:\n 0 < x\n ==>\n True"], - "proofStatus": "Incomplete: contains metavariable(s)", - "proofState": 7, - "goals": []} - -{"proofStatus": "Incomplete: contains metavariable(s)", - "proofState": 8, "messages": [{"severity": "error", "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, - "data": "unsolved goals\nx : Int\nh0 : x > 0\n⊢ x > 0"}], - "goals": []} + "data": + "tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n x\nx : Int\nh0 h : x > 0\n⊢ False"}], + "goals": ["x : Int\nh0 : x > 0\n⊢ x > 0", "x : Int\nh0 h : x > 0\n⊢ False"]} -{"proofStatus": "Incomplete: contains metavariable(s)", - "proofState": 9, +{"proofStatus": "Incomplete: open goals remain", + "proofState": 5, "messages": [{"severity": "error", "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, - "data": "unsolved goals\nx : Int\nh0 : x > 0\n⊢ x > 0"}], - "goals": []} + "data": + "tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n x\nx : Int\nh0 h : x > 0\n⊢ False"}], + "goals": ["x : Int\nh0 : x > 0\n⊢ x > 0", "x : Int\nh0 h : x > 0\n⊢ False"]} diff --git a/test/sorry_hypotheses.expected.out b/test/sorry_hypotheses.expected.out index d59e9b1e..32abd682 100644 --- a/test/sorry_hypotheses.expected.out +++ b/test/sorry_hypotheses.expected.out @@ -10,8 +10,7 @@ "data": "declaration uses 'sorry'"}], "env": 0} -{"sorries": [{"proofState": 1, "goal": "x : Int\n⊢ x = 1"}], - "proofStatus": "Incomplete: open goals remain", - "proofState": 2, - "goals": ["x : Int\nh : x = 1\n⊢ x = x"]} +{"proofStatus": "Incomplete: open goals remain", + "proofState": 1, + "goals": ["x : Int\nh : x = 1\n⊢ x = x", "x : Int\n⊢ x = 1"]} diff --git a/test/tactic_have_branching.expected.out b/test/tactic_have_branching.expected.out new file mode 100644 index 00000000..037d9321 --- /dev/null +++ b/test/tactic_have_branching.expected.out @@ -0,0 +1,33 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 22}, + "goal": "⊢ 1 = 1", + "endPos": {"line": 1, "column": 27}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 0}, + "endPos": {"line": 1, "column": 7}, + "data": "declaration uses 'sorry'"}], + "env": 0} + +{"proofStatus": "Completed", "proofState": 1, "goals": []} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 2, + "goals": ["this : 2 = 2\n⊢ 1 = 1", "⊢ 2 = 2"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 3, + "messages": + [{"severity": "error", + "pos": {"line": 0, "column": 0}, + "endPos": {"line": 0, "column": 0}, + "data": "unknown identifier 'h1'"}], + "goals": ["⊢ 2 = 2", "this : 2 = 2\n⊢ 1 = 1"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 4, + "goals": ["⊢ 2 = 2"]} + +{"proofStatus": "Completed", "proofState": 5, "goals": []} + diff --git a/test/tactic_have_branching.in b/test/tactic_have_branching.in new file mode 100644 index 00000000..c52a042d --- /dev/null +++ b/test/tactic_have_branching.in @@ -0,0 +1,12 @@ +{"cmd": "example : 1 = 1 := by sorry"} + +{"tactic": "rfl", "proofState": 0} + +{"tactic": "have : 2 = 2 := by sorry", "proofState": 0} + +{"tactic": "exact h1", "proofState": 2} + +{"tactic": "rfl", "proofState": 2} + +{"tactic": "rfl", "proofState": 4} + diff --git a/test/tactic_mode_sorry.expected.out b/test/tactic_mode_sorry.expected.out index 15c007e6..341b6969 100644 --- a/test/tactic_mode_sorry.expected.out +++ b/test/tactic_mode_sorry.expected.out @@ -10,8 +10,7 @@ "data": "declaration uses 'sorry'"}], "env": 0} -{"sorries": [{"proofState": 1, "goal": "⊢ Nat"}], - "proofStatus": "Incomplete: contains sorry", - "proofState": 2, - "goals": []} +{"proofStatus": "Incomplete: open goals remain", + "proofState": 1, + "goals": ["⊢ Nat"]} From 58643ebae1128302617682e93d491eb3b64cf85d Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 4 Jul 2025 12:19:46 +0200 Subject: [PATCH 4/8] Improve goal ordering --- REPL/Snapshots.lean | 2 +- test/Mathlib/test/on_goal.expected.out | 8 ++-- test/app_type_mismatch2.expected.out | 6 +-- test/app_type_mismatch2.in | 2 +- test/auxiliary_declaration.expected.out | 23 --------- test/auxiliary_declaration.in | 8 ---- test/have_by_sorry.expected.out | 2 +- test/name_generator.expected.out | 64 ++++++++++++++----------- test/sketch_tactic.expected.out | 37 ++++++++++++++ test/sketch_tactic.in | 12 +++++ test/sorry_hypotheses.expected.out | 2 +- test/tactic_have_branching.expected.out | 6 +-- test/tactic_have_branching.in | 4 +- 13 files changed, 100 insertions(+), 76 deletions(-) delete mode 100644 test/auxiliary_declaration.expected.out delete mode 100644 test/auxiliary_declaration.in create mode 100644 test/sketch_tactic.expected.out create mode 100644 test/sketch_tactic.in diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index 15eb1679..6d456516 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -213,7 +213,7 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot := let exprHoles ← mctx.eAssignment.foldlM processExpr [] pure exprHoles - let combinedGoals := result'.tacticState.goals ++ newGoals + let combinedGoals := newGoals ++ result'.tacticState.goals return { result' with tacticState := { goals := combinedGoals } } /-- Pretty print the current goals in the `ProofSnapshot`. -/ diff --git a/test/Mathlib/test/on_goal.expected.out b/test/Mathlib/test/on_goal.expected.out index 108dd0bd..61748668 100644 --- a/test/Mathlib/test/on_goal.expected.out +++ b/test/Mathlib/test/on_goal.expected.out @@ -15,8 +15,8 @@ {"proofStatus": "Incomplete: open goals remain", "proofState": 1, "goals": - ["case pos\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : x < 0\n⊢ x < 0 ∨ 2 * x > 2", - "case neg\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : ¬x < 0\n⊢ x < 0 ∨ 2 * x > 2", - "x : ℝ\nh0 : |x| > 1\n⊢ x = x", - "x : ℝ\nh0 : |x| > 1\nh1 : x = x\n⊢ x = x"]} + ["x : ℝ\nh0 : |x| > 1\n⊢ x = x", + "x : ℝ\nh0 : |x| > 1\nh1 : x = x\n⊢ x = x", + "case pos\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : x < 0\n⊢ x < 0 ∨ 2 * x > 2", + "case neg\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : ¬x < 0\n⊢ x < 0 ∨ 2 * x > 2"]} diff --git a/test/app_type_mismatch2.expected.out b/test/app_type_mismatch2.expected.out index 8cd7c6be..3b5f9c19 100644 --- a/test/app_type_mismatch2.expected.out +++ b/test/app_type_mismatch2.expected.out @@ -34,12 +34,12 @@ {"proofStatus": "Incomplete: open goals remain", "proofState": 4, "goals": - ["case succ\nn✝ : Nat\nthis : true = true\n⊢ n✝ + 1 = 0", - "n✝ : Nat\n⊢ true = true"]} + ["n✝ : Nat\n⊢ true = true", + "case succ\nn✝ : Nat\nthis : true = true\n⊢ n✝ + 1 = 0"]} {"proofStatus": "Incomplete: open goals remain", "proofState": 5, - "goals": ["n✝ : Nat\n⊢ true = true"]} + "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"} diff --git a/test/app_type_mismatch2.in b/test/app_type_mismatch2.in index 47300014..1d58afa6 100644 --- a/test/app_type_mismatch2.in +++ b/test/app_type_mismatch2.in @@ -12,5 +12,5 @@ {"tactic": "apply ?succ", "proofState": 4} -{"tactic": "rfl", "proofState": 5} +{"tactic": "trivial", "proofState": 5} diff --git a/test/auxiliary_declaration.expected.out b/test/auxiliary_declaration.expected.out deleted file mode 100644 index 4fb06d00..00000000 --- a/test/auxiliary_declaration.expected.out +++ /dev/null @@ -1,23 +0,0 @@ -{"sorries": - [{"proofState": 0, - "pos": {"line": 1, "column": 21}, - "goal": "⊢ true = true", - "endPos": {"line": 1, "column": 26}}], - "messages": - [{"severity": "warning", - "pos": {"line": 1, "column": 0}, - "endPos": {"line": 1, "column": 7}, - "data": "declaration uses 'sorry'"}], - "env": 0} - -{"proofStatus": "Incomplete: open goals remain", - "proofState": 1, - "goals": ["p : ∃ x, x > 0 := Exists.intro 1 Nat.one_pos\n⊢ true = true"]} - -{"proofStatus": "Incomplete: open goals remain", - "proofState": 2, - "goals": - ["p : ∃ x, x > 0 := Exists.intro 1 Nat.one_pos\nn : Nat\nhn : n > 0\n⊢ true = true"]} - -{"proofStatus": "Completed", "proofState": 3, "goals": []} - diff --git a/test/auxiliary_declaration.in b/test/auxiliary_declaration.in deleted file mode 100644 index 6b26b301..00000000 --- a/test/auxiliary_declaration.in +++ /dev/null @@ -1,8 +0,0 @@ -{"cmd": "example : true := by sorry"} - -{"tactic": "let p : ∃ x : Nat, x > 0 := ⟨1, Nat.one_pos⟩", "proofState": 0} - -{"tactic": "let ⟨n, hn⟩ := p", "proofState": 1} - -{"tactic": "rfl", "proofState": 2} - diff --git a/test/have_by_sorry.expected.out b/test/have_by_sorry.expected.out index 23f1987e..c8dba09c 100644 --- a/test/have_by_sorry.expected.out +++ b/test/have_by_sorry.expected.out @@ -24,5 +24,5 @@ {"proofStatus": "Incomplete: open goals remain", "proofState": 2, - "goals": ["x : Int\nh : x = 1\n⊢ x = 1", "x : Int\n⊢ x = 1"]} + "goals": ["x : Int\n⊢ x = 1", "x : Int\nh : x = 1\n⊢ x = 1"]} diff --git a/test/name_generator.expected.out b/test/name_generator.expected.out index 99c81b85..1ed48ad9 100644 --- a/test/name_generator.expected.out +++ b/test/name_generator.expected.out @@ -12,51 +12,57 @@ {"proofStatus": "Incomplete: open goals remain", "proofState": 1, - "goals": ["x : Int\nh0 h : x > 0\n⊢ False", "x : Int\nh0 : x > 0\n⊢ x > 0"]} - -{"message": - "Lean error:\ntype mismatch\n h0\nhas type\n x > 0 : Prop\nbut is expected to have type\n False : Prop"} - -{"message": - "Lean error:\ntactic 'assumption' failed\nx : Int\nh0 h : x > 0\n⊢ False"} - -{"message": "Lean error:\nsimp made no progress"} + "goals": ["x : Int\nh0 : x > 0\n⊢ x > 0", "x : Int\nh0 h : x > 0\n⊢ False"]} {"proofStatus": "Incomplete: open goals remain", "proofState": 2, - "messages": - [{"severity": "error", - "pos": {"line": 0, "column": 0}, - "endPos": {"line": 0, "column": 0}, - "data": "simp made no progress"}], - "goals": ["x : Int\nh0 : x > 0\n⊢ x > 0", "x : Int\nh0 h : x > 0\n⊢ False"]} + "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]} {"proofStatus": "Incomplete: open goals remain", "proofState": 3, - "messages": - [{"severity": "error", - "pos": {"line": 0, "column": 0}, - "endPos": {"line": 0, "column": 0}, - "data": "simp made no progress"}], - "goals": ["x : Int\nh0 : x > 0\n⊢ x > 0", "x : Int\nh0 h : x > 0\n⊢ False"]} + "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]} -{"proofStatus": "Incomplete: open goals remain", +{"traces": + ["[Meta.Tactic.simp.rewrite] of_eq_true (eq_true h0):1000:\n x > 0\n ==>\n True"], + "proofStatus": "Incomplete: open goals remain", "proofState": 4, + "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]} + +{"traces": + ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000:\n x > 0\n ==>\n 0 < x", + "[Meta.Tactic.simp.rewrite] h0:1000:\n 0 < x\n ==>\n True"], + "proofStatus": "Incomplete: open goals remain", + "proofState": 5, + "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]} + +{"traces": + ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000:\n x > 0\n ==>\n 0 < x", + "[Meta.Tactic.simp.rewrite] h0:1000:\n 0 < x\n ==>\n True"], + "proofStatus": "Incomplete: open goals remain", + "proofState": 6, + "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 7, "messages": [{"severity": "error", "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, - "data": - "tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n x\nx : Int\nh0 h : x > 0\n⊢ False"}], - "goals": ["x : Int\nh0 : x > 0\n⊢ x > 0", "x : Int\nh0 h : x > 0\n⊢ False"]} + "data": "unsolved goals\nx : Int\nh0 : x > 0\n⊢ x > 0"}], + "goals": + ["x : Int\nh0 : x > 0\n⊢ x > 0", + "x : Int\nh0 : x > 0\n⊢ x > 0", + "x : Int\nh0 h : x > 0\n⊢ False"]} {"proofStatus": "Incomplete: open goals remain", - "proofState": 5, + "proofState": 8, "messages": [{"severity": "error", "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, - "data": - "tactic 'rewrite' failed, did not find instance of the pattern in the target expression\n x\nx : Int\nh0 h : x > 0\n⊢ False"}], - "goals": ["x : Int\nh0 : x > 0\n⊢ x > 0", "x : Int\nh0 h : x > 0\n⊢ False"]} + "data": "unsolved goals\nx : Int\nh0 : x > 0\n⊢ x > 0"}], + "goals": + ["x : Int\nh0 : x > 0\n⊢ x > 0", + "x : Int\nh0 : x > 0\n⊢ x > 0", + "x : Int\nh0 h : x > 0\n⊢ False"]} diff --git a/test/sketch_tactic.expected.out b/test/sketch_tactic.expected.out new file mode 100644 index 00000000..b7d32be4 --- /dev/null +++ b/test/sketch_tactic.expected.out @@ -0,0 +1,37 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 70}, + "goal": "⊢ ∀ (n m : Nat), n + m = m + n", + "endPos": {"line": 1, "column": 75}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 37}, + "data": "declaration uses 'sorry'"}], + "env": 0} + +{"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 : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m", + "m : Nat\n⊢ 0 + m = m"]} + +{"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\nh_base : 0 + m = m\n⊢ m + 0 = m", + "m : Nat\n⊢ 0 + m = m"]} + +{"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"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 4, + "goals": ["m : Nat\n⊢ 0 + m = m"]} + +{"proofStatus": "Completed", "proofState": 5, "goals": []} + diff --git a/test/sketch_tactic.in b/test/sketch_tactic.in new file mode 100644 index 00000000..d99b8051 --- /dev/null +++ b/test/sketch_tactic.in @@ -0,0 +1,12 @@ +{"cmd": "theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry"} + +{"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": 2} + +{"tactic": "apply Nat.add_zero", "proofState": 3} + +{"tactic": "apply Nat.zero_add", "proofState": 4} + diff --git a/test/sorry_hypotheses.expected.out b/test/sorry_hypotheses.expected.out index 32abd682..5fea7fd3 100644 --- a/test/sorry_hypotheses.expected.out +++ b/test/sorry_hypotheses.expected.out @@ -12,5 +12,5 @@ {"proofStatus": "Incomplete: open goals remain", "proofState": 1, - "goals": ["x : Int\nh : x = 1\n⊢ x = x", "x : Int\n⊢ x = 1"]} + "goals": ["x : Int\n⊢ x = 1", "x : Int\nh : x = 1\n⊢ x = x"]} diff --git a/test/tactic_have_branching.expected.out b/test/tactic_have_branching.expected.out index 037d9321..07b9c2db 100644 --- a/test/tactic_have_branching.expected.out +++ b/test/tactic_have_branching.expected.out @@ -14,7 +14,7 @@ {"proofStatus": "Incomplete: open goals remain", "proofState": 2, - "goals": ["this : 2 = 2\n⊢ 1 = 1", "⊢ 2 = 2"]} + "goals": ["⊢ True", "this : True\n⊢ 1 = 1"]} {"proofStatus": "Incomplete: open goals remain", "proofState": 3, @@ -23,11 +23,11 @@ "pos": {"line": 0, "column": 0}, "endPos": {"line": 0, "column": 0}, "data": "unknown identifier 'h1'"}], - "goals": ["⊢ 2 = 2", "this : 2 = 2\n⊢ 1 = 1"]} + "goals": ["⊢ True", "this : True\n⊢ 1 = 1"]} {"proofStatus": "Incomplete: open goals remain", "proofState": 4, - "goals": ["⊢ 2 = 2"]} + "goals": ["this : True\n⊢ 1 = 1"]} {"proofStatus": "Completed", "proofState": 5, "goals": []} diff --git a/test/tactic_have_branching.in b/test/tactic_have_branching.in index c52a042d..721cb9fa 100644 --- a/test/tactic_have_branching.in +++ b/test/tactic_have_branching.in @@ -2,11 +2,11 @@ {"tactic": "rfl", "proofState": 0} -{"tactic": "have : 2 = 2 := by sorry", "proofState": 0} +{"tactic": "have : True := by sorry", "proofState": 0} {"tactic": "exact h1", "proofState": 2} -{"tactic": "rfl", "proofState": 2} +{"tactic": "exact True.intro", "proofState": 2} {"tactic": "rfl", "proofState": 4} From 2a92964369cc594cfe7ea43ae9da6ee5b371a324 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 4 Jul 2025 12:19:46 +0200 Subject: [PATCH 5/8] Add "grouped" sorry collection: collect all sorries form one declaration into one proofstate --- REPL/JSON.lean | 24 +++++++---- REPL/Lean/InfoTree.lean | 23 +++++++---- REPL/Main.lean | 41 ++++++++++++------- test/Mathlib/test/20240209.expected.out | 3 +- test/Mathlib/test/20240209.in | 2 +- test/Mathlib/test/H20231115.expected.out | 3 +- test/Mathlib/test/H20231115.in | 2 +- test/Mathlib/test/H20231115_2.expected.out | 6 ++- test/Mathlib/test/H20231115_2.in | 2 +- test/Mathlib/test/H20231215_2.expected.out | 3 +- test/Mathlib/test/H20231215_2.in | 2 +- test/Mathlib/test/exact.expected.out | 6 ++- test/Mathlib/test/exact.in | 4 +- test/Mathlib/test/induction.expected.out | 3 +- test/Mathlib/test/induction.in | 2 +- test/Mathlib/test/on_goal.expected.out | 3 +- test/Mathlib/test/on_goal.in | 2 +- test/Mathlib/test/pickle.expected.out | 3 +- test/Mathlib/test/pickle.in | 2 +- .../test/placeholder_synthesis.expected.out | 3 +- test/Mathlib/test/placeholder_synthesis.in | 2 +- test/all_tactics.expected.out | 2 + test/app_type_mismatch.expected.out | 3 +- test/app_type_mismatch.in | 2 +- test/app_type_mismatch2.expected.out | 3 +- test/app_type_mismatch2.in | 2 +- test/assumption_proof.expected.out | 3 +- test/assumption_proof.in | 2 +- test/by_cases.expected.out | 3 +- test/by_cases.in | 2 +- test/calc.expected.out | 10 ++++- test/calc.in | 2 +- test/dup_sorries.expected.out | 6 ++- test/dup_sorries.in | 4 +- test/file.expected.out | 1 + test/goal_branching.expected.out | 3 +- test/goal_branching.in | 2 +- test/have_by_sorry.expected.out | 6 ++- test/have_by_sorry.in | 6 +-- test/invalid_tactic.expected.out | 3 +- test/invalid_tactic.in | 2 +- test/name_generator.expected.out | 3 +- test/name_generator.in | 2 +- test/no_goal_sorry_2.expected.out | 3 +- test/no_goal_sorry_2.in | 2 +- test/pickle_open_scoped.expected.out | 3 +- test/pickle_open_scoped.in | 2 +- test/pickle_open_scoped_2.expected.out | 3 +- test/pickle_open_scoped_2.in | 2 +- test/pickle_proof_state_1.expected.out | 3 +- test/pickle_proof_state_1.in | 2 +- test/pickle_proof_state_env.expected.out | 3 +- test/pickle_proof_state_env.in | 2 +- test/proof_branching.expected.out | 3 +- test/proof_branching.in | 2 +- test/proof_branching2.expected.out | 3 +- test/proof_branching2.in | 2 +- test/proof_step.expected.out | 3 +- test/proof_step.in | 2 +- test/proof_transitivity.expected.out | 6 ++- test/proof_transitivity.in | 4 +- test/readme.expected.out | 3 +- test/readme.in | 2 +- test/root_goals.expected.out | 8 ++-- test/root_goals.in | 2 +- test/self_proof_apply_check.expected.out | 3 +- test/self_proof_apply_check.in | 2 +- test/self_proof_check.expected.out | 18 ++++---- test/self_proof_check.in | 10 ++--- test/self_proof_exact_check.expected.out | 3 +- test/self_proof_exact_check.in | 2 +- test/self_proof_rw.expected.out | 3 +- test/self_proof_rw.in | 2 +- test/sketch_tactic.expected.out | 3 +- test/sketch_tactic.in | 2 +- test/sorry_hypotheses.expected.out | 3 +- test/sorry_hypotheses.in | 2 +- test/tactic_have_branching.expected.out | 3 +- test/tactic_have_branching.in | 2 +- test/tactic_mode_sorry.expected.out | 3 +- test/tactic_mode_sorry.in | 2 +- test/tactic_sorry.expected.out | 3 +- test/tactic_sorry.in | 2 +- test/term_sorry.expected.out | 3 +- test/term_sorry.in | 2 +- test/trace_simp.expected.out | 3 +- test/trace_simp.in | 2 +- test/unknown_proof_state.expected.out | 3 +- test/unknown_proof_state.in | 2 +- test/unknown_tactic.expected.out | 3 +- test/unknown_tactic.in | 2 +- test/variables.expected.out | 5 ++- test/variables.in | 2 +- 93 files changed, 229 insertions(+), 144 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 5e7270f4..492bbe75 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -13,7 +13,8 @@ namespace REPL structure CommandOptions where allTactics : Option Bool := none - rootGoals : Option Bool := none + -- Should be "individual", "grouped", or "rootGoals". + sorries : Option String := none /-- Should be "full", "tactics", "original", or "substantive". Anything else is ignored. @@ -76,28 +77,32 @@ def Message.of (m : Lean.Message) : IO Message := do pure <| structure Sorry where pos : Pos endPos : Pos - goal : String + goals : List String /-- The index of the proof state at the sorry. You can use the `ProofStep` instruction to run a tactic at this state. -/ proofState : Option Nat + parentDecl: Option Name := none deriving FromJson instance : ToJson Sorry where toJson r := Json.mkObj <| .flatten [ - [("goal", r.goal)], + [("goals", toJson r.goals)], [("proofState", toJson r.proofState)], if r.pos.line ≠ 0 then [("pos", toJson r.pos)] else [], if r.endPos.line ≠ 0 then [("endPos", toJson r.endPos)] else [], + if r.parentDecl.isSome then [("parentDecl", toJson r.parentDecl)] else [] ] /-- Construct the JSON representation of a Lean sorry. -/ -def Sorry.of (goal : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry := +def Sorry.of (goals : List String) (pos endPos : Lean.Position) (proofState : Option Nat) +(parentDecl : Option Name): Sorry := { pos := ⟨pos.line, pos.column⟩, endPos := ⟨endPos.line, endPos.column⟩, - goal, - proofState } + goals, + proofState, + parentDecl } structure Tactic where pos : Pos @@ -106,16 +111,19 @@ structure Tactic where tactic : String proofState : Option Nat usedConstants : Array Name + parentDecl : Option Name := none deriving ToJson, FromJson /-- Construct the JSON representation of a Lean tactic. -/ -def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : Option Nat) (usedConstants : Array Name) : Tactic := +def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : Option Nat) +(usedConstants : Array Name) (parentDecl : Option Name) : Tactic := { pos := ⟨pos.line, pos.column⟩, endPos := ⟨endPos.line, endPos.column⟩, goals, tactic, proofState, - usedConstants } + usedConstants, + parentDecl } /-- A response to a Lean command. diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean index a3f68165..ba1687e4 100644 --- a/REPL/Lean/InfoTree.lean +++ b/REPL/Lean/InfoTree.lean @@ -195,18 +195,18 @@ def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo × List MVa | (.ofTacticInfo i, some ctx, rootGoals) => (i, ctx, rootGoals) | _ => none -/-- Returns the root goals for a given `InfoTree`. -/ -partial def findRootGoals (t : InfoTree) (ctx? : Option ContextInfo := none) : - List (TacticInfo × ContextInfo × List MVarId) := +/-- Returns the root and last goals for a given `InfoTree`. -/ +partial def findRootAndLastGoals (t : InfoTree) (ctx? : Option ContextInfo := none) : + List (TacticInfo × ContextInfo × List MVarId × List MVarId) := match t with - | .context ctx t => t.findRootGoals (ctx.mergeIntoOuter? ctx?) + | .context ctx t => t.findRootAndLastGoals (ctx.mergeIntoOuter? ctx?) | .node info ts => match info with | .ofTacticInfo i => match ctx? with - | some ctx => [(i, ctx, i.goalsBefore)] + | some ctx => [(i, ctx, i.goalsBefore, i.goalsAfter)] | _ => [] - | _ => ts.toList.flatMap (fun t => t.findRootGoals ctx?) + | _ => ts.toList.flatMap (fun t => t.findRootAndLastGoals ctx?) | _ => [] /-- Return all `TacticInfo` nodes in an `InfoTree` @@ -264,12 +264,21 @@ def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × List i.getUsedConstantsAsSet.toArray ) def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) := - t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ => + t.findRootAndLastGoals.map fun ⟨i, ctx, rootGoals, _⟩ => let range := stxRange ctx.fileMap i.stx ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, rootGoals, range.fst ) +def rootAndLastGoals (t : InfoTree) : List (ContextInfo × List MVarId × List MVarId × Position × Position) := + t.findRootAndLastGoals.map fun ⟨i, ctx, rootGoals, lastGoals⟩ => + let range := stxRange ctx.fileMap i.stx + ( { ctx with mctx := i.mctxAfter, ngen := ctx.ngen.mkChild.1 }, + rootGoals, + lastGoals, + range.fst, + range.snd ) + end Lean.Elab.InfoTree namespace Lean.Elab.TacticInfo diff --git a/REPL/Main.lean b/REPL/Main.lean index 39bb3a0d..0a1ce54c 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -100,20 +100,33 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op | .term _ none => false | _ => true ) |>.mapM fun ⟨ctx, g, pos, endPos⟩ => do - let (goal, proofState) ← match g with + let (goals, proofState) ← match g with | .tactic g => do let lctx ← ctx.runMetaM {} do match ctx.mctx.findDecl? g with | some decl => return decl.lctx | none => throwError "unknown metavariable '{g}'" let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals? - pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) + pure ((← s.ppGoals).map (s!"{·}"), some s) | .term lctx (some t) => do let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t] - pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) + pure ((← s.ppGoals).map (s!"{·}"), some s) | .term _ none => unreachable! let proofStateId ← proofState.mapM recordProofSnapshot - return Sorry.of goal pos endPos proofStateId + return Sorry.of goals pos endPos proofStateId ctx.parentDecl? + +def groupedSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do + let a ← trees.flatMap InfoTree.rootAndLastGoals |>.mapM + fun ⟨ctx, rootGoals, lastGoals, startPos, endPos⟩ => do + let proofState ← ProofSnapshot.create ctx none env? lastGoals rootGoals + let proofState' ← proofState.runString "skip" -- Trick to get the sorries + let goals := (← proofState'.ppGoals).map (s!"{·}") + if goals.isEmpty then + return [] + else + let proofStateId ← recordProofSnapshot proofState' + return [Sorry.of goals startPos endPos proofStateId ctx.parentDecl?] + return a.flatten def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := ctx.runMetaM {} try @@ -128,15 +141,15 @@ def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tact let goals := s!"{(← ctx.ppGoals goals)}".trim let tactic := Format.pretty (← ppTactic ctx stx) let proofStateId ← proofState.mapM recordProofSnapshot - return Tactic.of goals tactic pos endPos proofStateId ns + return Tactic.of goals tactic pos endPos proofStateId ns ctx.parentDecl? def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do trees.flatMap InfoTree.rootGoals |>.mapM fun ⟨ctx, goals, pos⟩ => do let proofState := some (← ProofSnapshot.create ctx none env? goals goals) - let goals := s!"{(← ctx.ppGoals goals)}".trim + let goals ← goals.mapM (fun g => do pure s!"{(← ctx.ppGoals [g])}".trim) let proofStateId ← proofState.mapM recordProofSnapshot - return Sorry.of goals pos pos proofStateId + return Sorry.of goals pos ⟨0,0⟩ proofStateId ctx.parentDecl? private def collectFVarsAux : Expr → NameSet @@ -200,6 +213,8 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do let pf ← abstractAllLambdaFVars pf let pft ← Meta.inferType pf >>= instantiateMVars + if pf.hasSorry then + return "Incomplete: contains sorry" if pf.hasExprMVar then return "Incomplete: contains metavariable(s)" @@ -220,9 +235,6 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do let _ ← addDecl decl catch ex => return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" - - if pf.hasSorry then - return "Incomplete: contains sorry" return "Completed" | _ => return "Not verified: more than one initial goal" @@ -298,10 +310,11 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do let messages ← messages.mapM fun m => Message.of m -- For debugging purposes, sometimes we print out the trees here: -- trees.forM fun t => do IO.println (← t.format) - let sorries ← sorries trees initialCmdState.env none - let sorries ← match s.rootGoals with - | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env)) - | _ => pure sorries + let sorries ← match s.sorries with + | some "individual" => sorries trees initialCmdState.env none + | some "grouped" => groupedSorries trees initialCmdState.env + | some "rootGoals" => collectRootGoalsAsSorries trees initialCmdState.env + | _ => pure [] let tactics ← match s.allTactics with | some true => tactics trees initialCmdState.env | _ => pure [] diff --git a/test/Mathlib/test/20240209.expected.out b/test/Mathlib/test/20240209.expected.out index 521f9c7e..cabececb 100644 --- a/test/Mathlib/test/20240209.expected.out +++ b/test/Mathlib/test/20240209.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 22}, - "goal": "⊢ False", + "parentDecl": "_example", + "goals": ["⊢ False"], "endPos": {"line": 1, "column": 27}}], "messages": [{"severity": "warning", diff --git a/test/Mathlib/test/20240209.in b/test/Mathlib/test/20240209.in index 08ebbb21..28f4d8ea 100644 --- a/test/Mathlib/test/20240209.in +++ b/test/Mathlib/test/20240209.in @@ -1,3 +1,3 @@ -{"cmd": "example : False := by sorry"} +{"cmd": "example : False := by sorry", "sorries": "individual"} {"tactic": "simpa using show False by done", "proofState": 0} diff --git a/test/Mathlib/test/H20231115.expected.out b/test/Mathlib/test/H20231115.expected.out index e283b375..4d7cbd6f 100644 --- a/test/Mathlib/test/H20231115.expected.out +++ b/test/Mathlib/test/H20231115.expected.out @@ -3,7 +3,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 36}, - "goal": "x : Nat\n⊢ x + 1 > x", + "parentDecl": "_example", + "goals": ["x : Nat\n⊢ x + 1 > x"], "endPos": {"line": 1, "column": 41}}], "messages": [{"severity": "warning", diff --git a/test/Mathlib/test/H20231115.in b/test/Mathlib/test/H20231115.in index 4bca3cda..d780d278 100644 --- a/test/Mathlib/test/H20231115.in +++ b/test/Mathlib/test/H20231115.in @@ -1,5 +1,5 @@ {"cmd": "import Mathlib.Tactic.Cases"} -{"cmd": "example {x : Nat} : x + 1 > x := by sorry", "env": 0} +{"cmd": "example {x : Nat} : x + 1 > x := by sorry", "env": 0, "sorries": "individual"} {"tactic": "induction' x with x hx", "proofState": 0} diff --git a/test/Mathlib/test/H20231115_2.expected.out b/test/Mathlib/test/H20231115_2.expected.out index 3c19b57e..4c85f89a 100644 --- a/test/Mathlib/test/H20231115_2.expected.out +++ b/test/Mathlib/test/H20231115_2.expected.out @@ -3,11 +3,13 @@ {"sorries": [{"proofState": 0, "pos": {"line": 3, "column": 12}, - "goal": "case zero\n⊢ 0 + 1 > 0", + "parentDecl": "_example", + "goals": ["case zero\n⊢ 0 + 1 > 0"], "endPos": {"line": 3, "column": 17}}, {"proofState": 1, "pos": {"line": 3, "column": 12}, - "goal": "case succ\nx : Nat\nhx : x + 1 > x\n⊢ x + 1 + 1 > x + 1", + "parentDecl": "_example", + "goals": ["case succ\nx : Nat\nhx : x + 1 > x\n⊢ x + 1 + 1 > x + 1"], "endPos": {"line": 3, "column": 17}}], "messages": [{"severity": "warning", diff --git a/test/Mathlib/test/H20231115_2.in b/test/Mathlib/test/H20231115_2.in index bab26d4b..9f6da6c6 100644 --- a/test/Mathlib/test/H20231115_2.in +++ b/test/Mathlib/test/H20231115_2.in @@ -1,4 +1,4 @@ {"cmd": "import Mathlib.Tactic.Cases"} -{"cmd": "example {x : Nat} : x + 1 > x := by\n induction' x with x hx\n all_goals sorry", "env": 0} +{"cmd": "example {x : Nat} : x + 1 > x := by\n induction' x with x hx\n all_goals sorry", "env": 0, "sorries": "individual"} diff --git a/test/Mathlib/test/H20231215_2.expected.out b/test/Mathlib/test/H20231215_2.expected.out index 1a83bcff..408dc2a2 100644 --- a/test/Mathlib/test/H20231215_2.expected.out +++ b/test/Mathlib/test/H20231215_2.expected.out @@ -3,7 +3,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 2, "column": 20}, - "goal": "⊢ 9! % 10 = 0", + "parentDecl": "mathd_numbertheory_739", + "goals": ["⊢ 9! % 10 = 0"], "endPos": {"line": 2, "column": 25}}], "messages": [{"severity": "warning", diff --git a/test/Mathlib/test/H20231215_2.in b/test/Mathlib/test/H20231215_2.in index 72323c8b..cb9f4ff0 100644 --- a/test/Mathlib/test/H20231215_2.in +++ b/test/Mathlib/test/H20231215_2.in @@ -1,3 +1,3 @@ {"unpickleEnvFrom": "test/H20231215.olean"} -{"cmd": "theorem mathd_numbertheory_739 :\n 9! % 10 = 0 := by sorry", "env": 0} +{"cmd": "theorem mathd_numbertheory_739 :\n 9! % 10 = 0 := by sorry", "env": 0, "sorries": "individual"} diff --git a/test/Mathlib/test/exact.expected.out b/test/Mathlib/test/exact.expected.out index 39e77965..6a6793a0 100644 --- a/test/Mathlib/test/exact.expected.out +++ b/test/Mathlib/test/exact.expected.out @@ -3,7 +3,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 27}, - "goal": "⊢ 0 < 1", + "parentDecl": "test", + "goals": ["⊢ 0 < 1"], "endPos": {"line": 1, "column": 32}}], "messages": [{"severity": "warning", @@ -24,7 +25,8 @@ {"sorries": [{"proofState": 2, "pos": {"line": 1, "column": 27}, - "goal": "⊢ 3 = 7", + "parentDecl": "test", + "goals": ["⊢ 3 = 7"], "endPos": {"line": 1, "column": 32}}], "messages": [{"severity": "warning", diff --git a/test/Mathlib/test/exact.in b/test/Mathlib/test/exact.in index 72b4c503..3eff4b9e 100644 --- a/test/Mathlib/test/exact.in +++ b/test/Mathlib/test/exact.in @@ -1,10 +1,10 @@ {"cmd": "import Mathlib"} -{"cmd": "theorem test : 0 < 1 := by sorry", "env": 0} +{"cmd": "theorem test : 0 < 1 := by sorry", "env": 0, "sorries": "individual"} {"tactic": "exact?", "proofState": 0} -{"cmd": "theorem test : 3 = 7 := by sorry", "env": 0} +{"cmd": "theorem test : 3 = 7 := by sorry", "env": 0, "sorries": "individual"} {"tactic": "exact?", "proofState": 2} diff --git a/test/Mathlib/test/induction.expected.out b/test/Mathlib/test/induction.expected.out index 9b2ca0d0..5e672ee7 100644 --- a/test/Mathlib/test/induction.expected.out +++ b/test/Mathlib/test/induction.expected.out @@ -3,7 +3,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 36}, - "goal": "x : ℕ\n⊢ x = x", + "parentDecl": "foo", + "goals": ["x : ℕ\n⊢ x = x"], "endPos": {"line": 1, "column": 41}}], "messages": [{"severity": "warning", diff --git a/test/Mathlib/test/induction.in b/test/Mathlib/test/induction.in index f739d556..c98728f1 100644 --- a/test/Mathlib/test/induction.in +++ b/test/Mathlib/test/induction.in @@ -1,6 +1,6 @@ {"cmd": "import Mathlib"} -{"env" : 0, "cmd": "theorem foo (x : Nat) : x = x := by sorry"} +{"env" : 0, "cmd": "theorem foo (x : Nat) : x = x := by sorry", "sorries": "individual"} {"proofState" : 0, "tactic": "induction x"} diff --git a/test/Mathlib/test/on_goal.expected.out b/test/Mathlib/test/on_goal.expected.out index 61748668..4221aa86 100644 --- a/test/Mathlib/test/on_goal.expected.out +++ b/test/Mathlib/test/on_goal.expected.out @@ -3,7 +3,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 60}, - "goal": "x : ℝ\nh0 : |x| > 1\n⊢ x < 0 ∨ 2 * x > 2", + "parentDecl": "_example", + "goals": ["x : ℝ\nh0 : |x| > 1\n⊢ x < 0 ∨ 2 * x > 2"], "endPos": {"line": 1, "column": 65}}], "messages": [{"severity": "warning", diff --git a/test/Mathlib/test/on_goal.in b/test/Mathlib/test/on_goal.in index 3fd2baa9..04bfc188 100644 --- a/test/Mathlib/test/on_goal.in +++ b/test/Mathlib/test/on_goal.in @@ -1,5 +1,5 @@ {"cmd": "import Mathlib\nopen Real"} -{"cmd": "example {x : ℝ} (h0: |x| > 1) : (x < 0) ∨ (2 * x > 2) := by sorry", "env": 0} +{"cmd": "example {x : ℝ} (h0: |x| > 1) : (x < 0) ∨ (2 * x > 2) := by sorry", "env": 0, "sorries": "individual"} {"tactic": "on_goal 1 =>\n have h1 : x = x := by sorry\n have h2 : x = x := by sorry\n by_cases h3 : x < 0", "proofState": 0} diff --git a/test/Mathlib/test/pickle.expected.out b/test/Mathlib/test/pickle.expected.out index e3d1c163..a5ca0d85 100644 --- a/test/Mathlib/test/pickle.expected.out +++ b/test/Mathlib/test/pickle.expected.out @@ -3,7 +3,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 4, "column": 14}, - "goal": "x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3", + "parentDecl": "mathd_algebra_455", + "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"], "endPos": {"line": 4, "column": 19}}], "messages": [{"severity": "warning", diff --git a/test/Mathlib/test/pickle.in b/test/Mathlib/test/pickle.in index 0951e383..4893d0c4 100644 --- a/test/Mathlib/test/pickle.in +++ b/test/Mathlib/test/pickle.in @@ -1,6 +1,6 @@ {"cmd": "import Mathlib\nopen BigOperators\nopen Real\nopen Nat"} -{"cmd": "theorem mathd_algebra_455\n (x : Nat)\n (h : 2 * (2 * (2 * (2 * x))) = 48) :\n x = 3 := by sorry", "env": 0} +{"cmd": "theorem mathd_algebra_455\n (x : Nat)\n (h : 2 * (2 * (2 * (2 * x))) = 48) :\n x = 3 := by sorry", "env": 0, "sorries": "individual"} {"pickleTo": "test/pickle.olean", "proofState": 0} diff --git a/test/Mathlib/test/placeholder_synthesis.expected.out b/test/Mathlib/test/placeholder_synthesis.expected.out index ad26358f..ccd4c02f 100644 --- a/test/Mathlib/test/placeholder_synthesis.expected.out +++ b/test/Mathlib/test/placeholder_synthesis.expected.out @@ -11,7 +11,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 19}, - "goal": "⊢ 1 = 0", + "parentDecl": "_example", + "goals": ["⊢ 1 = 0"], "endPos": {"line": 1, "column": 24}}], "messages": [{"severity": "warning", diff --git a/test/Mathlib/test/placeholder_synthesis.in b/test/Mathlib/test/placeholder_synthesis.in index 040097d3..c77d4fda 100644 --- a/test/Mathlib/test/placeholder_synthesis.in +++ b/test/Mathlib/test/placeholder_synthesis.in @@ -2,7 +2,7 @@ {"cmd": "example : 1 = 0 := by\n cases' exists_ne 2 with n h\n simpa [] using h _", "env": 0} -{"cmd": "example : 1 = 0 := sorry", "env": 0} +{"cmd": "example : 1 = 0 := sorry", "env": 0, "sorries": "individual"} {"tactic": "cases' exists_ne 2 with n h", "proofState": 0} diff --git a/test/all_tactics.expected.out b/test/all_tactics.expected.out index 6a08ee4b..79c2df79 100644 --- a/test/all_tactics.expected.out +++ b/test/all_tactics.expected.out @@ -3,12 +3,14 @@ "tactic": "have t := 37", "proofState": 0, "pos": {"line": 1, "column": 18}, + "parentDecl": "f", "goals": "⊢ Nat", "endPos": {"line": 1, "column": 30}}, {"usedConstants": [], "tactic": "exact t", "proofState": 1, "pos": {"line": 1, "column": 32}, + "parentDecl": "f", "goals": "t : Nat\n⊢ Nat", "endPos": {"line": 1, "column": 39}}], "env": 0} diff --git a/test/app_type_mismatch.expected.out b/test/app_type_mismatch.expected.out index 317d655e..13a2888c 100644 --- a/test/app_type_mismatch.expected.out +++ b/test/app_type_mismatch.expected.out @@ -8,7 +8,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 19}, - "goal": "⊢ 1 = 0", + "parentDecl": "_example", + "goals": ["⊢ 1 = 0"], "endPos": {"line": 1, "column": 24}}], "messages": [{"severity": "warning", diff --git a/test/app_type_mismatch.in b/test/app_type_mismatch.in index 4fc13b04..eb9ab9ee 100644 --- a/test/app_type_mismatch.in +++ b/test/app_type_mismatch.in @@ -1,6 +1,6 @@ {"cmd": "example : 1 = 0 := by\n cases 1\n rfl\n apply ?succ"} -{"cmd": "example : 1 = 0 := sorry"} +{"cmd": "example : 1 = 0 := sorry", "sorries": "individual"} {"tactic": "cases 1", "proofState": 0} diff --git a/test/app_type_mismatch2.expected.out b/test/app_type_mismatch2.expected.out index 3b5f9c19..37f3fd78 100644 --- a/test/app_type_mismatch2.expected.out +++ b/test/app_type_mismatch2.expected.out @@ -9,7 +9,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 19}, - "goal": "⊢ 1 = 0", + "parentDecl": "_example", + "goals": ["⊢ 1 = 0"], "endPos": {"line": 1, "column": 24}}], "messages": [{"severity": "warning", diff --git a/test/app_type_mismatch2.in b/test/app_type_mismatch2.in index 1d58afa6..bf1c1f79 100644 --- a/test/app_type_mismatch2.in +++ b/test/app_type_mismatch2.in @@ -1,6 +1,6 @@ {"cmd": "example : 1 = 0 := by\n cases 1\n rfl\n have: true := by\n apply ?succ\n trivial"} -{"cmd": "example : 1 = 0 := sorry"} +{"cmd": "example : 1 = 0 := sorry", "sorries": "individual"} {"tactic": "cases 1", "proofState": 0} diff --git a/test/assumption_proof.expected.out b/test/assumption_proof.expected.out index 0c253350..01b03e58 100644 --- a/test/assumption_proof.expected.out +++ b/test/assumption_proof.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 49}, - "goal": "x : Nat\nh1 : x = 2\n⊢ x = 2", + "parentDecl": "aa", + "goals": ["x : Nat\nh1 : x = 2\n⊢ x = 2"], "endPos": {"line": 1, "column": 54}}], "messages": [{"severity": "warning", diff --git a/test/assumption_proof.in b/test/assumption_proof.in index af5348c4..cd914697 100644 --- a/test/assumption_proof.in +++ b/test/assumption_proof.in @@ -1,3 +1,3 @@ -{"cmd": "theorem aa (x : Nat) (h1 : x = 2) : x = 2 := by sorry"} +{"cmd": "theorem aa (x : Nat) (h1 : x = 2) : x = 2 := by sorry", "sorries": "individual"} {"tactic": "assumption", "proofState": 0} diff --git a/test/by_cases.expected.out b/test/by_cases.expected.out index f7b19de6..1e99b39a 100644 --- a/test/by_cases.expected.out +++ b/test/by_cases.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 36}, - "goal": "x : Int\n⊢ x = x", + "parentDecl": "foo", + "goals": ["x : Int\n⊢ x = x"], "endPos": {"line": 1, "column": 41}}], "messages": [{"severity": "warning", diff --git a/test/by_cases.in b/test/by_cases.in index 031c43f6..2580c708 100644 --- a/test/by_cases.in +++ b/test/by_cases.in @@ -1,4 +1,4 @@ -{"cmd": "theorem foo (x : Int) : x = x := by sorry"} +{"cmd": "theorem foo (x : Int) : x = x := by sorry", "sorries": "individual"} {"proofState" : 0, "tactic": "by_cases h : x < 0"} diff --git a/test/calc.expected.out b/test/calc.expected.out index 8db4c61b..1d896a3d 100644 --- a/test/calc.expected.out +++ b/test/calc.expected.out @@ -15,12 +15,14 @@ "tactic": "calc\n 3 = 4 := by sorry\n 4 = 5 := by sorry", "proofState": 2, "pos": {"line": 1, "column": 22}, + "parentDecl": "_example", "goals": "⊢ 3 = 5", "endPos": {"line": 3, "column": 19}}, {"usedConstants": [], "tactic": "\n 3 = 4 := by sorry\n 4 = 5 := by sorry", "proofState": 3, "pos": {"line": 2, "column": 2}, + "parentDecl": "_example", "goals": "no goals", "endPos": {"line": 3, "column": 19}}, {"usedConstants": @@ -37,6 +39,7 @@ "tactic": "sorry", "proofState": 4, "pos": {"line": 2, "column": 14}, + "parentDecl": "_example", "goals": "⊢ 3 = 4", "endPos": {"line": 2, "column": 19}}, {"usedConstants": @@ -53,16 +56,19 @@ "tactic": "sorry", "proofState": 5, "pos": {"line": 3, "column": 14}, + "parentDecl": "_example", "goals": "⊢ 4 = 5", "endPos": {"line": 3, "column": 19}}], "sorries": [{"proofState": 0, "pos": {"line": 2, "column": 14}, - "goal": "⊢ 3 = 4", + "parentDecl": "_example", + "goals": ["⊢ 3 = 4"], "endPos": {"line": 2, "column": 19}}, {"proofState": 1, "pos": {"line": 3, "column": 14}, - "goal": "⊢ 4 = 5", + "parentDecl": "_example", + "goals": ["⊢ 4 = 5"], "endPos": {"line": 3, "column": 19}}], "messages": [{"severity": "warning", diff --git a/test/calc.in b/test/calc.in index 895da449..c268372d 100644 --- a/test/calc.in +++ b/test/calc.in @@ -1 +1 @@ -{"cmd": "example : 3 = 5 := by calc\n 3 = 4 := by sorry\n 4 = 5 := by sorry", "allTactics": true } +{"cmd": "example : 3 = 5 := by calc\n 3 = 4 := by sorry\n 4 = 5 := by sorry", "allTactics": true, "sorries": "individual"} diff --git a/test/dup_sorries.expected.out b/test/dup_sorries.expected.out index d01dd9b0..65f30c99 100644 --- a/test/dup_sorries.expected.out +++ b/test/dup_sorries.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 24}, - "goal": "⊢ 1 = 1", + "parentDecl": "thm1", + "goals": ["⊢ 1 = 1"], "endPos": {"line": 1, "column": 29}}], "messages": [{"severity": "warning", @@ -13,7 +14,8 @@ {"sorries": [{"proofState": 1, "pos": {"line": 1, "column": 24}, - "goal": "⊢ 2 = 2", + "parentDecl": "thm2", + "goals": ["⊢ 2 = 2"], "endPos": {"line": 1, "column": 29}}], "messages": [{"severity": "warning", diff --git a/test/dup_sorries.in b/test/dup_sorries.in index 78c8e1d3..477d52b5 100644 --- a/test/dup_sorries.in +++ b/test/dup_sorries.in @@ -1,3 +1,3 @@ -{"cmd": "theorem thm1 : 1 = 1 := sorry"} +{"cmd": "theorem thm1 : 1 = 1 := sorry", "sorries": "individual"} -{"cmd": "theorem thm2 : 2 = 2 := sorry", "env": 0} +{"cmd": "theorem thm2 : 2 = 2 := sorry", "sorries": "individual", "env": 0} diff --git a/test/file.expected.out b/test/file.expected.out index dcfd7e8d..446a1feb 100644 --- a/test/file.expected.out +++ b/test/file.expected.out @@ -4,6 +4,7 @@ "tactic": "exact rfl", "proofState": 0, "pos": {"line": 5, "column": 29}, + "parentDecl": "h", "goals": "⊢ f + g = 39", "endPos": {"line": 5, "column": 38}}], "env": 0} diff --git a/test/goal_branching.expected.out b/test/goal_branching.expected.out index cfebf5cf..9d6de033 100644 --- a/test/goal_branching.expected.out +++ b/test/goal_branching.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 53}, - "goal": "⊢ 1 = 1 ∧ 2 = 2 ∧ 3 = 3", + "parentDecl": "branching_test", + "goals": ["⊢ 1 = 1 ∧ 2 = 2 ∧ 3 = 3"], "endPos": {"line": 1, "column": 58}}], "messages": [{"severity": "warning", diff --git a/test/goal_branching.in b/test/goal_branching.in index b6389527..aec374aa 100644 --- a/test/goal_branching.in +++ b/test/goal_branching.in @@ -1,4 +1,4 @@ -{"cmd" : "theorem branching_test : 1 = 1 ∧ 2 = 2 ∧ 3 = 3 := by sorry"} +{"cmd" : "theorem branching_test : 1 = 1 ∧ 2 = 2 ∧ 3 = 3 := by sorry", "sorries" : "individual"} {"tactic": "constructor", "proofState": 0} diff --git a/test/have_by_sorry.expected.out b/test/have_by_sorry.expected.out index c8dba09c..33129473 100644 --- a/test/have_by_sorry.expected.out +++ b/test/have_by_sorry.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 2, "column": 23}, - "goal": "x : Int\n⊢ x = 1", + "parentDecl": "foo", + "goals": ["x : Int\n⊢ x = 1"], "endPos": {"line": 2, "column": 28}}], "messages": [{"severity": "error", @@ -13,7 +14,8 @@ {"sorries": [{"proofState": 1, "pos": {"line": 1, "column": 36}, - "goal": "x : Int\n⊢ x = x", + "parentDecl": "foo", + "goals": ["x : Int\n⊢ x = x"], "endPos": {"line": 1, "column": 41}}], "messages": [{"severity": "warning", diff --git a/test/have_by_sorry.in b/test/have_by_sorry.in index adb2b520..af6f7c10 100644 --- a/test/have_by_sorry.in +++ b/test/have_by_sorry.in @@ -1,6 +1,6 @@ -{"cmd": "theorem foo (x : Int) : x = x := by\n have h : x = 1 := by sorry"} +{"cmd": "theorem foo (x : Int) : x = x := by\n have h : x = 1 := by sorry", "sorries": "individual"} -{"cmd": "theorem foo (x : Int) : x = x := by sorry"} +{"cmd": "theorem foo (x : Int) : x = x := by sorry", "sorries": "individual"} -{"proofState" : 0, "tactic": "have h : x = 1 := by sorry"} +{"proofState" : 0, "tactic": "have h : x = 1 := by sorry", "sorries": "individual"} diff --git a/test/invalid_tactic.expected.out b/test/invalid_tactic.expected.out index d22e4698..ee390307 100644 --- a/test/invalid_tactic.expected.out +++ b/test/invalid_tactic.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 43}, - "goal": "x : Nat\n⊢ x = x", + "parentDecl": "my_theorem", + "goals": ["x : Nat\n⊢ x = x"], "endPos": {"line": 1, "column": 48}}], "messages": [{"severity": "warning", diff --git a/test/invalid_tactic.in b/test/invalid_tactic.in index df92192c..64887fd9 100644 --- a/test/invalid_tactic.in +++ b/test/invalid_tactic.in @@ -1,3 +1,3 @@ -{"cmd": "theorem my_theorem (x : Nat) : x = x := by sorry"} +{"cmd": "theorem my_theorem (x : Nat) : x = x := by sorry", "sorries": "individual"} {"tactic": "exact my_fake_premise", "proofState": 0} diff --git a/test/name_generator.expected.out b/test/name_generator.expected.out index 1ed48ad9..34483e57 100644 --- a/test/name_generator.expected.out +++ b/test/name_generator.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 2, "column": 45}, - "goal": "x : Int\nh0 : x > 0\n⊢ False", + "parentDecl": "_example", + "goals": ["x : Int\nh0 : x > 0\n⊢ False"], "endPos": {"line": 2, "column": 50}}], "messages": [{"severity": "warning", diff --git a/test/name_generator.in b/test/name_generator.in index 232c37da..4fe6a58d 100644 --- a/test/name_generator.in +++ b/test/name_generator.in @@ -1,4 +1,4 @@ -{"cmd": "set_option trace.Meta.Tactic.simp true\nexample {x : Int} (h0 : x > 0) : False := by sorry"} +{"cmd": "set_option trace.Meta.Tactic.simp true\nexample {x : Int} (h0 : x > 0) : False := by sorry", "sorries": "individual"} {"tactic": "have h : x > 0 := by sorry", "proofState": 0} diff --git a/test/no_goal_sorry_2.expected.out b/test/no_goal_sorry_2.expected.out index 31e74936..f509f934 100644 --- a/test/no_goal_sorry_2.expected.out +++ b/test/no_goal_sorry_2.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 2, "column": 2}, - "goal": "⊢ True", + "parentDecl": "_example", + "goals": ["⊢ True"], "endPos": {"line": 2, "column": 7}}], "messages": [{"severity": "error", diff --git a/test/no_goal_sorry_2.in b/test/no_goal_sorry_2.in index 07211903..5d3be350 100644 --- a/test/no_goal_sorry_2.in +++ b/test/no_goal_sorry_2.in @@ -1 +1 @@ -{"cmd" : "example : True := by\n sorry\n sorry"} +{"cmd" : "example : True := by\n sorry\n sorry", "sorries": "individual"} diff --git a/test/pickle_open_scoped.expected.out b/test/pickle_open_scoped.expected.out index df23507a..c6f22edd 100644 --- a/test/pickle_open_scoped.expected.out +++ b/test/pickle_open_scoped.expected.out @@ -5,7 +5,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 22}, - "goal": "⊢ ◾", + "parentDecl": "_example", + "goals": ["⊢ ◾"], "endPos": {"line": 1, "column": 27}}], "messages": [{"severity": "warning", diff --git a/test/pickle_open_scoped.in b/test/pickle_open_scoped.in index dafcbc65..e13fb5e8 100644 --- a/test/pickle_open_scoped.in +++ b/test/pickle_open_scoped.in @@ -2,7 +2,7 @@ {"cmd": "open Lean.Compiler", "env": 0} -{"cmd": "unsafe example : ◾ := sorry", "env": 1} +{"cmd": "unsafe example : ◾ := sorry", "env": 1, "sorries": "individual"} {"pickleTo": "test/f.olean", "env": 1} diff --git a/test/pickle_open_scoped_2.expected.out b/test/pickle_open_scoped_2.expected.out index f21692d2..9aee3bd1 100644 --- a/test/pickle_open_scoped_2.expected.out +++ b/test/pickle_open_scoped_2.expected.out @@ -3,7 +3,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 22}, - "goal": "⊢ ◾", + "parentDecl": "_example", + "goals": ["⊢ ◾"], "endPos": {"line": 1, "column": 27}}], "messages": [{"severity": "warning", diff --git a/test/pickle_open_scoped_2.in b/test/pickle_open_scoped_2.in index 6b587fc0..8177a8b4 100644 --- a/test/pickle_open_scoped_2.in +++ b/test/pickle_open_scoped_2.in @@ -1,3 +1,3 @@ {"unpickleEnvFrom": "test/f.olean"} -{"cmd": "unsafe example : ◾ := sorry", "env": 0} +{"cmd": "unsafe example : ◾ := sorry", "env": 0, "sorries": "individual"} diff --git a/test/pickle_proof_state_1.expected.out b/test/pickle_proof_state_1.expected.out index 238b74c9..e902b67d 100644 --- a/test/pickle_proof_state_1.expected.out +++ b/test/pickle_proof_state_1.expected.out @@ -3,7 +3,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 18}, - "goal": "⊢ Nat", + "parentDecl": "f", + "goals": ["⊢ Nat"], "endPos": {"line": 1, "column": 23}}], "messages": [{"severity": "warning", diff --git a/test/pickle_proof_state_1.in b/test/pickle_proof_state_1.in index 1b1afdf5..0ea70a0d 100644 --- a/test/pickle_proof_state_1.in +++ b/test/pickle_proof_state_1.in @@ -1,6 +1,6 @@ {"cmd" : "import Lean"} -{"cmd" : "def f : Nat := by sorry", "env": 0} +{"cmd" : "def f : Nat := by sorry", "env": 0, "sorries": "individual"} {"pickleTo": "test/c.olean", "proofState": 0} diff --git a/test/pickle_proof_state_env.expected.out b/test/pickle_proof_state_env.expected.out index 238b74c9..e902b67d 100644 --- a/test/pickle_proof_state_env.expected.out +++ b/test/pickle_proof_state_env.expected.out @@ -3,7 +3,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 18}, - "goal": "⊢ Nat", + "parentDecl": "f", + "goals": ["⊢ Nat"], "endPos": {"line": 1, "column": 23}}], "messages": [{"severity": "warning", diff --git a/test/pickle_proof_state_env.in b/test/pickle_proof_state_env.in index fdd99f75..292d9b1d 100644 --- a/test/pickle_proof_state_env.in +++ b/test/pickle_proof_state_env.in @@ -1,6 +1,6 @@ {"cmd" : "import Lean"} -{"cmd" : "def f : Nat := by sorry", "env": 0} +{"cmd" : "def f : Nat := by sorry", "env": 0, "sorries": "individual"} {"pickleTo": "test/c.olean", "proofState": 0} diff --git a/test/proof_branching.expected.out b/test/proof_branching.expected.out index bfea811d..2218e577 100644 --- a/test/proof_branching.expected.out +++ b/test/proof_branching.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 75}, - "goal": "p q r : Prop\nh1 : p ∧ q\nh2 : q → r\n⊢ p ∧ r", + "parentDecl": "complex_and", + "goals": ["p q r : Prop\nh1 : p ∧ q\nh2 : q → r\n⊢ p ∧ r"], "endPos": {"line": 1, "column": 80}}], "messages": [{"severity": "warning", diff --git a/test/proof_branching.in b/test/proof_branching.in index 0c32a386..04549ae4 100644 --- a/test/proof_branching.in +++ b/test/proof_branching.in @@ -1,4 +1,4 @@ -{"cmd": "theorem complex_and (p q r : Prop) (h1 : p ∧ q) (h2 : q → r) : p ∧ r := by sorry"} +{"cmd": "theorem complex_and (p q r : Prop) (h1 : p ∧ q) (h2 : q → r) : p ∧ r := by sorry", "sorries": "individual"} {"tactic": "apply And.intro", "proofState": 0} diff --git a/test/proof_branching2.expected.out b/test/proof_branching2.expected.out index 1bcd8e1e..01d5e055 100644 --- a/test/proof_branching2.expected.out +++ b/test/proof_branching2.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 43}, - "goal": "p q : Prop\n⊢ p ∧ q → q ∧ p", + "parentDecl": "_example", + "goals": ["p q : Prop\n⊢ p ∧ q → q ∧ p"], "endPos": {"line": 1, "column": 48}}], "messages": [{"severity": "warning", diff --git a/test/proof_branching2.in b/test/proof_branching2.in index 0b25f70e..35ad189d 100644 --- a/test/proof_branching2.in +++ b/test/proof_branching2.in @@ -1,4 +1,4 @@ -{"cmd": "example (p q : Prop) : p ∧ q → q ∧ p := by sorry"} +{"cmd": "example (p q : Prop) : p ∧ q → q ∧ p := by sorry", "sorries": "individual"} {"tactic": "intro h", "proofState": 0} diff --git a/test/proof_step.expected.out b/test/proof_step.expected.out index 013889b6..628df81b 100644 --- a/test/proof_step.expected.out +++ b/test/proof_step.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 18}, - "goal": "⊢ Nat", + "parentDecl": "f", + "goals": ["⊢ Nat"], "endPos": {"line": 1, "column": 23}}], "messages": [{"severity": "warning", diff --git a/test/proof_step.in b/test/proof_step.in index a0b5d533..a1393bd0 100644 --- a/test/proof_step.in +++ b/test/proof_step.in @@ -1,4 +1,4 @@ -{"cmd" : "def f : Nat := by sorry"} +{"cmd" : "def f : Nat := by sorry", "sorries" : "individual"} {"tactic": "apply Int.natAbs", "proofState": 0} diff --git a/test/proof_transitivity.expected.out b/test/proof_transitivity.expected.out index 45f4b082..cb113dfb 100644 --- a/test/proof_transitivity.expected.out +++ b/test/proof_transitivity.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 62}, - "goal": "x y z : Nat\nh1 : x = y\nh2 : y = z\n⊢ x = z", + "parentDecl": "_example", + "goals": ["x y z : Nat\nh1 : x = y\nh2 : y = z\n⊢ x = z"], "endPos": {"line": 1, "column": 67}}], "messages": [{"severity": "warning", @@ -15,7 +16,8 @@ {"sorries": [{"proofState": 2, "pos": {"line": 1, "column": 64}, - "goal": "f : Nat → Nat\nn : Nat\nh : n = 3\n⊢ f n = f 3", + "parentDecl": "_example", + "goals": ["f : Nat → Nat\nn : Nat\nh : n = 3\n⊢ f n = f 3"], "endPos": {"line": 1, "column": 69}}], "messages": [{"severity": "warning", diff --git a/test/proof_transitivity.in b/test/proof_transitivity.in index 9245305c..aca370f0 100644 --- a/test/proof_transitivity.in +++ b/test/proof_transitivity.in @@ -1,8 +1,8 @@ -{"cmd": "example (x y z : Nat) (h1 : x = y) (h2 : y = z) : x = z := by sorry"} +{"cmd": "example (x y z : Nat) (h1 : x = y) (h2 : y = z) : x = z := by sorry", "sorries": "individual"} {"tactic": "exact Eq.trans h1 h2", "proofState": 0} -{"cmd": "example (f : Nat → Nat) (n : Nat) (h : n = 3) : f n = f 3 := by sorry"} +{"cmd": "example (f : Nat → Nat) (n : Nat) (h : n = 3) : f n = f 3 := by sorry", "sorries": "individual"} {"tactic": "exact congrArg f h", "proofState": 2} diff --git a/test/readme.expected.out b/test/readme.expected.out index 7ffa1109..a6e854a0 100644 --- a/test/readme.expected.out +++ b/test/readme.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 29}, - "goal": "x : Unit\n⊢ Nat", + "parentDecl": "f", + "goals": ["x : Unit\n⊢ Nat"], "endPos": {"line": 1, "column": 34}}], "messages": [{"severity": "warning", diff --git a/test/readme.in b/test/readme.in index a13635c9..2116ad7e 100644 --- a/test/readme.in +++ b/test/readme.in @@ -1,4 +1,4 @@ -{"cmd" : "def f (x : Unit) : Nat := by sorry"} +{"cmd" : "def f (x : Unit) : Nat := by sorry", "sorries" : "individual"} {"tactic": "apply Int.natAbs", "proofState": 0} diff --git a/test/root_goals.expected.out b/test/root_goals.expected.out index 053aeeac..533106fe 100644 --- a/test/root_goals.expected.out +++ b/test/root_goals.expected.out @@ -1,12 +1,12 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 17}, - "goal": "⊢ 1 = 1", - "endPos": {"line": 1, "column": 17}}, + "parentDecl": "_example", + "goals": ["⊢ 1 = 1"]}, {"proofState": 1, "pos": {"line": 5, "column": 22}, - "goal": "⊢ 1 + 1 = 2", - "endPos": {"line": 5, "column": 22}}], + "parentDecl": "bb", + "goals": ["⊢ 1 + 1 = 2"]}], "messages": [{"severity": "info", "pos": {"line": 3, "column": 2}, diff --git a/test/root_goals.in b/test/root_goals.in index 487ad72a..d5392ae8 100644 --- a/test/root_goals.in +++ b/test/root_goals.in @@ -1,4 +1,4 @@ -{"cmd": "example : 1=1 := by\n skip\n exact?\n\ntheorem bb : 1+1=2 := by rfl", "rootGoals": true} +{"cmd": "example : 1=1 := by\n skip\n exact?\n\ntheorem bb : 1+1=2 := by rfl", "sorries": "rootGoals"} {"proofState" : 0, "tactic": "rfl"} diff --git a/test/self_proof_apply_check.expected.out b/test/self_proof_apply_check.expected.out index ba526f4f..f7cf74f6 100644 --- a/test/self_proof_apply_check.expected.out +++ b/test/self_proof_apply_check.expected.out @@ -9,7 +9,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 22}, - "goal": "⊢ False", + "parentDecl": "ex", + "goals": ["⊢ False"], "endPos": {"line": 1, "column": 27}}], "messages": [{"severity": "warning", diff --git a/test/self_proof_apply_check.in b/test/self_proof_apply_check.in index f01ccc4c..0e680a23 100644 --- a/test/self_proof_apply_check.in +++ b/test/self_proof_apply_check.in @@ -1,5 +1,5 @@ {"cmd": "theorem ex : False := by apply ex"} -{"cmd": "theorem ex : False := sorry"} +{"cmd": "theorem ex : False := sorry", "sorries": "individual"} {"proofState": 0, "tactic": "apply ex"} diff --git a/test/self_proof_check.expected.out b/test/self_proof_check.expected.out index 48253d70..8af7cd48 100644 --- a/test/self_proof_check.expected.out +++ b/test/self_proof_check.expected.out @@ -9,7 +9,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 22}, - "goal": "⊢ False", + "parentDecl": "ex", + "goals": ["⊢ False"], "endPos": {"line": 1, "column": 27}}], "messages": [{"severity": "warning", @@ -24,7 +25,8 @@ {"sorries": [{"proofState": 1, "pos": {"line": 1, "column": 25}, - "goal": "⊢ False", + "parentDecl": "ex", + "goals": ["⊢ False"], "endPos": {"line": 1, "column": 30}}], "messages": [{"severity": "warning", @@ -51,12 +53,14 @@ "tactic": "sorry", "proofState": 3, "pos": {"line": 1, "column": 25}, + "parentDecl": "ex", "goals": "⊢ False", "endPos": {"line": 1, "column": 30}}], "sorries": [{"proofState": 2, "pos": {"line": 1, "column": 25}, - "goal": "⊢ False", + "parentDecl": "ex", + "goals": ["⊢ False"], "endPos": {"line": 1, "column": 30}}], "messages": [{"severity": "warning", @@ -70,13 +74,9 @@ {"sorries": [{"proofState": 4, - "pos": {"line": 1, "column": 25}, - "goal": "⊢ False", - "endPos": {"line": 1, "column": 30}}, - {"proofState": 5, "pos": {"line": 1, "column": 22}, - "goal": "⊢ False", - "endPos": {"line": 1, "column": 22}}], + "parentDecl": "ex", + "goals": ["⊢ False"]}], "messages": [{"severity": "warning", "pos": {"line": 1, "column": 8}, diff --git a/test/self_proof_check.in b/test/self_proof_check.in index 216d80f6..bd521adf 100644 --- a/test/self_proof_check.in +++ b/test/self_proof_check.in @@ -1,18 +1,18 @@ {"cmd": "theorem ex : False := by exact?"} -{"cmd": "theorem ex : False := sorry"} +{"cmd": "theorem ex : False := sorry", "sorries": "individual"} {"proofState": 0, "tactic": "exact?"} -{"cmd": "theorem ex : False := by sorry"} +{"cmd": "theorem ex : False := by sorry", "sorries": "individual"} {"proofState": 1, "tactic": "exact?"} -{"cmd": "theorem ex : False := by sorry", "allTactics": true} +{"cmd": "theorem ex : False := by sorry", "allTactics": true, "sorries": "individual"} {"proofState": 3, "tactic": "exact?"} -{"cmd": "theorem ex : False := by sorry", "rootGoals": true} +{"cmd": "theorem ex : False := by sorry", "sorries": "rootGoals"} -{"proofState": 5, "tactic": "exact?"} +{"proofState": 4, "tactic": "exact?"} diff --git a/test/self_proof_exact_check.expected.out b/test/self_proof_exact_check.expected.out index ba526f4f..f7cf74f6 100644 --- a/test/self_proof_exact_check.expected.out +++ b/test/self_proof_exact_check.expected.out @@ -9,7 +9,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 22}, - "goal": "⊢ False", + "parentDecl": "ex", + "goals": ["⊢ False"], "endPos": {"line": 1, "column": 27}}], "messages": [{"severity": "warning", diff --git a/test/self_proof_exact_check.in b/test/self_proof_exact_check.in index aa1dac4c..8e1acfea 100644 --- a/test/self_proof_exact_check.in +++ b/test/self_proof_exact_check.in @@ -1,5 +1,5 @@ {"cmd": "theorem ex : False := by exact ex"} -{"cmd": "theorem ex : False := sorry"} +{"cmd": "theorem ex : False := sorry", "sorries": "individual"} {"proofState": 0, "tactic": "exact ex"} diff --git a/test/self_proof_rw.expected.out b/test/self_proof_rw.expected.out index f424072d..9cfb3d41 100644 --- a/test/self_proof_rw.expected.out +++ b/test/self_proof_rw.expected.out @@ -9,7 +9,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 39}, - "goal": "⊢ 1 = 0", + "parentDecl": "self_application", + "goals": ["⊢ 1 = 0"], "endPos": {"line": 1, "column": 44}}], "messages": [{"severity": "warning", diff --git a/test/self_proof_rw.in b/test/self_proof_rw.in index 945894ef..2a7eb5d9 100644 --- a/test/self_proof_rw.in +++ b/test/self_proof_rw.in @@ -1,5 +1,5 @@ {"cmd": "theorem self_application : 1 = 0 := by rw [self_application]"} -{"cmd": "theorem self_application : 1 = 0 := by sorry"} +{"cmd": "theorem self_application : 1 = 0 := by sorry", "sorries": "individual"} {"proofState": 0, "tactic": "rw [self_application]"} diff --git a/test/sketch_tactic.expected.out b/test/sketch_tactic.expected.out index b7d32be4..618d461c 100644 --- a/test/sketch_tactic.expected.out +++ b/test/sketch_tactic.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 70}, - "goal": "⊢ ∀ (n m : Nat), n + m = m + n", + "parentDecl": "add_comm_proved_formal_sketch", + "goals": ["⊢ ∀ (n m : Nat), n + m = m + n"], "endPos": {"line": 1, "column": 75}}], "messages": [{"severity": "warning", diff --git a/test/sketch_tactic.in b/test/sketch_tactic.in index d99b8051..db2dd111 100644 --- a/test/sketch_tactic.in +++ b/test/sketch_tactic.in @@ -1,4 +1,4 @@ -{"cmd": "theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry"} +{"cmd": "theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry", "sorries": "individual"} {"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} diff --git a/test/sorry_hypotheses.expected.out b/test/sorry_hypotheses.expected.out index 5fea7fd3..96546942 100644 --- a/test/sorry_hypotheses.expected.out +++ b/test/sorry_hypotheses.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 36}, - "goal": "x : Int\n⊢ x = x", + "parentDecl": "foo", + "goals": ["x : Int\n⊢ x = x"], "endPos": {"line": 1, "column": 41}}], "messages": [{"severity": "warning", diff --git a/test/sorry_hypotheses.in b/test/sorry_hypotheses.in index 515c15cc..0f6e2899 100644 --- a/test/sorry_hypotheses.in +++ b/test/sorry_hypotheses.in @@ -1,4 +1,4 @@ -{"cmd": "theorem foo (x : Int) : x = x := by sorry"} +{"cmd": "theorem foo (x : Int) : x = x := by sorry", "sorries": "individual"} {"proofState" : 0, "tactic": "have h : x = 1 := sorry"} diff --git a/test/tactic_have_branching.expected.out b/test/tactic_have_branching.expected.out index 07b9c2db..5c8798c4 100644 --- a/test/tactic_have_branching.expected.out +++ b/test/tactic_have_branching.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 22}, - "goal": "⊢ 1 = 1", + "parentDecl": "_example", + "goals": ["⊢ 1 = 1"], "endPos": {"line": 1, "column": 27}}], "messages": [{"severity": "warning", diff --git a/test/tactic_have_branching.in b/test/tactic_have_branching.in index 721cb9fa..47259fbb 100644 --- a/test/tactic_have_branching.in +++ b/test/tactic_have_branching.in @@ -1,4 +1,4 @@ -{"cmd": "example : 1 = 1 := by sorry"} +{"cmd": "example : 1 = 1 := by sorry", "sorries": "individual"} {"tactic": "rfl", "proofState": 0} diff --git a/test/tactic_mode_sorry.expected.out b/test/tactic_mode_sorry.expected.out index 341b6969..50edb259 100644 --- a/test/tactic_mode_sorry.expected.out +++ b/test/tactic_mode_sorry.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 18}, - "goal": "⊢ Nat", + "parentDecl": "f", + "goals": ["⊢ Nat"], "endPos": {"line": 1, "column": 23}}], "messages": [{"severity": "warning", diff --git a/test/tactic_mode_sorry.in b/test/tactic_mode_sorry.in index 32465b9c..b9b1197b 100644 --- a/test/tactic_mode_sorry.in +++ b/test/tactic_mode_sorry.in @@ -1,3 +1,3 @@ -{"cmd": "def f : Nat := by sorry"} +{"cmd": "def f : Nat := by sorry", "sorries": "individual"} {"proofState": 0, "tactic": "sorry"} diff --git a/test/tactic_sorry.expected.out b/test/tactic_sorry.expected.out index 0394d4f8..5644af1a 100644 --- a/test/tactic_sorry.expected.out +++ b/test/tactic_sorry.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 18}, - "goal": "⊢ Nat", + "parentDecl": "f", + "goals": ["⊢ Nat"], "endPos": {"line": 1, "column": 23}}], "messages": [{"severity": "warning", diff --git a/test/tactic_sorry.in b/test/tactic_sorry.in index 7e9e61da..ce7c5872 100644 --- a/test/tactic_sorry.in +++ b/test/tactic_sorry.in @@ -1 +1 @@ -{"cmd": "def f : Nat := by sorry"} +{"cmd": "def f : Nat := by sorry", "sorries": "individual"} diff --git a/test/term_sorry.expected.out b/test/term_sorry.expected.out index ab332e35..be9674e1 100644 --- a/test/term_sorry.expected.out +++ b/test/term_sorry.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 15}, - "goal": "⊢ Nat", + "parentDecl": "f", + "goals": ["⊢ Nat"], "endPos": {"line": 1, "column": 20}}], "messages": [{"severity": "warning", diff --git a/test/term_sorry.in b/test/term_sorry.in index 1bf62faa..91d2ac25 100644 --- a/test/term_sorry.in +++ b/test/term_sorry.in @@ -1 +1 @@ -{"cmd": "def f : Nat := sorry"} +{"cmd": "def f : Nat := sorry", "sorries": "individual"} diff --git a/test/trace_simp.expected.out b/test/trace_simp.expected.out index 0f3bbba7..e916edf1 100644 --- a/test/trace_simp.expected.out +++ b/test/trace_simp.expected.out @@ -15,7 +15,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 23}, - "goal": "⊢ f = 37", + "parentDecl": "_example", + "goals": ["⊢ f = 37"], "endPos": {"line": 1, "column": 28}}], "messages": [{"severity": "warning", diff --git a/test/trace_simp.in b/test/trace_simp.in index 7e2a4a2e..583fc5d3 100644 --- a/test/trace_simp.in +++ b/test/trace_simp.in @@ -6,7 +6,7 @@ {"cmd": "example : f = 37 := by simp", "env": 2} -{"cmd": "example : f = 37 := by sorry", "env": 2} +{"cmd": "example : f = 37 := by sorry", "env": 2, "sorries": "individual"} {"tactic": "trace \"37\"", "proofState": 0} diff --git a/test/unknown_proof_state.expected.out b/test/unknown_proof_state.expected.out index ee52464f..9f1dfc33 100644 --- a/test/unknown_proof_state.expected.out +++ b/test/unknown_proof_state.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 18}, - "goal": "⊢ Nat", + "parentDecl": "f", + "goals": ["⊢ Nat"], "endPos": {"line": 1, "column": 23}}], "messages": [{"severity": "warning", diff --git a/test/unknown_proof_state.in b/test/unknown_proof_state.in index bdd1a68f..ef2f8daf 100644 --- a/test/unknown_proof_state.in +++ b/test/unknown_proof_state.in @@ -1,3 +1,3 @@ -{"cmd" : "def f : Nat := by sorry"} +{"cmd" : "def f : Nat := by sorry", "sorries" : "individual"} {"tactic": "exact 42", "proofState": 1} diff --git a/test/unknown_tactic.expected.out b/test/unknown_tactic.expected.out index 7e55103b..c016420c 100644 --- a/test/unknown_tactic.expected.out +++ b/test/unknown_tactic.expected.out @@ -1,7 +1,8 @@ {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 18}, - "goal": "⊢ Nat", + "parentDecl": "f", + "goals": ["⊢ Nat"], "endPos": {"line": 1, "column": 23}}], "messages": [{"severity": "warning", diff --git a/test/unknown_tactic.in b/test/unknown_tactic.in index d1af2492..a8f771b3 100644 --- a/test/unknown_tactic.in +++ b/test/unknown_tactic.in @@ -1,3 +1,3 @@ -{"cmd" : "def f : Nat := by sorry"} +{"cmd" : "def f : Nat := by sorry", "sorries" : "individual"} {"tactic": "exat 42", "proofState": 0} diff --git a/test/variables.expected.out b/test/variables.expected.out index d67e84bd..7cab6396 100644 --- a/test/variables.expected.out +++ b/test/variables.expected.out @@ -11,8 +11,9 @@ {"sorries": [{"proofState": 0, "pos": {"line": 3, "column": 2}, - "goal": - "x y : Nat\nf : Nat → Nat\nh0 : f 5 = 3\nh1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y))\n⊢ ∃ k, f 2015 = k", + "parentDecl": "problem", + "goals": + ["x y : Nat\nf : Nat → Nat\nh0 : f 5 = 3\nh1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y))\n⊢ ∃ k, f 2015 = k"], "endPos": {"line": 3, "column": 7}}], "messages": [{"severity": "warning", diff --git a/test/variables.in b/test/variables.in index 4682e37f..e699263a 100644 --- a/test/variables.in +++ b/test/variables.in @@ -2,4 +2,4 @@ {"cmd": "variable (f : Nat → Nat)", "env": 0} -{"cmd": "theorem problem (h0 : f 5 = 3) (h1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y))) :\n ∃ (k : Nat), f 2015 = k := by\n sorry", "env": 1} +{"cmd": "theorem problem (h0 : f 5 = 3) (h1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y))) :\n ∃ (k : Nat), f 2015 = k := by\n sorry", "env": 1, "sorries": "individual"} From 6c4f87adc127bcab42727af8b1848ec1781b00ec Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 4 Jul 2025 12:19:47 +0200 Subject: [PATCH 6/8] Add sketch test --- test/sketch_file.expected.out | 49 +++++++++++++++++++++++++++++++++++ test/sketch_file.in | 9 +++++++ test/sketch_file.lean | 11 ++++++++ 3 files changed, 69 insertions(+) create mode 100644 test/sketch_file.expected.out create mode 100644 test/sketch_file.in create mode 100644 test/sketch_file.lean diff --git a/test/sketch_file.expected.out b/test/sketch_file.expected.out new file mode 100644 index 00000000..ab737aeb --- /dev/null +++ b/test/sketch_file.expected.out @@ -0,0 +1,49 @@ +{"sorries": + [{"proofState": 0, + "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\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"], + "endPos": {"line": 8, "column": 24}}, + {"proofState": 1, + "pos": {"line": 11, "column": 49}, + "parentDecl": "add_rfl2", + "goals": ["⊢ ∀ (n m : Nat), n + m = n + m"], + "endPos": {"line": 11, "column": 57}}], + "messages": + [{"severity": "warning", + "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}, + "data": "declaration uses 'sorry'"}], + "env": 0} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 2, + "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"]} + +{"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"]} + +{"proofStatus": "Incomplete: open goals remain", + "proofState": 4, + "goals": ["m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m"]} + +{"proofStatus": "Completed", "proofState": 5, "goals": []} + diff --git a/test/sketch_file.in b/test/sketch_file.in new file mode 100644 index 00000000..44dc8e8d --- /dev/null +++ b/test/sketch_file.in @@ -0,0 +1,9 @@ +{"path": "test/sketch_file.lean", "sorries": "grouped"} + +{"tactic": "apply Nat.zero_add", "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} diff --git a/test/sketch_file.lean b/test/sketch_file.lean new file mode 100644 index 00000000..2301763b --- /dev/null +++ b/test/sketch_file.lean @@ -0,0 +1,11 @@ +theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by + intros n m + induction n with + | zero => + have h_base: 0 + m = m := sorry + have h_symm: m + 0 = m := sorry + sorry + | succ n ih => sorry + +theorem add_rfl : ∀ n m : Nat, n + m = n + m := by intros; rfl +theorem add_rfl2 : ∀ n m : Nat, n + m = n + m := by sorry From de070323e9e79d539f8c3fd01a8f96c841edb6d0 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 4 Jul 2025 12:19:47 +0200 Subject: [PATCH 7/8] Update readme --- README.md | 8 +++++--- test/sketch_file.expected.out | 2 ++ test/sketch_file.in | 2 ++ 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index fb7fe1bb..3455eef2 100644 --- a/README.md +++ b/README.md @@ -44,7 +44,8 @@ Example output: {"sorries": [{"pos": {"line": 1, "column": 18}, "endPos": {"line": 1, "column": 23}, - "goal": "⊢ Nat", + "parentDecl": "h", + "goals": ["⊢ Nat"], "proofState": 0}], "messages": [{"severity": "error", @@ -92,12 +93,13 @@ and then use the `proofState` index returned for each `sorry`. Example usage: ```json -{"cmd" : "def f (x : Unit) : Nat := by sorry"} +{"cmd" : "def f (x : Unit) : Nat := by sorry", "sorries": "individual"} {"sorries": [{"proofState": 0, "pos": {"line": 1, "column": 29}, - "goal": "x : Unit\n⊢ Nat", + "parentDecl": "f", + "goals": ["x : Unit\n⊢ Nat"], "endPos": {"line": 1, "column": 34}}], "messages": [{"severity": "warning", diff --git a/test/sketch_file.expected.out b/test/sketch_file.expected.out index ab737aeb..56d1d663 100644 --- a/test/sketch_file.expected.out +++ b/test/sketch_file.expected.out @@ -47,3 +47,5 @@ {"proofStatus": "Completed", "proofState": 5, "goals": []} +{"proofStatus": "Completed", "proofState": 6, "goals": []} + diff --git a/test/sketch_file.in b/test/sketch_file.in index 44dc8e8d..ba89f9ed 100644 --- a/test/sketch_file.in +++ b/test/sketch_file.in @@ -7,3 +7,5 @@ {"tactic": "rw [Nat.succ_add, Nat.add_succ, ih]", "proofState": 3} {"tactic": "apply Nat.add_zero", "proofState": 4} + +{"tactic": "(\nintros; rfl)", "proofState": 1} From a1de50b48654ad893190e61f05b79f835c075256 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 4 Jul 2025 12:19:47 +0200 Subject: [PATCH 8/8] Fix a few tests --- test/all_tactics-20250622.expected.out | 1 + test/app_type_mismatch2.expected.out | 6 ++++-- test/by_cases.expected.out | 2 +- test/file2.expected.out | 1 + test/line_breaks.expected.out | 3 ++- test/line_breaks.in | 2 +- test/sketch_file.expected.out | 14 +++++--------- test/sketch_file.in | 4 ++-- test/sketch_tactic.expected.out | 16 +++++++++------- test/sketch_tactic.in | 7 +++---- 10 files changed, 29 insertions(+), 27 deletions(-) diff --git a/test/all_tactics-20250622.expected.out b/test/all_tactics-20250622.expected.out index 3b16cd5b..4124bd0f 100644 --- a/test/all_tactics-20250622.expected.out +++ b/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} diff --git a/test/app_type_mismatch2.expected.out b/test/app_type_mismatch2.expected.out index 37f3fd78..63127c71 100644 --- a/test/app_type_mismatch2.expected.out +++ b/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": []} diff --git a/test/by_cases.expected.out b/test/by_cases.expected.out index 1e99b39a..7dc6574b 100644 --- a/test/by_cases.expected.out +++ b/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"]} diff --git a/test/file2.expected.out b/test/file2.expected.out index 0fe4f6e7..fdda1d31 100644 --- a/test/file2.expected.out +++ b/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} diff --git a/test/line_breaks.expected.out b/test/line_breaks.expected.out index d6e980af..24b76f61 100644 --- a/test/line_breaks.expected.out +++ b/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", diff --git a/test/line_breaks.in b/test/line_breaks.in index 6ac457a1..7e6a776f 100644 --- a/test/line_breaks.in +++ b/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 diff --git a/test/sketch_file.expected.out b/test/sketch_file.expected.out index 56d1d663..12aa7732 100644 --- a/test/sketch_file.expected.out +++ b/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": []} diff --git a/test/sketch_file.in b/test/sketch_file.in index ba89f9ed..d8010b96 100644 --- a/test/sketch_file.in +++ b/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} diff --git a/test/sketch_tactic.expected.out b/test/sketch_tactic.expected.out index 618d461c..db2cc091 100644 --- a/test/sketch_tactic.expected.out +++ b/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": []} diff --git a/test/sketch_tactic.in b/test/sketch_tactic.in index db2dd111..b789c451 100644 --- a/test/sketch_tactic.in +++ b/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}