From ac8dcc4130f0b9d80e56447625da043335b93904 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 10 Jul 2025 11:42:25 -0700 Subject: [PATCH] feat: Display `Message` metadata --- Pantograph/Frontend/Basic.lean | 4 ---- Pantograph/Goal.lean | 24 ++++++++++++------- Pantograph/Protocol.lean | 10 +++----- Repl.lean | 6 +++-- Test/Common.lean | 3 +-- Test/Integration.lean | 43 ++++++++++++++++++++++++++++------ Test/Proofs.lean | 19 +++++++++------ Test/Tactic/Prograde.lean | 9 +++---- Test/Tactic/Special.lean | 4 +++- 9 files changed, 79 insertions(+), 43 deletions(-) diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean index 035c34b..3fbc99d 100644 --- a/Pantograph/Frontend/Basic.lean +++ b/Pantograph/Frontend/Basic.lean @@ -52,10 +52,6 @@ structure CompilationStep where namespace CompilationStep -@[export pantograph_frontend_compilation_step_message_strings_m] -def messageStrings (step: CompilationStep) : IO (Array String) := do - List.toArray <$> step.msgs.mapM (·.toString) - end CompilationStep diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index e646448..0642ac9 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -472,20 +472,19 @@ protected def GoalState.step (state : GoalState) (site : Site) (tacticM : Elab.T /-- Response for executing a tactic -/ inductive TacticResult where -- Goes to next state - | success (state : GoalState) (messages : Array String) + | success (state : GoalState) (messages : Array Message) -- Tactic failed with messages - | failure (messages : Array String) + | failure (messages : Array Message) -- Could not parse tactic | parseError (message : String) -- The given action cannot be executed in the state | invalidAction (message : String) -private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (Bool × Array String) := do +private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (Bool × List Message) := do let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength let hasErrors := newMessages.any (·.severity == .error) - let newMessages ← newMessages.mapM λ m => m.toString Core.resetMessageLog - return (hasErrors, newMessages.toArray) + return (hasErrors, 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 @@ -499,15 +498,22 @@ def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM -- Check if error messages have been generated in the core. let (hasError, newMessages) ← dumpMessageLog if hasError then - return .failure newMessages + return .failure newMessages.toArray else - return .success state newMessages + return .success state newMessages.toArray catch exception => match exception with | .internal _ => let (_, messages) ← dumpMessageLog - return .failure messages - | _ => return .failure #[← exception.toMessageData.toString] + return .failure 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/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index f83d0ed..086fe92 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -6,6 +6,7 @@ its field names to avoid confusion with error messages generated by the REPL. -/ import Lean.Data.Json import Lean.Data.Position +import Lean.Message namespace Pantograph.Protocol @@ -77,8 +78,6 @@ structure Goal where vars : Array Variable := #[] deriving Lean.ToJson - - --- Individual Commands and return types --- structure Command where @@ -96,9 +95,6 @@ def errorOperation (desc: String): InteractionError := { error := "operation", d def errorExpr (desc: String): InteractionError := { error := "expr", desc } ---- Individual command and return types --- - - structure Reset where deriving Lean.FromJson structure Stat where @@ -278,7 +274,7 @@ structure GoalTacticResult where -- is .none, there has been a tactic error. goals?: Option (Array Goal) := .none - messages? : Option (Array String) := .some #[] + messages? : Option (Array Lean.SerialMessage) := .some #[] -- Existence of this field shows the tactic parsing has failed parseError? : Option String := .none @@ -388,7 +384,7 @@ structure InvokedTactic where structure CompilationUnit where -- String boundaries of compilation units boundary: (Nat × Nat) - messages: Array String := #[] + messages: Array Lean.SerialMessage := #[] -- Number of tactic invocations nInvocations?: Option Nat := .none goalStateId?: Option Nat := .none diff --git a/Repl.lean b/Repl.lean index c7a997d..ef91a5e 100644 --- a/Repl.lean +++ b/Repl.lean @@ -157,6 +157,7 @@ def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := | .ok e => env.hasUnsafe e | .error _ => false let goals ← runCoreM $ nextGoalState.serializeGoals (options := state.options) |>.run' + let messages ← messages.mapM (·.serialize) return { nextStateId? := .some nextStateId, goals? := .some goals, @@ -169,6 +170,7 @@ def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := | .ok (.invalidAction message) => Protocol.throw $ errorI "invalid" message | .ok (.failure messages) => + let messages ← messages.mapM (·.serialize) return { messages? := .some messages } end Goal @@ -181,7 +183,7 @@ structure CompilationUnit where boundary : Nat × Nat invocations : List Protocol.InvokedTactic sorrys : List Frontend.InfoWithContext - messages : Array String + messages : Array SerialMessage newConstants : List Name def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do @@ -209,7 +211,7 @@ def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendP Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals }) else pure [] - let messages ← step.messageStrings + let messages ← step.msgs.toArray.mapM (·.serialize) let newConstants ← if args.newConstants then Frontend.collectNewDefinedConstants step else diff --git a/Test/Common.lean b/Test/Common.lean index 22926aa..a8ee1d5 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -75,8 +75,7 @@ def GoalState.tacticOn' (state: GoalState) (goalId: Nat) (tactic: TSyntax `tacti def TacticResult.toString : TacticResult → String | .success state _messages => s!".success ({state.goals.length} goals)" | .failure messages => - let messages := "\n".intercalate messages.toList - s!".failure {messages}" + s!".failure ({messages.size} messages)" | .parseError error => s!".parseError {error}" | .invalidAction error => s!".invalidAction {error}" diff --git a/Test/Integration.lean b/Test/Integration.lean index e700ea0..e49d9f0 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -23,6 +23,9 @@ deriving instance Lean.ToJson for Protocol.FrontendData abbrev TestM α := TestT MainM α abbrev Test := TestM Unit +def getFileName : TestM String := do + return (← read).coreContext.fileName + def step { α β } [Lean.ToJson α] [Lean.ToJson β] (cmd: String) (payload: α) (expected: β) (name? : Option String := .none) : TestM Unit := do let payload := Lean.toJson payload @@ -96,8 +99,14 @@ def test_tactic : Test := do step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic) ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult) step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic) - ({ messages? := .some #["tactic 'apply' failed, could not unify the conclusion of `@Nat.le_of_succ_le`\n ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith the goal\n ∀ (q : Prop), x ∨ q → q ∨ x\n\nNote: The full type of `@Nat.le_of_succ_le` is\n ∀ {n m : Nat}, n.succ ≤ m → n ≤ m\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }: - Protocol.GoalTacticResult) + ({ + messages? := .some #[{ + fileName := ← getFileName, + kind := .anonymous, + pos := ⟨0, 0⟩, + data := "tactic 'apply' failed, could not unify the conclusion of `@Nat.le_of_succ_le`\n ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith the goal\n ∀ (q : Prop), x ∨ q → q ∨ x\n\nNote: The full type of `@Nat.le_of_succ_le` is\n ∀ {n m : Nat}, n.succ ≤ m → n ≤ m\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x", + }] + }: Protocol.GoalTacticResult) step "goal.tactic" ({ stateId := 0, tactic? := .some "sorry" }: Protocol.GoalTactic) ({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult) example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by @@ -312,7 +321,14 @@ def test_frontend_process_sorry : Test := do goalStateId? := .some 0, goals? := .some #[goal1], goalSrcBoundaries? := .some #[(57, 62)], - messages := #[":2:0: warning: declaration uses 'sorry'\n"], + messages := #[{ + fileName := "", + kind := `hasSorry, + pos := ⟨2, 0⟩, + endPos := .some ⟨2, 7⟩, + severity := .warning, + data := "declaration uses 'sorry'", + }], }], }: Protocol.FrontendProcessResult) @@ -363,12 +379,25 @@ def test_frontend_process_circular : Test := do goalStateId? := .some 0, goals? := .some #[goal1], goalSrcBoundaries? := .some #[(35, 40)], - messages := #[":1:8: warning: declaration uses 'sorry'\n"], + messages := #[{ + fileName := "", + kind := `hasSorry, + pos := ⟨1, 8⟩, + endPos := .some ⟨1, 15⟩, + severity := .warning, + data := "declaration uses 'sorry'" + }], }], - }: Protocol.FrontendProcessResult) + } : Protocol.FrontendProcessResult) step "goal.tactic" ({ stateId := 0, tactic? := .some "exact?" }: Protocol.GoalTactic) - ({ messages? := .some #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."] } - : Protocol.GoalTacticResult) + ({ + messages? := .some #[{ + fileName := ← getFileName, + kind := .anonymous, + pos := ⟨0, 0⟩, + data := "`exact?` could not close the goal. Try `apply?` to see partial suggestions." + }] + } : Protocol.GoalTacticResult) def runTestSuite (env : Lean.Environment) (steps : Test): IO LSpec.TestSeq := do -- Setup the environment for execution diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 5f1e1b7..2df2594 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -105,9 +105,11 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do match ← state1.tacticOn 0 "assumption" with | .failure #[message] => - addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n") + checkEq "assumption" + (← message.toString) + s!"{← getFileName}:0:0: error: tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n\n" | other => do - addTest $ assertUnreachable $ other.toString + addTest $ assertUnreachable other.toString let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with | .success state _ => pure state @@ -317,8 +319,10 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do return () let tactic := "exact ⟨0, by simp⟩" - let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" - checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"] + let .failure #[message] ← state1.tacticOn 0 tactic + | fail s!"{tactic} should fail with 1 message" + checkEq s!"{tactic} fails" (← message.toString) + s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n" def test_tactic_failure_synthesize_placeholder : TestM Unit := do let state? ← startProof (.expr "∀ (p q r : Prop) (h : p → q), q ∧ r") @@ -348,9 +352,10 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do -- buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r" --] - let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" - let message := s!":0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n" - checkEq s!"{tactic} fails" messages #[message] + let .failure #[message] ← state1.tacticOn 0 tactic + | addTest $ assertUnreachable s!"{tactic} should fail" + 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" def test_deconstruct : TestM Unit := do let state? ← startProof (.expr "∀ (p q : Prop) (h : And p q), And q p") diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index aace238..f854553 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -185,8 +185,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) = - #[]) + checkEq s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize)) #[] let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr" addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p q h y => Or.inl y") @@ -264,9 +263,11 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do let tactic := "exact h" match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with | .failure #[message] => - addTest $ LSpec.check tactic (message = s!"type mismatch\n h\nhas type\n a : Prop\nbut is expected to have type\n {mainTarget} : Prop") + checkEq tactic + (← message.toString) + s!"{← getFileName}:0:0: error: type mismatch\n h\nhas type\n a : Prop\nbut is expected to have type\n {mainTarget} : Prop\n" | other => do - addTest $ assertUnreachable $ other.toString + fail s!"Should be a failure: {other.toString}" let tactic := "exact Or.inl (Or.inl h)" let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with diff --git a/Test/Tactic/Special.lean b/Test/Tactic/Special.lean index 2342b3f..d8d4bf4 100644 --- a/Test/Tactic/Special.lean +++ b/Test/Tactic/Special.lean @@ -13,7 +13,9 @@ def test_exact_q : TestT Elab.TermElabM Unit := do let tactic := "exact?" let state1? ← state0.tacticOn (goalId := 0) (tactic := tactic) let .failure messages := state1? | fail "Must fail" - checkEq "messages" messages #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."] + checkEq "messages" + (← messages.mapM (·.toString)) + #[s!"{← getFileName}:0:0: error: `exact?` could not close the goal. Try `apply?` to see partial suggestions.\n"] def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ -- 2.44.1