Pantograph/Protocol.lean

@@ -312,8 +312,6 @@ structure FrontendProcess where
   invocations: Bool := false
   -- If set to true, collect `sorry`s
   sorrys: Bool := false
-  -- If set to true, extract new constants
-  newConstants: Bool := false
   deriving Lean.FromJson
 structure InvokedTactic where
   goalBefore: String
@@ -327,16 +325,13 @@ 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?: Option (Array Goal) := .none
+  goals: Array Goal := #[]
   -- Code segments which generated the goals
-  goalSrcBoundaries?: Option (Array (Nat × Nat)) := .none
-
-  -- New constants defined in compilation unit
-  newConstants?: Option (Array String) := .none
+  goalSrcBoundaries: Array (Nat × Nat) := #[]
+  messages: Array String := #[]
   deriving Lean.ToJson
 structure FrontendProcessResult where
   units: List CompilationUnit

Repl.lean

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

Test/Integration.lean

@@ -174,7 +174,6 @@ def test_frontend_process : Test :=
         ("file", .str file),
         ("invocations", .bool true),
         ("sorrys", .bool false),
-        ("newConstants", .bool false),
       ]
      ({
        units := [{
@@ -215,7 +214,6 @@ def test_frontend_process_sorry : Test :=
         ("file", .str file),
         ("invocations", .bool false),
         ("sorrys", .bool true),
-        ("newConstants", .bool false),
       ]
      ({
        units := [{
@@ -223,8 +221,8 @@ def test_frontend_process_sorry : Test :=
        }, {
          boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
          goalStateId? := .some 0,
-         goals? := .some #[goal1],
-         goalSrcBoundaries? := .some #[(57, 62)],
+         goals := #[goal1],
+         goalSrcBoundaries := #[(57, 62)],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
     }: Protocol.FrontendProcessResult),