From 8684c8966de808661e100330d11b59865de82347 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 2 Feb 2024 16:49:20 +1100 Subject: [PATCH] fix: NameGenerator bug --- REPL/Lean/InfoTree.lean | 6 ++-- REPL/Main.lean | 9 ++++-- REPL/Snapshots.lean | 2 +- test/name_generator.expected.out | 49 ++++++++++++++++++++++++++++++++ test/name_generator.in | 18 ++++++++++++ test/unknown_tactic.expected.out | 2 +- 6 files changed, 79 insertions(+), 7 deletions(-) create mode 100644 test/name_generator.expected.out create mode 100644 test/name_generator.in diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean index 84bf93a..4f7e65e 100644 --- a/REPL/Lean/InfoTree.lean +++ b/REPL/Lean/InfoTree.lean @@ -189,7 +189,7 @@ def findSorryTermNodes (t : InfoTree) : List (TermInfo × ContextInfo) := inductive SorryType | tactic : MVarId → SorryType | term : LocalContext → Option Expr → SorryType - +#check MVarId /-- Finds all appearances of `sorry` in an `InfoTree`, reporting * the `ContextInfo` at that point, @@ -199,7 +199,9 @@ Finds all appearances of `sorry` in an `InfoTree`, reporting -/ def sorries (t : InfoTree) : List (ContextInfo × SorryType × Position × Position) := (t.findSorryTacticNodes.map fun ⟨i, ctx⟩ => - ({ ctx with mctx := i.mctxBefore }, .tactic i.goalsBefore.head!, stxRange ctx.fileMap i.stx)) ++ + let g := i.goalsBefore.head! + let ngen := { ctx.ngen with namePrefix := g.name } + ({ ctx with mctx := i.mctxBefore, ngen := ngen }, .tactic g, stxRange ctx.fileMap i.stx)) ++ (t.findSorryTermNodes.map fun ⟨i, ctx⟩ => (ctx, .term i.lctx i.expectedType?, stxRange ctx.fileMap i.stx)) diff --git a/REPL/Main.lean b/REPL/Main.lean index f8b255f..853706a 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -240,7 +240,7 @@ def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error) := do let proofState' ← proofState.runString s.tactic return .inl (← createProofStepReponse proofState' proofState) catch ex => - return .inr ⟨ex.toString⟩ + return .inr ⟨"Lean error:\n" ++ ex.toString⟩ end REPL @@ -272,7 +272,8 @@ inductive Input def parse (query : String) : IO Input := do let json := Json.parse query match json with - | .error e => throw <| IO.userError <| toString <| toJson (⟨e⟩ : Error) + | .error e => throw <| IO.userError <| toString <| toJson <| + (⟨"Could not parse JSON:\n" ++ e⟩ : Error) | .ok j => match fromJson? j with | .ok (r : REPL.ProofStep) => return .proofStep r | .error _ => match fromJson? j with @@ -285,7 +286,8 @@ def parse (query : String) : IO Input := do | .ok (r : REPL.UnpickleProofState) => return .unpickleProofSnapshot r | .error _ => match fromJson? j with | .ok (r : REPL.Command) => return .command r - | .error e => throw <| IO.userError <| toString <| toJson (⟨e⟩ : Error) + | .error e => throw <| IO.userError <| toString <| toJson <| + (⟨"Could not parse as a valid JSON command:\n" ++ e⟩ : Error) /-- Read-eval-print loop for Lean. -/ unsafe def repl : IO Unit := @@ -294,6 +296,7 @@ where loop : M IO Unit := do let query ← getLines if query = "" then return () + if query.startsWith "#" || query.startsWith "--" then loop else IO.println <| toString <| ← match ← parse query with | .command r => return toJson (← runCommand r) | .proofStep r => return toJson (← runProofStep r) diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index 8c83339..5a18974 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -182,7 +182,6 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot := /-- Pretty print the current goals in the `ProofSnapshot`. -/ def ppGoals (p : ProofSnapshot) : IO (List Format) := Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·) - /-- Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals. @@ -193,6 +192,7 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (goals : List MVarId) (types : List Expr := []) : IO ProofSnapshot := do ctx.runMetaM (lctx?.getD {}) do let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) + goals.head!.withContext do pure <| { coreState := ← getThe Core.State coreContext := ← readThe Core.Context diff --git a/test/name_generator.expected.out b/test/name_generator.expected.out new file mode 100644 index 0000000..33bb796 --- /dev/null +++ b/test/name_generator.expected.out @@ -0,0 +1,49 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 2, "column": 45}, + "goal": "x : Int\nh0 : x > 0\n⊢ False", + "endPos": {"line": 2, "column": 50}}], + "messages": + [{"severity": "warning", + "pos": {"line": 2, "column": 0}, + "endPos": {"line": 2, "column": 7}, + "data": "declaration uses 'sorry'"}], + "env": 0} + +{"sorries": [{"proofState": 1, "goal": "x : Int\nh0 : x > 0\n⊢ x > 0"}], + "proofState": 2, + "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]} + +{"proofState": 3, "goals": []} + +{"proofState": 4, "goals": []} + +{"traces": + ["[Meta.Tactic.simp.rewrite] of_eq_true (eq_true h0):1000, x > 0 ==> True"], + "proofState": 5, + "goals": []} + +{"traces": ["[Meta.Tactic.simp.rewrite] h0:1000, x > 0 ==> True"], + "proofState": 6, + "goals": []} + +{"traces": ["[Meta.Tactic.simp.rewrite] h0:1000, x > 0 ==> True"], + "proofState": 7, + "goals": []} + +{"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": []} + +{"proofState": 9, + "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": []} + diff --git a/test/name_generator.in b/test/name_generator.in new file mode 100644 index 0000000..232c37d --- /dev/null +++ b/test/name_generator.in @@ -0,0 +1,18 @@ +{"cmd": "set_option trace.Meta.Tactic.simp true\nexample {x : Int} (h0 : x > 0) : False := by sorry"} + +{"tactic": "have h : x > 0 := by sorry", "proofState": 0} + +{"tactic": "exact h0", "proofState": 1} + +{"tactic": "assumption", "proofState": 1} + +{"tactic": "simp only [of_eq_true (eq_true h0)]", "proofState": 1} + +{"tactic": "{ simp [h0] }", "proofState": 1} + +{"tactic": "{ simp (config := {memoize := false}) [h0] }", "proofState": 1} + +{"tactic": "{ rw (config := {}) [(show x = x from rfl)] }", "proofState": 1} + +{"tactic": "{ rw [(show x = x from rfl)] }", "proofState": 1} + diff --git a/test/unknown_tactic.expected.out b/test/unknown_tactic.expected.out index acef247..7e55103 100644 --- a/test/unknown_tactic.expected.out +++ b/test/unknown_tactic.expected.out @@ -10,5 +10,5 @@ "data": "declaration uses 'sorry'"}], "env": 0} -{"message": ":1:1: unknown tactic"} +{"message": "Lean error:\n:1:1: unknown tactic"}