Merge pull request 'feat: Display `Message` metadata' (#232) from frontend/message into dev

Reviewed-on: #232

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
 
 

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 messages.toArray
-    | _ => return .failure #[← exception.toMessageData.toString]
+    | _ =>
+      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

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

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

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.size} messages)"
-    s!".failure {messages}"
   | .parseError error => s!".parseError {error}"
   | .invalidAction error => s!".invalidAction {error}"
 

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

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"
+  let .failure #[message] ← state1.tacticOn 0 tactic
-  checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"]
+    | 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 .failure #[message] ← state1.tacticOn 0 tactic
-  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"
+    | addTest $ assertUnreachable s!"{tactic} should fail"
-  checkEq s!"{tactic} fails" messages #[message]
+  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")

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

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) :=
   [