Pantograph/Protocol.lean

@@ -327,14 +327,16 @@ structure InvokedTactic where
 structure CompilationUnit where
   -- String boundaries of compilation units
   boundary: (Nat × Nat)
+  messages: Array String := #[]
   -- Tactic invocations
   invocations?: Option (List InvokedTactic) := .none
   goalStateId?: Option Nat := .none
-  goals: Array Goal := #[]
+  goals?: Option (Array Goal) := .none
   -- Code segments which generated the goals
-  goalSrcBoundaries: Array (Nat × Nat) := #[]
+  goalSrcBoundaries?: Option (Array (Nat × Nat)) := .none
-  messages: Array String := #[]
+
-  newConstants: Option (Array String) := .none
+  -- New constants defined in compilation unit
+  newConstants?: Option (Array String) := .none
   deriving Lean.ToJson
 structure FrontendProcessResult where
   units: List CompilationUnit

Repl.lean

@@ -269,25 +269,26 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         return (step.before, boundary, invocations?, sorrys, messages, newConstants)
       let li ← frontendM.run context |>.run' state
       let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages, newConstants) => Lean.withEnv env do
-        let newConstants := if args.newConstants then
+        let newConstants? := if args.newConstants then
             .some $ newConstants.toArray.map λ name => name.toString
           else
             .none
-        let (goalStateId?, goals, goalSrcBoundaries) ← if sorrys.isEmpty then do
+        let (goalStateId?, goals?, goalSrcBoundaries?) ← if sorrys.isEmpty then do
-            pure (.none, #[], #[])
+            pure (.none, .none, .none)
           else do
             let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
             let stateId ← newGoalState state
             let goals ← goalSerialize state options
-            pure (.some stateId, goals, srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx)))
+            let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
+            pure (.some stateId, .some goals, .some srcBoundaries)
         return {
           boundary,
+          messages,
           invocations?,
           goalStateId?,
-          goals,
+          goals?,
-          goalSrcBoundaries,
+          goalSrcBoundaries?,
-          messages,
+          newConstants?,
-          newConstants,
         }
       return .ok { units }
     catch e =>

Test/Integration.lean

@@ -223,8 +223,8 @@ def test_frontend_process_sorry : Test :=
        }, {
          boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
          goalStateId? := .some 0,
-         goals := #[goal1],
+         goals? := .some #[goal1],
-         goalSrcBoundaries := #[(57, 62)],
+         goalSrcBoundaries? := .some #[(57, 62)],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
     }: Protocol.FrontendProcessResult),