Pantograph/Frontend/Basic.lean

@@ -42,6 +42,14 @@ structure CompilationStep where
   msgs : List Message
   trees : List Elab.InfoTree
 
+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
+
 
 /--
 Process one command, returning a `CompilationStep` and

Pantograph/Protocol.lean

@@ -298,11 +298,18 @@ structure InvokedTactic where
   goalAfter: String
   tactic: String
   deriving Lean.ToJson
-structure FrontendProcessResult where
+
+structure CompilationUnit where
   -- String boundaries of compilation units
-  units: List (Nat × Nat)
+  boundary: (Nat × Nat)
+  -- Tactic invocations
   invocations?: Option (List InvokedTactic) := .none
-  goalStates?: Option (List (Nat × Array Goal)) := .none
+  goalStateId?: Option Nat := .none
+  goals: Array Goal := #[]
+  messages: Array String := #[]
+  deriving Lean.ToJson
+structure FrontendProcessResult where
+  units: List CompilationUnit
   deriving Lean.ToJson
 
 abbrev CR α := Except InteractionError α

Repl.lean

@@ -216,35 +216,36 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           let env ← Lean.MonadEnv.getEnv
           pure <| .some env
       let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
-      let m := Frontend.mapCompilationSteps λ step => do
+      let frontendM := Frontend.mapCompilationSteps λ step => do
-        let unitBoundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
+        let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
-        let tacticInvocations ← if args.invocations then
+        let invocations?: Option (List Protocol.InvokedTactic) ← if args.invocations then
-            Frontend.collectTacticsFromCompilationStep step
+            let invocations ← Frontend.collectTacticsFromCompilationStep step
+            pure $ .some invocations
           else
-            pure []
+            pure .none
         let sorrys := if args.sorrys then
             Frontend.collectSorrys step
           else
             []
-        return (unitBoundary, tacticInvocations, sorrys)
+        let messages ← step.messageStrings
-      let li ← m.run context |>.run' state
+        return (boundary, invocations?, sorrys, messages)
-      let units := li.map λ (unit, _, _) => unit
+      let li ← frontendM.run context |>.run' state
-      let invocations? := if args.invocations then
+      let units ← li.mapM λ (boundary, invocations?, sorrys, messages) => do
-          .some $ li.bind λ (_, invocations, _) => invocations
+        let (goalStateId?, goals) ← if sorrys.isEmpty then do
-        else
+            pure (.none, #[])
-          .none
+          else do
-      let goalStates? ← if args.sorrys then do
-          let stateIds ← li.filterMapM λ (_, _, sorrys) => do
-            if sorrys.isEmpty then
-              return .none
             let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
             let stateId ← newGoalState goalState
             let goals ← goalSerialize goalState options
-            return .some (stateId, goals)
+            pure (.some stateId, goals)
-          pure $ .some stateIds
+        return {
-        else
+          boundary,
-          pure .none
+          invocations?,
-      return .ok { units, invocations?, goalStates? }
+          goalStateId?,
+          goals,
+          messages,
+        }
+      return .ok { units }
     catch e =>
       return .error $ errorI "frontend" (← e.toMessageData.toString)
 

Test/Integration.lean

@@ -176,19 +176,21 @@ def test_frontend_process : Test :=
         ("sorrys", .bool false),
       ]
      ({
-       units := [(0, file.utf8ByteSize)],
+       units := [{
-       invocations? := .some [
+         boundary := (0, file.utf8ByteSize),
-         {
+         invocations? := .some [
-           goalBefore := "⊢ ∀ (p : Prop), p → p",
+           {
-           goalAfter := goal1,
+             goalBefore := "⊢ ∀ (p : Prop), p → p",
-           tactic := "intro p h",
+             goalAfter := goal1,
-         },
+             tactic := "intro p h",
-         {
+           },
-           goalBefore := goal1 ,
+           {
-           goalAfter := "",
+             goalBefore := goal1 ,
-           tactic := "exact h",
+             goalAfter := "",
-         },
+             tactic := "exact h",
-       ]
+           },
+         ]
+       }],
     }: Protocol.FrontendProcessResult),
   ]
 
@@ -212,13 +214,14 @@ def test_frontend_process_sorry : Test :=
         ("sorrys", .bool true),
       ]
      ({
-       units := [
+       units := [{
-         (0, solved.utf8ByteSize),
+         boundary := (0, solved.utf8ByteSize),
-         (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
+       }, {
-       ],
+         boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
-       goalStates? := [
+         goalStateId? := .some 0,
-         (0, #[goal1]),
+         goals := #[goal1],
-       ]
+         messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
+       }],
     }: Protocol.FrontendProcessResult),
   ]