2025-07-10 11:45:45 -07:00
9 changed files with 79 additions and 43 deletions
--- 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


--- 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
--- 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
--- 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
--- 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}"

--- 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 := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
+       messages := #[{
+         fileName := "<anonymous>",
+         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 := #["<anonymous>:1:8: warning: declaration uses 'sorry'\n"],
+       messages := #[{
+         fileName := "<anonymous>",
+         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
--- 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!"<Pantograph>: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")
--- 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
--- 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) :=
  [