From 1fcc24283be328140a72791209b713e96e90dffd Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 10 Jul 2025 13:18:35 -0700 Subject: [PATCH 1/3] refactor: Use consistent error handling --- Pantograph/Goal.lean | 38 ++++++++++++++++---------------------- Test/Proofs.lean | 4 ++-- 2 files changed, 18 insertions(+), 24 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 0642ac9..93c3c3c 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -6,7 +6,6 @@ All the functions starting with `try` resume their inner monadic state. import Pantograph.Tactic import Lean - namespace Pantograph open Lean @@ -141,8 +140,8 @@ protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit := let { nextMacroScope, ngen, .. } := state - modifyGetThe Core.State (fun st => ((), - { st with nextMacroScope, ngen })) + modifyGetThe Core.State fun st => ((), + { st with nextMacroScope, ngen }) -- Restore the name generator and macro scopes of the core state protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := restoreCoreMExtra state.coreState @@ -469,7 +468,7 @@ protected def GoalState.step (state : GoalState) (site : Site) (tacticM : Elab.T : Elab.TermElabM GoalState := Prod.snd <$> GoalState.step' state site tacticM guardMVarErrors -/-- Response for executing a tactic -/ +/-- Result for executing a tactic, capturing errors in the process -/ inductive TacticResult where -- Goes to next state | success (state : GoalState) (messages : Array Message) @@ -480,40 +479,35 @@ inductive TacticResult where -- The given action cannot be executed in the state | invalidAction (message : String) -private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (Bool × List Message) := do +private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (List Message) := do let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength - let hasErrors := newMessages.any (·.severity == .error) Core.resetMessageLog - return (hasErrors, newMessages) + return newMessages /-- Execute a `TermElabM` producing a goal state, capturing the error and turn it into a `TacticResult` -/ def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM TacticResult := do let messageLog ← Core.getMessageLog unless messageLog.toList.isEmpty do IO.eprintln s!"{← messageLog.toList.mapM (·.toString)}" - assert! messageLog.toList.isEmpty + throwError "Message log must be empty at the beginning." try let state ← elabM -- Check if error messages have been generated in the core. - let (hasError, newMessages) ← dumpMessageLog - if hasError then + let newMessages ← dumpMessageLog + let hasErrors := newMessages.any (·.severity == .error) + if hasErrors then return .failure newMessages.toArray else return .success state newMessages.toArray catch exception => - match exception with - | .internal _ => - let (_, messages) ← dumpMessageLog - return .failure messages.toArray - | _ => - let (_, messages) ← dumpMessageLog - let message := { - fileName := ← getFileName, - pos := ← getRefPosition, - data := exception.toMessageData, - } - return .failure (message :: messages).toArray + let messages ← dumpMessageLog + let message := { + fileName := ← getFileName, + pos := ← getRefPosition, + data := exception.toMessageData, + } + return .failure (message :: messages).toArray /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/ protected def GoalState.tryTacticM diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 2df2594..2442243 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -352,8 +352,8 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do -- buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r" --] - let .failure #[message] ← state1.tacticOn 0 tactic - | addTest $ assertUnreachable s!"{tactic} should fail" + let .failure #[_head, message] ← state1.tacticOn 0 tactic + | addTest $ assertUnreachable s!"{tactic} should fail with 2 messages" checkEq s!"{tactic} fails" (← message.toString) s!"{← getFileName}:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n" -- 2.44.1 From bd7dde8235500a968f0dd2bca63f30db9b84a4c7 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 10 Jul 2025 14:43:58 -0700 Subject: [PATCH 2/3] chore: Code cleanup --- Pantograph/Goal.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 93c3c3c..0f552e2 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -140,8 +140,7 @@ protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit := let { nextMacroScope, ngen, .. } := state - modifyGetThe Core.State fun st => ((), - { st with nextMacroScope, ngen }) + modifyThe Core.State ({ · with nextMacroScope, ngen }) -- Restore the name generator and macro scopes of the core state protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := restoreCoreMExtra state.coreState @@ -151,9 +150,6 @@ protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := do protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := do state.restoreCoreMExtra state.savedState.term.restore -private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do - state.restoreElabM - Elab.Tactic.setGoals [goal] /-- Brings into scope a list of goals. User must ensure `goals` are distinct. -- 2.44.1 From 9fdaefe5391535d6436886051cc620986d10a081 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 10 Jul 2025 15:30:46 -0700 Subject: [PATCH 3/3] doc: Cleanup tactic documentation --- Pantograph/Protocol.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 086fe92..a003e8d 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -257,13 +257,16 @@ structure GoalTactic where autoResume?: Option Bool := .none -- One of the fields here must be filled tactic?: Option String := .none - mode?: Option String := .none -- Changes the current category to {"tactic", "calc", "conv"} + -- Changes the current category to {"tactic", "calc", "conv"} + mode?: Option String := .none + -- Assigns an expression to the current goal expr?: Option String := .none have?: Option String := .none let?: Option String := .none draft?: Option String := .none - -- In case of the `have` tactic, the new free variable name is provided here + -- In case of the `have` and `let` tactics, the new free variable name is + -- provided here binderName?: Option String := .none deriving Lean.FromJson -- 2.44.1