Pantograph/Frontend/MetaTranslate.lean

@@ -68,8 +68,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
     match e with
     | .fvar fvarId =>
       let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
-      -- Delegating this to `Meta.check` later
+      assert! (← getLCtx).contains fvarId'
-      --assert! (← getLCtx).contains fvarId'
       return .done $ .fvar fvarId'
     | .mvar mvarId => do
       -- Must not be assigned

Pantograph/Library.lean

@@ -207,14 +207,6 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: Stri
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
-@[export pantograph_goal_try_draft_m]
-protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult := do
-  let expr ← match (← parseTermM expr) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  runTermElabM do
-    state.restoreElabM
-    state.tryTacticM goal (Tactic.evalDraft expr)
 @[export pantograph_goal_let_m]
 def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
   runTermElabM <| state.tryLet goal binderName type

Pantograph/Protocol.lean

@@ -255,7 +255,6 @@ structure GoalTactic where
   calc?: Option String := .none
   -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
   conv?: Option Bool := .none
-  draft?: Option String := .none
 
   -- In case of the `have` tactic, the new free variable name is provided here
   binderName?: Option String := .none

Pantograph/Serial.lean

@@ -59,12 +59,6 @@ and then add the new constants.
 def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit :=
   Pantograph.pickle path (env.header.imports, env.constants.map₂)
 
-def resurrectEnvironment
-  (imports : Array Import)
-  (map₂ : PHashMap Name ConstantInfo)
-  : IO Environment := do
-  let env ← importModules imports {} 0
-  env.replay (Std.HashMap.ofList map₂.toList)
 /--
 Unpickle an `Environment` from disk.
 
@@ -74,7 +68,8 @@ and then replace the new constants.
 @[export pantograph_env_unpickle_m]
 def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
   let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
-  return (← resurrectEnvironment imports map₂, region)
+  let env ← importModules imports {} 0
+  return (← env.replay (Std.HashMap.ofList map₂.toList), region)
 
 
 open Lean.Core in
@@ -93,9 +88,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
     savedState := {
       term := {
         meta := {
-          core := {
+          core,
-            env, nextMacroScope, ngen, ..
-          },
           meta,
         }
         «elab»,
@@ -107,10 +100,9 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
     convMVar?,
     calcPrevRhs?,
   } := goalState
+  --let env := core.env
   Pantograph.pickle path (
-    env.constants.map₂,
+    ({ core with } : CompactCoreState),
-
-    ({ nextMacroScope, ngen } : CompactCoreState),
     meta,
     «elab»,
     tactic,
@@ -125,8 +117,6 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
 def goalStateUnpickle (path : System.FilePath) (env : Environment)
     : IO (GoalState × CompactedRegion) := unsafe do
   let ((
-    map₂,
-
     compactCore,
     meta,
     «elab»,
@@ -137,8 +127,6 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
     convMVar?,
     calcPrevRhs?,
   ), region) ← Pantograph.unpickle (
-    PHashMap Name ConstantInfo ×
-
     CompactCoreState ×
     Meta.State ×
     Elab.Term.State ×
@@ -149,7 +137,6 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
     Option (MVarId × MVarId × List MVarId) ×
     Option (MVarId × Expr)
   ) path
-  let env ← env.replay (Std.HashMap.ofList map₂.toList)
   let goalState := {
     savedState := {
       term := {

Repl.lean

@@ -152,27 +152,24 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let .some goal := goalState.goals.get? args.goalId |
       return .error $ errorIndex s!"Invalid goal index {args.goalId}"
     let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
-      -- NOTE: Should probably use a macro to handle this...
+      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?  with
-      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?, args.draft?  with
+      | .some tactic, .none, .none, .none, .none, .none => do
-      | .some tactic, .none, .none, .none, .none, .none, .none => do
         pure <| Except.ok <| ← goalState.tryTactic goal tactic
-      | .none, .some expr, .none, .none, .none, .none, .none => do
+      | .none, .some expr, .none, .none, .none, .none => do
         pure <| Except.ok <| ← goalState.tryAssign goal expr
-      | .none, .none, .some type, .none, .none, .none, .none => do
+      | .none, .none, .some type, .none, .none, .none => do
         let binderName := args.binderName?.getD ""
         pure <| Except.ok <| ← goalState.tryHave goal binderName type
-      | .none, .none, .none, .some type, .none, .none, .none => do
+      | .none, .none, .none, .some type, .none, .none => do
         let binderName := args.binderName?.getD ""
         pure <| Except.ok <| ← goalState.tryLet goal binderName type
-      | .none, .none, .none, .none, .some pred, .none, .none => do
+      | .none, .none, .none, .none, .some pred, .none => do
         pure <| Except.ok <| ← goalState.tryCalc goal pred
-      | .none, .none, .none, .none, .none, .some true, .none => do
+      | .none, .none, .none, .none, .none, .some true => do
         pure <| Except.ok <| ← goalState.conv goal
-      | .none, .none, .none, .none, .none, .some false, .none => do
+      | .none, .none, .none, .none, .none, .some false => do
         pure <| Except.ok <| ← goalState.convExit
-      | .none, .none, .none, .none, .none, .none, .some draft => do
+      | _, _, _, _, _, _ =>
-        pure <| Except.ok <| ← goalState.tryDraft goal draft
-      | _, _, _, _, _, _, _ =>
         let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
         pure $ Except.error $ error
     match nextGoalState? with

doc/repl.md

@@ -33,7 +33,6 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
     to the previous `rhs`.
   - `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
     exit, the goal id is ignored.
-  - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
   Execute continuation/resumption
   - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.
@@ -45,12 +44,11 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   state. The user is responsible to ensure the sender/receiver instances share
   the same environment.
 * `frontend.process { ["fileName": <fileName>,] ["file": <str>], invocations:
-  <bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
+  <bool>, sorrys: <bool>, newConstants: <bool> }`: Executes the Lean frontend on
-  Executes the Lean frontend on a file, collecting the tactic invocations
+  a file, collecting the tactic invocations (`"invocations": true`), the
-  (`"invocations": true`), the sorrys and type errors into goal states
+  sorrys and type errors into goal states (`"sorrys": true`), and new constants
-  (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
+  (`"newConstants": true`). In the case of `sorrys`, this command additionally
-  `sorrys`, this command additionally outputs the position of each captured
+  outputs the position of each captured `sorry`.
-  `sorry`.
 
 ## Errors