.gitignore

@@ -1,4 +1,6 @@
 .*
 !.gitignore
-*.[io]lean
-/result
+
+*.olean
+/build
+/lake-packages

Pantograph/Delate.lean

@@ -264,24 +264,25 @@ def serializeName (name: Name) (sanitize: Bool := true): String :=
     if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
 
 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
-partial def serializeSortLevel (level: Level) : String :=
+partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
   let k := level.getOffset
   let u := level.getLevelOffset
   let u_str := match u with
     | .zero => "0"
     | .succ _ => panic! "getLevelOffset should not return .succ"
     | .max v w =>
-      let v := serializeSortLevel v
-      let w := serializeSortLevel w
+      let v := serializeSortLevel v sanitize
+      let w := serializeSortLevel w sanitize
       s!"(:max {v} {w})"
     | .imax v w =>
-      let v := serializeSortLevel v
-      let w := serializeSortLevel w
+      let v := serializeSortLevel v sanitize
+      let w := serializeSortLevel w sanitize
       s!"(:imax {v} {w})"
     | .param name =>
+      let name := serializeName name sanitize
       s!"{name}"
     | .mvar id =>
-      let name := id.name
+      let name := serializeName id.name sanitize
       s!"(:mv {name})"
   match k, u with
   | 0, _ => u_str
@@ -294,7 +295,7 @@ partial def serializeSortLevel (level: Level) : String :=
 
 A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 -/
-partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
+partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
   self expr
   where
   delayedMVarToSexp (e: Expr): MetaM (Option String) := do
@@ -326,17 +327,16 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
       -- Lean these are handled using a `#` prefix.
       pure s!"{deBruijnIndex}"
     | .fvar fvarId =>
-      let name := fvarId.name
+      let name := ofName fvarId.name
       pure s!"(:fv {name})"
     | .mvar mvarId => do
         let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
-        let name := mvarId.name
+        let name := ofName mvarId.name
         pure s!"(:{pref} {name})"
     | .sort level =>
-      let level := serializeSortLevel level
+      let level := serializeSortLevel level sanitize
       pure s!"(:sort {level})"
     | .const declName _ =>
-      let declName := serializeName declName (sanitize := false)
       -- The universe level of the const expression is elided since it should be
       -- inferrable from surrounding expression
       pure s!"(:c {declName})"
@@ -346,20 +346,20 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
       let args := " ".intercalate args
       pure s!"({fn'} {args})"
     | .lam binderName binderType body binderInfo => do
-      let binderName' := binderName.eraseMacroScopes
+      let binderName' := ofName binderName
       let binderType' ← self binderType
       let body' ← self body
       let binderInfo' := binderInfoSexp binderInfo
       pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
     | .forallE binderName binderType body binderInfo => do
-      let binderName' := binderName.eraseMacroScopes
+      let binderName' := ofName binderName
       let binderType' ← self binderType
       let body' ← self body
       let binderInfo' := binderInfoSexp binderInfo
       pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
     | .letE name type value body _ => do
       -- Dependent boolean flag diacarded
-      let name' := name.eraseMacroScopes
+      let name' := serializeName name
       let type' ← self type
       let value' ← self value
       let body' ← self body
@@ -369,7 +369,7 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
       -- is wrapped in a :lit sexp.
       let v' := match v with
         | .natVal val => toString val
-        | .strVal val => IR.EmitC.quoteString val
+        | .strVal val => s!"\"{val}\""
       pure s!"(:lit {v'})"
     | .mdata _ inner =>
       -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
@@ -384,9 +384,10 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
   -- Elides all unhygenic names
   binderInfoSexp : Lean.BinderInfo → String
     | .default => ""
-    | .implicit => " :i"
-    | .strictImplicit => " :si"
-    | .instImplicit => " :ii"
+    | .implicit => " :implicit"
+    | .strictImplicit => " :strictImplicit"
+    | .instImplicit => " :instImplicit"
+  ofName (name: Name) := serializeName name sanitize
 
 def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
   let pp?: Option String ← match options.printExprPretty with
@@ -419,13 +420,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
       match localDecl with
       | .cdecl _ fvarId userName _ _ _ =>
         return {
-          name := fvarId.name.toString,
+          name := ofName fvarId.name,
           userName:= ofName userName.simpMacroScopes,
           isInaccessible := userName.isInaccessibleUserName
         }
       | .ldecl _ fvarId userName _ _ _ _ => do
         return {
-          name := fvarId.name.toString,
+          name := ofName fvarId.name,
           userName := toString userName.simpMacroScopes,
           isInaccessible := userName.isInaccessibleUserName
         }
@@ -435,7 +436,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         let userName := userName.simpMacroScopes
         let type ← instantiate type
         return {
-          name := fvarId.name.toString,
+          name := ofName fvarId.name,
           userName:= ofName userName,
           isInaccessible := userName.isInaccessibleUserName
           type? := .some (← serializeExpression options type)
@@ -449,7 +450,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         else
           pure $ .none
         return {
-          name := fvarId.name.toString,
+          name := ofName fvarId.name,
           userName:= ofName userName,
           isInaccessible := userName.isInaccessibleUserName
           type? := .some (← serializeExpression options type)
@@ -468,7 +469,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
           | false => ppVar localDecl
         return var::acc
     return {
-      name := goal.name.toString,
+      name := ofName goal.name,
       userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
       isConversion := isLHSGoal? mvarDecl.type |>.isSome,
       target := (← serializeExpression options (← instantiate mvarDecl.type)),
@@ -532,7 +533,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
         then instantiateAll decl.type
         else pure $ decl.type
       let type_sexp ← if options.printSexp then
-          let sexp ← serializeExpressionSexp type
+          let sexp ← serializeExpressionSexp type (sanitize := false)
           pure <| " " ++ sexp
         else
           pure ""

Pantograph/Environment.lean

@@ -58,7 +58,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
     | some info => pure info
   let module? := env.getModuleIdxFor? name >>=
-    (λ idx => env.allImportedModuleNames.get? idx.toNat)
+    (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
   let value? := match args.value?, info with
     | .some true, _ => info.value?
     | .some false, _ => .none
@@ -80,7 +80,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
       then value?.map (λ e =>
         e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
       else .none,
-    module? := module?.map (·.toString)
+    module? := module?
   }
   let result ← match info with
     | .inductInfo induct => pure { core with inductInfo? := .some {
@@ -113,20 +113,6 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           k := r.k,
       } }
     | _ => pure core
-  let result ← if args.source?.getD false then
-      let srcSearchPath ← initSrcSearchPath
-      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
-      let declRange? ← findDeclarationRanges? name
-      let sourceStart? := declRange?.map (·.range.pos)
-      let sourceEnd? := declRange?.map (·.range.endPos)
-      .pure {
-        result with
-        sourceUri?,
-        sourceStart?,
-        sourceEnd?,
-      }
-    else
-      .pure result
   return .ok result
 def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
   let env ← Lean.MonadEnv.getEnv

Pantograph/Frontend.lean

@@ -1,4 +1,4 @@
+/- Adapted from lean-training-data by semorrison -/
 import Pantograph.Frontend.Basic
 import Pantograph.Frontend.Elab
-import Pantograph.Frontend.InfoTree
 import Pantograph.Frontend.MetaTranslate

Pantograph/Frontend/Basic.lean

@@ -30,13 +30,6 @@ end Lean.PersistentArray
 
 namespace Pantograph.Frontend
 
-@[export pantograph_frontend_stx_byte_range]
-def stxByteRange (stx : Syntax) : String.Pos × String.Pos :=
-  let pos := stx.getPos?.getD 0
-  let endPos := stx.getTailPos?.getD 0
-  (pos, endPos)
-
-
 abbrev FrontendM := Elab.Frontend.FrontendM
 
 structure CompilationStep where
@@ -67,7 +60,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let s := (← get).commandState
   let before := s.env
   let done ← Elab.Frontend.processCommand
-  let stx := (← get).commands.back!
+  let stx := (← get).commands.back
   let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
   let s' := (← get).commandState
   let after := s'.env

Pantograph/Frontend/Elab.lean

@@ -1,21 +1,87 @@
+/- Adapted from https://github.com/semorrison/lean-training-data -/
 import Lean.Elab.Import
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
-import Lean.DeclarationRange
 
 import Pantograph.Frontend.Basic
 import Pantograph.Frontend.MetaTranslate
 import Pantograph.Goal
 import Pantograph.Protocol
-import Pantograph.Frontend.InfoTree
 
 open Lean
 
+namespace Lean.Elab.Info
+/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
+protected def stx? : Info → Option Syntax
+  | .ofTacticInfo         info => info.stx
+  | .ofTermInfo           info => info.stx
+  | .ofCommandInfo        info => info.stx
+  | .ofMacroExpansionInfo info => info.stx
+  | .ofOptionInfo         info => info.stx
+  | .ofFieldInfo          info => info.stx
+  | .ofCompletionInfo     info => info.stx
+  | .ofUserWidgetInfo     info => info.stx
+  | .ofCustomInfo         info => info.stx
+  | .ofFVarAliasInfo      _    => none
+  | .ofFieldRedeclInfo    info => info.stx
+  | .ofOmissionInfo       info => info.stx
+/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
+protected def isOriginal (i : Info) : Bool :=
+  match i.stx? with
+  | none => true   -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
+  | some stx => match stx.getHeadInfo with
+    | .original .. => true
+    | _ => false
+end Lean.Elab.Info
+
+namespace Lean.Elab.TacticInfo
+
+/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
+def name? (t : TacticInfo) : Option Name :=
+  match t.stx with
+  | Syntax.node _ n _ => some n
+  | _ => none
+/-- Decide whether a tactic is "substantive",
+or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
+def isSubstantive (t : TacticInfo) : Bool :=
+  match t.name? with
+  | none => false
+  | some `null => false
+  | some ``cdot => false
+  | some ``cdotTk => false
+  | some ``Lean.Parser.Term.byTactic => false
+  | some ``Lean.Parser.Tactic.tacticSeq => false
+  | some ``Lean.Parser.Tactic.tacticSeq1Indented => false
+  | some ``Lean.Parser.Tactic.«tactic_<;>_» => false
+  | some ``Lean.Parser.Tactic.paren => false
+  | _ => true
+
+end Lean.Elab.TacticInfo
+
+namespace Lean.Elab.InfoTree
+
+/--
+Keep `.node` nodes and `.hole` nodes satisfying predicates.
+
+Returns a `List InfoTree`, although in most situations this will be a singleton.
+-/
+partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
+    InfoTree → List InfoTree
+  | .context ctx tree => tree.filter p m |>.map (.context ctx)
+  | .node info children =>
+    if p info then
+      [.node info (children.toList.map (filter p m)).join.toPArray']
+    else
+      (children.toList.map (filter p m)).join
+  | .hole mvar => if m mvar then [.hole mvar] else []
+
+end Lean.Elab.InfoTree
+
+
 namespace Pantograph.Frontend
 
 -- Info tree filtering functions
 
-/- Adapted from lean-training-data -/
 structure TacticInvocation where
   info : Elab.TacticInfo
   ctx : Elab.ContextInfo
@@ -65,10 +131,19 @@ protected def usedConstants (t: TacticInvocation) : NameSet :=
 
 end TacticInvocation
 
+/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
+partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
+    List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
+  match t with
+  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
+  | .node i children  =>
+      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
+  | _ => []
+
 /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
 each equipped with its relevant `ContextInfo`, and any children info trees. -/
 private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
-  let infos := t.findAllInfo none false fun i => match i with
+  let infos := findAllInfo t none fun i => match i with
     | .ofTacticInfo _ => true
     | _ => false
   infos.filterMap fun p => match p with
@@ -80,18 +155,16 @@ def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
 
 @[export pantograph_frontend_collect_tactics_from_compilation_step_m]
 def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
-  let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ
+  let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
     | info@(.ofTacticInfo _) => info.isOriginal
     | _ => false
-  let tactics := tacticInfoTrees.flatMap collectTactics
+  let tactics := tacticInfoTrees.bind collectTactics
   tactics.mapM λ invocation => do
     let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
     let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
-    let tactic ← invocation.ctx.runMetaM {} <| Meta.withMCtx invocation.info.mctxBefore do
-      return (← invocation.ctx.ppSyntax {} invocation.info.stx).pretty
-      -- FIXME: Why does this not work? There are problems with `term.pseudo.antiquot`
-      --PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
-      --return t.pretty
+    let tactic ← invocation.ctx.runMetaM {} do
+      let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
+      return t.pretty
     let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
     return {
       goalBefore,
@@ -104,91 +177,47 @@ structure InfoWithContext where
   info: Elab.Info
   context?: Option Elab.ContextInfo := .none
 
-structure GoalCollectionOptions where
-  collectTypeErrors : Bool := false
-
-private def collectSorrysInTree (t : Elab.InfoTree) (options : GoalCollectionOptions := {})
-    : IO (List InfoWithContext) := do
-  let infos ← t.findAllInfoM none fun i ctx? => match i with
-    | .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
-      let .some ctx := ctx? | return (false, true)
-      if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
-        if expectedType?.isNone then
-          throw $ .userError "Sorry of indeterminant type is not allowed"
-        return (true, false)
-      unless options.collectTypeErrors do
-        return (false, true)
-      let .some expectedType := expectedType? | return (false, true)
-      let typeMatch ← ctx.runMetaM lctx do
-        let type ← Meta.inferType expr
-        Meta.isExprDefEqGuarded type expectedType
-      return match typeMatch, expr.hasSorry with
-      | false, true => (true, false) -- Types mismatch but has sorry -> collect, halt
-      | false, false => (true, false) -- Types mistmatch but no sorry -> collect, halt
-      | true, true => (false, true) -- Types match but has sorry -> continue
-      | true, false => (false, false) -- Types match but no sorries -> halt
+private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
+  let infos := findAllInfo t none fun i => match i with
+    | .ofTermInfo { expectedType?, expr, stx, .. } =>
+      expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
     | .ofTacticInfo { stx, goalsBefore, .. } =>
       -- The `sorry` term is distinct from the `sorry` tactic
       let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry
-      return (isSorry ∧ !goalsBefore.isEmpty, ¬ isSorry)
-    | _ => return (false, true)
-  return infos.map fun (info, context?, _) => { info, context? }
+      isSorry ∧ !goalsBefore.isEmpty
+    | _ => false
+  infos.map fun (info, context?, _) => { info, context? }
 
 -- NOTE: Plural deliberately not spelled "sorries"
 @[export pantograph_frontend_collect_sorrys_m]
-def collectSorrys (step: CompilationStep) (options : GoalCollectionOptions := {})
-    : IO (List InfoWithContext) := do
-  return (← step.trees.mapM $ λ tree => collectSorrysInTree tree options).flatten
+def collectSorrys (step: CompilationStep) : List InfoWithContext :=
+  step.trees.bind collectSorrysInTree
+
 
-structure AnnotatedGoalState where
-  state : GoalState
-  srcBoundaries : List (String.Pos × String.Pos)
 
 /--
 Since we cannot directly merge `MetavarContext`s, we have to get creative. This
 function duplicates frozen mvars in term and tactic info nodes, and add them to
 the current `MetavarContext`.
 -/
-@[export pantograph_frontend_sorrys_to_goal_state_m]
-def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
+@[export pantograph_frontend_sorrys_to_goal_state]
+def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
   assert! !sorrys.isEmpty
   let goalsM := sorrys.mapM λ i => do
     match i.info with
     | .ofTermInfo termInfo  => do
       let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
-      if (← mvarId.getType).hasSorry then
-        throwError s!"Coupling is not allowed in drafting"
-      return [(mvarId, stxByteRange termInfo.stx)]
+      return [mvarId]
     | .ofTacticInfo tacticInfo => do
-      let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
-      for mvarId in mvarIds do
-        if (← mvarId.getType).hasSorry then
-          throwError s!"Coupling is not allowed in drafting"
-      let range := stxByteRange tacticInfo.stx
-      return mvarIds.map (·, range)
+      MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
     | _ => panic! "Invalid info"
-  let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
-  let goals := annotatedGoals.map Prod.fst
-  let srcBoundaries := annotatedGoals.map Prod.snd
+  let goals := List.join (← goalsM.run {} |>.run' {})
   let root := match goals with
     | [] => panic! "No MVars generated"
     | [g] => g
     | _ => { name := .anonymous }
-  let state ← GoalState.createFromMVars goals root
-  return { state, srcBoundaries }
+  GoalState.createFromMVars goals root
 
 
-@[export pantograph_frontend_collect_new_defined_constants_m]
-def collectNewDefinedConstants (step : CompilationStep) : IO (List Name) := do
-  step.after.constants.map₂.foldlM (λ acc name _ => do
-    if step.before.contains name then
-      return acc
-    let coreM : CoreM Bool := Option.isSome <$> findDeclarationRanges? name
-    let hasRange ← coreM.run' { fileName := step.fileName, fileMap := step.fileMap } { env := step.after } |>.toBaseIO
-    match hasRange with
-    | .ok true => return name :: acc
-    | .ok false => return acc
-    | .error e => throw $ IO.userError (← e.toMessageData.toString)
-    ) []
 
 end Pantograph.Frontend

Pantograph/Frontend/InfoTree.lean

@@ -1,157 +0,0 @@
-/- Adapted from lean-training-data -/
-import Lean.Elab.InfoTree
-import Lean.Parser.Term
-import Lean.PrettyPrinter
-
-open Lean
-
-namespace Lean.Elab
-
-private def elaboratorToString : Name → String
-  | .anonymous => ""
-  | n => s!"⟨{n}⟩ "
-private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("\t" ++ .)
-
-/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
-protected def Info.stx? : Info → Option Syntax
-  | .ofTacticInfo         info => info.stx
-  | .ofTermInfo           info => info.stx
-  | .ofCommandInfo        info => info.stx
-  | .ofMacroExpansionInfo info => info.stx
-  | .ofOptionInfo         info => info.stx
-  | .ofFieldInfo          info => info.stx
-  | .ofCompletionInfo     info => info.stx
-  | .ofUserWidgetInfo     info => info.stx
-  | .ofCustomInfo         info => info.stx
-  | .ofFVarAliasInfo      _    => none
-  | .ofFieldRedeclInfo    info => info.stx
-  | .ofOmissionInfo       info => info.stx
-  | .ofChoiceInfo         info => info.stx
-  | .ofPartialTermInfo    info => info.stx
-/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
-protected def Info.isOriginal (i : Info) : Bool :=
-  match i.stx? with
-  | none => true   -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
-  | some stx => match stx.getHeadInfo with
-    | .original .. => true
-    | _ => false
-
-def ContextInfo.ppExpr (ctx : ContextInfo) (lctx : LocalContext) (e : Expr) : IO Format :=
-  ctx.runMetaM lctx (do Meta.ppExpr (← instantiateMVars e))
-
-def CommandInfo.toString (info : CommandInfo) (ctx : ContextInfo) : IO String := do
-  let stx := (← ctx.ppSyntax {} info.stx).pretty
-  return s!"{elaboratorToString info.elaborator}\n{stx}"
-
-def TermInfo.toString (info : TermInfo) (ctx : ContextInfo) : IO String := do
-  let stx := (← ctx.ppSyntax info.lctx info.stx).pretty
-  let expectedType := (← info.expectedType?.mapM fun ty => do
-    pure s!": {(← ctx.ppExpr info.lctx ty).pretty}").getD ""
-  let expr := (← ctx.ppExpr info.lctx info.expr).pretty
-  return s!"{elaboratorToString info.elaborator}{expr}{expectedType}\n{stx}"
-
-/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
-def TacticInfo.name? (t : TacticInfo) : Option Name :=
-  match t.stx with
-  | Syntax.node _ n _ => some n
-  | _ => none
-/-- Decide whether a tactic is "substantive",
-or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
-def TacticInfo.isSubstantive (t : TacticInfo) : Bool :=
-  match t.name? with
-  | none => false
-  | some `null => false
-  | some ``cdot => false
-  | some ``cdotTk => false
-  | some ``Lean.Parser.Term.byTactic => false
-  | some ``Lean.Parser.Tactic.tacticSeq => false
-  | some ``Lean.Parser.Tactic.tacticSeq1Indented => false
-  | some ``Lean.Parser.Tactic.«tactic_<;>_» => false
-  | some ``Lean.Parser.Tactic.paren => false
-  | _ => true
-def TacticInfo.pp (info : TacticInfo) (ctx : ContextInfo) : IO Format :=
-  ctx.runMetaM {} try
-    Lean.PrettyPrinter.ppTactic ⟨info.stx⟩
-  catch _ =>
-    pure "<failed to pretty print>"
-def TacticInfo.toString (i : TacticInfo) (ctx : ContextInfo) : IO String := do
-  let name := i.name?
-  let stx := Format.pretty (← i.pp ctx)
-  return s!"{name}\n{stx}"
-
-/--
-Keep `.node` nodes and `.hole` nodes satisfying predicates.
-
-Returns a `List InfoTree`, although in most situations this will be a singleton.
--/
-partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
-    InfoTree → List InfoTree
-  | .context ctx tree => tree.filter p m |>.map (.context ctx)
-  | .node info children =>
-    if p info then
-      [.node info (children.toList.map (filter p m)).flatten.toPArray']
-    else
-      (children.toList.map (filter p m)).flatten
-  | .hole mvar => if m mvar then [.hole mvar] else []
-
-/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
-partial def InfoTree.findAllInfo
-    (t : InfoTree)
-    (context?: Option Elab.ContextInfo)
-    (haltOnMatch : Bool := false)
-    (pred : Elab.Info → Bool)
-    : List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
-  match t with
-  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
-  | .node i children  =>
-    let head := if pred i then [(i, context?, children)] else []
-    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.flatMap (fun t => findAllInfo t context? haltOnMatch pred)
-    head ++ tail
-  | _ => []
-
-/-- Monadic analogue of `findAllInfo`, but predicate controls whether to recurse. -/
-partial def InfoTree.findAllInfoM [Monad m]
-    (t : InfoTree)
-    (context?: Option Elab.ContextInfo)
-    (pred : Elab.Info → Option Elab.ContextInfo → m (Bool × Bool))
-    : m (List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree)) := do
-  match t with
-  | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) pred
-  | .node i children  =>
-    let (flagCollect, flagRecurse) ← pred i context?
-    let head := if flagCollect then [(i, context?, children)] else []
-    let tail := if ¬ flagRecurse then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? pred)
-    return head ++ (← tail).flatten
-  | _ => return []
-
-@[export pantograph_infotree_to_string_m]
-partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) : IO String := do
-  match t with
-  | .context ctx t => t.toString (ctx.mergeIntoOuter? ctx?)
-  | .node info children =>
-    if let some ctx := ctx? then
-      let node : String ← match info with
-      | .ofTermInfo    info => pure s!"[term] {(← info.toString ctx)}"
-      | .ofCommandInfo info => pure s!"[command] {(← info.toString ctx)}"
-      | .ofTacticInfo  info => pure s!"[tactic] {(← info.toString ctx)}"
-      | .ofMacroExpansionInfo _ => pure "[macro_exp]"
-      | .ofOptionInfo _ => pure "[option]"
-      | .ofFieldInfo _ => pure "[field]"
-      | .ofCompletionInfo _ => pure "[completion]"
-      | .ofUserWidgetInfo _ => pure "[user_widget]"
-      | .ofCustomInfo _ => pure "[custom]"
-      | .ofFVarAliasInfo _ => pure "[fvar]"
-      | .ofFieldRedeclInfo _ => pure "[field_redecl]"
-      | .ofOmissionInfo _ => pure "[omission]"
-      | .ofChoiceInfo _ => pure "[choice]"
-      | .ofPartialTermInfo  _ => pure "[partial_term]"
-      let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
-      return s!"{node}\n{children}"
-    else throw <| IO.userError "No `ContextInfo` available."
-  | .hole mvarId =>
-    if let some ctx := ctx? then
-      let payload := (← ctx.runMetaM {} (do Meta.ppGoal mvarId)).pretty
-      return s!"[hole] {payload}"
-    else throw <| IO.userError "No `ContextInfo` available."
-
-end Lean.Elab

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/Goal.lean

@@ -10,6 +10,8 @@ import Lean
 namespace Pantograph
 open Lean
 
+def filename: String := "<pantograph>"
+
 /--
 Represents an interconnected set of metavariables, or a state in proof search
  -/
@@ -71,8 +73,6 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O
   return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
 protected def GoalState.metaState (state: GoalState): Meta.State :=
   state.savedState.term.meta.meta
-protected def GoalState.coreState (state: GoalState): Core.SavedState :=
-  state.savedState.term.meta.core
 
 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
   mvarId.withContext m |>.run' (← read) state.metaState
@@ -177,52 +177,16 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI
 
 --- Tactic execution functions ---
 
--- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
-private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
-  -- These descendants serve as "seed" mvars. If a MVarError's mvar is related
-  -- to one of these seed mvars, it means an error has occurred when a tactic
-  -- was executing on `src`. `evalTactic`, will not capture these mvars, so we
-  -- need to manually find them and save them into the goal list.
-
-  let descendants ←  Meta.getMVars (.mvar src)
-  --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
-  let mut alreadyVisited : MVarIdSet := {}
-  let mut result : MVarIdSet := {}
-  for { mvarId, .. } in (← get).mvarErrorInfos do
-    unless alreadyVisited.contains mvarId do
-      alreadyVisited := alreadyVisited.insert mvarId
-      /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
-         delayed assigned to another metavariable that is unassigned. -/
-      let mvarDeps ← Meta.getMVars (.mvar mvarId)
-      if mvarDeps.any descendants.contains then do
-        result := mvarDeps.foldl (·.insert ·) result
-  return result.toList
-
-private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
-  let li2' := li2.filter (¬ li1.contains ·)
-  li1 ++ li2'
-
-/--
-Set `guardMVarErrors` to true to capture mvar errors. Lean will not
-automatically collect mvars from text tactics (vide
-`test_tactic_failure_synthesize_placeholder`)
--/
-protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
+protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
   : Elab.TermElabM GoalState := do
   unless (← getMCtx).decls.contains goal do
     throwError s!"Goal is not in context: {goal.name}"
   goal.checkNotAssigned `GoalState.step
-  let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
+  let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
   let nextElabState ← MonadBacktrack.saveState
-  Elab.Term.synthesizeSyntheticMVarsNoPostponing
-
-  let goals ← if guardMVarErrors then
-      pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
-    else
-      pure goals
   return {
     state with
-    savedState := { term := nextElabState, tactic := { goals }, },
+    savedState := { term := nextElabState, tactic := newGoals },
     parentMVar? := .some goal,
     calcPrevRhs? := .none,
   }
@@ -238,37 +202,16 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message: String)
 
-private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Array String) := do
-  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
-    |>.filterMapM λ m => do
-      if m.severity == .error then
-        return .some $ ← m.toString
-      else
-        return .none
-  Core.resetMessageLog
-  return newMessages.toArray
-
-/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
-protected def GoalState.tryTacticM
-    (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
-    (guardMVarErrors : Bool := false)
-    : Elab.TermElabM TacticResult := do
-  let prevMessageLength := state.coreState.messages.toList.length
+/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
+protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit):
+      Elab.TermElabM TacticResult := do
   try
-    let nextState ← state.step goal tacticM guardMVarErrors
-
-    -- Check if error messages have been generated in the core.
-    let newMessages ← dumpMessageLog prevMessageLength
-    if ¬ newMessages.isEmpty then
-      return .failure newMessages
+    let nextState ← state.step goal tacticM
     return .success nextState
   catch exception =>
-    match exception with
-    | .internal _ => return .failure $ ← dumpMessageLog prevMessageLength
-    | _ => return .failure #[← exception.toMessageData.toString]
+    return .failure #[← exception.toMessageData.toString]
 
 /-- Execute a string tactic on given state. Restores TermElabM -/
-@[export pantograph_goal_state_try_tactic_m]
 protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
     Elab.TermElabM TacticResult := do
   state.restoreElabM
@@ -276,10 +219,10 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
     (env := ← MonadEnv.getEnv)
     (catName := if state.isConv then `conv else `tactic)
     (input := tactic)
-    (fileName := ← getFileName) with
+    (fileName := filename) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true
+  state.tryTacticM goal $ Elab.Tactic.evalTactic tactic
 
 protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
       Elab.TermElabM TacticResult := do
@@ -288,7 +231,7 @@ protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: Strin
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := expr)
-    (fileName := ← getFileName) with
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.tryTacticM goal $ Tactic.evalAssign expr
@@ -302,7 +245,7 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := type)
-    (fileName := ← getFileName) with
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.tryTacticM goal $ Tactic.evalLet binderName.toName type
@@ -389,7 +332,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
     (env := state.env)
     (catName := `term)
     (input := pred)
-    (fileName := ← getFileName) with
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   goal.checkNotAssigned `GoalState.tryCalc
@@ -410,7 +353,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
       throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
     if let some prevRhs := calcPrevRhs? then
       unless ← Meta.isDefEqGuarded lhs prevRhs do
-        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}"
+        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- "
 
     -- Creates a mvar to represent the proof that the calc tactic solves the
     -- current branch

Pantograph/Library.lean

@@ -138,36 +138,17 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array
   runMetaM <| state.serializeGoals (parent := .none) options
 
 @[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
-  : CoreM Protocol.GoalPrintResult := runMetaM do
-  state.restoreMetaM
-
-  let root? ← if rootExpr then
-      state.rootExpr?.mapM λ expr => state.withRootContext do
-        serializeExpression options (← instantiateAll expr)
-    else
-      pure .none
-  let parent? ← if parentExpr then
-      state.parentExpr?.mapM λ expr => state.withParentContext do
-        serializeExpression options (← instantiateAll expr)
-    else
-      pure .none
-  let goals ← if goals then
-      goalSerialize state options
-    else
-      pure #[]
-  let extraMVars ← extraMVars.mapM λ mvarId => do
-    let mvarId: MVarId := { name := mvarId.toName }
-    let .some _ ← mvarId.findDecl? | return {}
-    state.withContext mvarId do
-      let .some expr ← getExprMVarAssignment? mvarId | return {}
-      serializeExpression options (← instantiateAll expr)
-  return {
-    root?,
-    parent?,
-    goals,
-    extraMVars,
-  }
+def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
+  runMetaM do
+    state.restoreMetaM
+    return {
+      root? := ← state.rootExpr?.mapM (λ expr =>
+        state.withRootContext do
+          serializeExpression options (← instantiateAll expr)),
+      parent? := ← state.parentExpr?.mapM (λ expr =>
+        state.withParentContext do
+          serializeExpression options (← instantiateAll expr)),
+    }
 
 @[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goal:  MVarId) (tactic: String): CoreM TacticResult :=
@@ -207,14 +188,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

@@ -5,7 +5,6 @@ Note that no command other than `InteractionError` may have `error` as one of
 its field names to avoid confusion with error messages generated by the REPL.
 -/
 import Lean.Data.Json
-import Lean.Data.Position
 
 namespace Pantograph.Protocol
 
@@ -122,13 +121,11 @@ structure EnvCatalogResult where
 -- Print the type of a symbol
 structure EnvInspect where
   name: String
-  -- Show the value expressions; By default definitions values are shown and
-  -- theorem values are hidden.
+  -- If true/false, show/hide the value expressions; By default definitions
+  -- values are shown and theorem values are hidden.
   value?: Option Bool := .some false
-  -- Show the type and value dependencies
+  -- If true, show the type and value dependencies
   dependency?: Option Bool := .some false
-  -- Show source location
-  source?: Option Bool := .some false
   deriving Lean.FromJson
 -- See `InductiveVal`
 structure InductInfo where
@@ -175,11 +172,6 @@ structure EnvInspectResult where
   inductInfo?:      Option InductInfo      := .none
   constructorInfo?: Option ConstructorInfo := .none
   recursorInfo?:    Option RecursorInfo    := .none
-
-  -- Location in source
-  sourceUri?: Option String := .none
-  sourceStart?: Option Lean.Position := .none
-  sourceEnd?: Option Lean.Position := .none
   deriving Lean.ToJson
 
 structure EnvAdd where
@@ -237,7 +229,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
@@ -280,23 +271,12 @@ structure GoalDeleteResult where
 
 structure GoalPrint where
   stateId: Nat
-
-  -- Print root?
-  rootExpr?: Option Bool := .some False
-  -- Print the parent expr?
-  parentExpr?: Option Bool := .some False
-  -- Print goals?
-  goals?: Option Bool := .some False
-  -- Print values of extra mvars?
-  extraMVars?: Option (Array String) := .none
   deriving Lean.FromJson
 structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
-  parent?: Option Expression := .none
-  goals: Array Goal := #[]
-  extraMVars: Array Expression := #[]
+  parent?: Option Expression
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL
@@ -309,33 +289,16 @@ structure GoalDiag where
   instantiate: Bool := true
   printSexp: Bool := false
 
-structure GoalSave where
-  id: Nat
-  path: System.FilePath
-  deriving Lean.FromJson
-structure GoalSaveResult where
-  deriving Lean.ToJson
-structure GoalLoad where
-  path: System.FilePath
-  deriving Lean.FromJson
-structure GoalLoadResult where
-  id: Nat
-  deriving Lean.ToJson
-
 
 /-- Executes the Lean compiler on a single file -/
 structure FrontendProcess where
   -- One of these two must be supplied: Either supply the file name or the content.
   fileName?: Option String := .none
   file?: Option String := .none
-  -- collect tactic invocations
+  -- If set to true, collect tactic invocations
   invocations: Bool := false
-  -- collect `sorry`s
+  -- If set to true, collect `sorry`s
   sorrys: Bool := false
-  -- collect type errors
-  typeErrorsAsGoals: Bool := false
-  -- list new constants from each compilation step
-  newConstants: Bool := false
   deriving Lean.FromJson
 structure InvokedTactic where
   goalBefore: String
@@ -349,16 +312,11 @@ 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
-  -- Code segments which generated the goals
-  goalSrcBoundaries?: Option (Array (Nat × Nat)) := .none
-
-  -- New constants defined in compilation unit
-  newConstants?: Option (Array String) := .none
+  goals: Array Goal := #[]
+  messages: Array String := #[]
   deriving Lean.ToJson
 structure FrontendProcessResult where
   units: List CompilationUnit

Pantograph/Serial.lean

@@ -2,7 +2,6 @@ import Lean.Environment
 import Lean.Replay
 import Init.System.IOError
 import Std.Data.HashMap
-import Pantograph.Goal
 
 /-!
 Input/Output functions
@@ -56,7 +55,7 @@ and when unpickling, we build a fresh `Environment` from the imports,
 and then add the new constants.
 -/
 @[export pantograph_env_pickle_m]
-def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit :=
+def env_pickle (env : Environment) (path : System.FilePath) : IO Unit :=
   Pantograph.pickle path (env.header.imports, env.constants.map₂)
 
 /--
@@ -66,97 +65,9 @@ We construct a fresh `Environment` with the relevant imports,
 and then replace the new constants.
 -/
 @[export pantograph_env_unpickle_m]
-def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
+def env_unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
   let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
   let env ← importModules imports {} 0
   return (← env.replay (Std.HashMap.ofList map₂.toList), region)
 
-
-open Lean.Core in
-structure CompactCoreState where
-  -- env             : Environment
-  nextMacroScope  : MacroScope     := firstFrontendMacroScope + 1
-  ngen            : NameGenerator  := {}
-  -- traceState      : TraceState     := {}
-  -- cache           : Cache     := {}
-  -- messages        : MessageLog     := {}
-  -- infoState       : Elab.InfoState := {}
-
-@[export pantograph_goal_state_pickle_m]
-def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :=
-  let {
-    savedState := {
-      term := {
-        meta := {
-          core,
-          meta,
-        }
-        «elab»,
-      },
-      tactic
-    }
-    root,
-    parentMVar?,
-    convMVar?,
-    calcPrevRhs?,
-  } := goalState
-  --let env := core.env
-  Pantograph.pickle path (
-    ({ core with } : CompactCoreState),
-    meta,
-    «elab»,
-    tactic,
-
-    root,
-    parentMVar?,
-    convMVar?,
-    calcPrevRhs?,
-  )
-
-@[export pantograph_goal_state_unpickle_m]
-def goalStateUnpickle (path : System.FilePath) (env : Environment)
-    : IO (GoalState × CompactedRegion) := unsafe do
-  let ((
-    compactCore,
-    meta,
-    «elab»,
-    tactic,
-
-    root,
-    parentMVar?,
-    convMVar?,
-    calcPrevRhs?,
-  ), region) ← Pantograph.unpickle (
-    CompactCoreState ×
-    Meta.State ×
-    Elab.Term.State ×
-    Elab.Tactic.State ×
-
-    MVarId ×
-    Option MVarId ×
-    Option (MVarId × MVarId × List MVarId) ×
-    Option (MVarId × Expr)
-  ) path
-  let goalState := {
-    savedState := {
-      term := {
-        meta := {
-          core := {
-            compactCore with
-            passedHeartbeats := 0,
-            env,
-          },
-          meta,
-        },
-        «elab»,
-      },
-      tactic,
-    },
-    root,
-    parentMVar?,
-    convMVar?,
-    calcPrevRhs?,
-  }
-  return (goalState, region)
-
 end Pantograph

Pantograph/Tactic/Assign.lean

@@ -27,38 +27,5 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
   goal.assign expr
   Elab.Tactic.replaceMainGoal nextGoals
 
-def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
-  Meta.transform src λ
-    | .app (.app (.const ``sorryAx ..) type) .. => do
-      let type ← instantiateMVars type
-      if type.hasSorry then
-        throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}"
-      let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
-      modify (mvar.mvarId! :: .)
-      pure $ .done mvar
-    | _ => pure .continue
-
--- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals.
-def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do
-  goal.checkNotAssigned `Pantograph.Tactic.draft
-  let exprType ← Meta.inferType expr
-  let goalType ← goal.getType
-  unless ← Meta.isDefEq goalType exprType do
-    throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
-
-  let (expr', holes) ← sorryToHole expr |>.run []
-  goal.assign expr'
-  return holes.reverse
-
-def evalDraft : Elab.Tactic.Tactic := fun stx ↦ Elab.Tactic.withMainContext do
-  let target ← Elab.Tactic.getMainTarget
-  let goal ← Elab.Tactic.getMainGoal
-  let (expr, holeGoals) ← Elab.Tactic.elabTermWithHoles stx
-    (expectedType? := .some target)
-    (tagSuffix := .anonymous)
-    (allowNaturalHoles := true)
-  let draftGoals ← draft goal expr
-  Elab.Tactic.replaceMainGoal $ holeGoals ++ draftGoals
-
 
 end Pantograph.Tactic

Pantograph/Tactic/Prograde.lean

@@ -40,7 +40,7 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
   let fvarId ← mkFreshFVarId
   let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
   let mvarUpstream ←
-    Meta.withLCtx lctxUpstream #[] do
+    withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
       Meta.withNewLocalInstances #[.fvar fvarId] 0 do
         let mvarUpstream ← mkUpstreamMVar mvarId
         --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream

Pantograph/Version.lean

@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.2.25"
+def version := "0.2.19"
 
 end Pantograph

README.md

@@ -7,8 +7,6 @@ A Machine-to-Machine interaction system for Lean 4.
 Pantograph provides interfaces to execute proofs, construct expressions, and
 examine the symbol list of a Lean project for machine learning.
 
-See [documentations](doc/rationale.md) for design rationale and references.
-
 ## Installation
 
 For Nix users, run
@@ -17,9 +15,7 @@ nix build .#{sharedLib,executable}
 ```
 to build either the shared library or executable.
 
-Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and
-run
-
+Install `elan` and `lake`, and run
 ``` sh
 lake build
 ```
@@ -28,12 +24,9 @@ This builds the executable in `.lake/build/bin/pantograph-repl`.
 ## Executable Usage
 
 ``` sh
-pantograph-repl MODULES|LEAN_OPTIONS
+pantograph MODULES|LEAN_OPTIONS
 ```
 
-The `pantograph-repl` executable must be run with a list of modules to import.
-It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
-
 The REPL loop accepts commands as single-line JSON inputs and outputs either an
 `Error:` (indicating malformed command) or a JSON return value indicating the
 result of a command execution.  The command can be passed in one of two formats
@@ -44,6 +37,8 @@ command { ... }
 The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
 empty command aborts the REPL.
 
+The `pantograph` executable must be run with a list of modules to import. It can
+also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
 
 Example: (~5k symbols)
 ```
@@ -69,7 +64,62 @@ stat
 ```
 where the application of `assumption` should lead to a failure.
 
-For a list of commands, see [REPL Documentation](doc/repl.md).
+### Commands
+
+See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
+* `reset`: Delete all cached expressions and proof trees
+* `stat`: Display resource usage
+* `expr.echo {"expr": <expr>, "type": <optional expected type>, ["levels": [<levels>]]}`: Determine the
+  type of an expression and format it.
+* `env.catalog`: Display a list of all safe Lean symbols in the current environment
+* `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
+  given symbol; If value flag is set, the value is printed or hidden. By default
+  only the values of definitions are printed.
+* `options.set { key: value, ... }`: Set one or more options (not Lean options; those
+  have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
+
+  One particular option for interest for machine learning researchers is the
+  automatic mode (flag: `"automaticMode"`).  By default it is turned on, with
+  all goals automatically resuming. This makes Pantograph act like a gym,
+  with no resumption necessary to manage your goals.
+* `options.print`: Display the current set of options
+* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
+  Start a new proof from a given expression or symbol
+* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
+  given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
+  - `{ "tactic": <tactic> }`: Execute an ordinary tactic
+  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
+  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
+  - `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
+    be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
+    to the previous `rhs`.
+  - `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
+    exit, the goal id is ignored.
+* `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
+  Execute continuation/resumption
+  - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.
+  - `{ "goals": <names> }`: Resume the given goals
+* `goal.remove {"stateIds": [<id>]}"`: Drop the goal states specified in the list
+* `goal.print {"stateId": <id>}"`: Print a goal state
+* `frontend.process { ["fileName": <fileName>",] ["file": <str>], invocations:
+  <bool>, sorrys: <bool> }`: Executes the Lean frontend on a file, collecting
+  either the tactic invocations (`"invocations": true`) or the sorrys into goal
+  states (`"sorrys": true`)
+
+### Errors
+
+When an error pertaining to the execution of a command happens, the returning JSON structure is
+
+``` json
+{ "error": "type", "desc": "description" }
+```
+Common error forms:
+* `command`: Indicates malformed command structure which results from either
+  invalid command or a malformed JSON structure that cannot be fed to an
+  individual command.
+* `index`: Indicates an invariant maintained by the output of one command and
+  input of another is broken. For example, attempting to query a symbol not
+  existing in the library or indexing into a non-existent proof state.
 
 ### Project Environment
 
@@ -80,7 +130,7 @@ the environment might be setup like this:
 
 ``` sh
 LIB="../lib"
-LIB_MATHLIB="$LIB/mathlib4/.lake"
+LIB_MATHLIB="$LIB/mathlib4/lake-packages"
 export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
 
 LEAN_PATH=$LEAN_PATH build/bin/pantograph $@

Repl.lean

@@ -15,16 +15,6 @@ structure State where
 /-- Main state monad for executing commands -/
 abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
 
-def newGoalState (goalState: GoalState) : MainM Nat := do
-  let state ← get
-  let stateId := state.nextId
-  set { state with
-    goalStates := state.goalStates.insert stateId goalState,
-    nextId := state.nextId + 1
-  }
-  return stateId
-
-
 -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
 -- certain monadic features in `MainM`
 abbrev CR α := Except Protocol.InteractionError α
@@ -60,8 +50,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     | "goal.continue" => run goal_continue
     | "goal.delete"   => run goal_delete
     | "goal.print"    => run goal_print
-    | "goal.save"     => run goal_save
-    | "goal.load"     => run goal_load
     | "frontend.process"  => run frontend_process
     | cmd =>
       let error: Protocol.InteractionError :=
@@ -74,12 +62,19 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   errorCommand := errorI "command"
   errorIndex := errorI "index"
   errorIO := errorI "io"
+  newGoalState (goalState: GoalState) : MainM Nat := do
+    let state ← get
+    let stateId := state.nextId
+    set { state with
+      goalStates := state.goalStates.insert stateId goalState,
+      nextId := state.nextId + 1
+    }
+    return stateId
   -- Command Functions
   reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
     let state ← get
     let nGoals := state.goalStates.size
     set { state with nextId := 0, goalStates := .empty }
-    Lean.Core.resetMessageLog
     return .ok { nGoals }
   stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
     let state ← get
@@ -95,10 +90,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     Environment.addDecl args
   env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
     let env ← Lean.MonadEnv.getEnv
-    environmentPickle env args.path
+    env_pickle env args.path
     return .ok {}
   env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
-    let (env, _) ← environmentUnpickle args.path
+    let (env, _) ← env_unpickle args.path
     Lean.setEnv env
     return .ok {}
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
@@ -145,27 +140,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?, args.draft?  with
-      | .some tactic, .none, .none, .none, .none, .none, .none => do
+      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?  with
+      | .some tactic, .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
@@ -211,7 +203,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     match nextState? with
     | .error error => return .error <| errorI "structure" error
     | .ok nextGoalState =>
-      let nextStateId ← newGoalState nextGoalState
+      let nextStateId := state.nextId
+      set { state with
+        goalStates := state.goalStates.insert nextStateId nextGoalState,
+        nextId := state.nextId + 1
+      }
       let goals ← goalSerialize nextGoalState (options := state.options)
       return .ok {
         nextStateId,
@@ -226,24 +222,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let .some goalState := state.goalStates[args.stateId]? |
       return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← runMetaInMainM <| goalPrint
-        goalState
-        (rootExpr := args.rootExpr?.getD False)
-        (parentExpr := args.parentExpr?.getD False)
-        (goals := args.goals?.getD False)
-        (extraMVars := args.extraMVars?.getD #[])
-        (options := state.options)
+    let result ← runMetaInMainM <| goalPrint goalState state.options
     return .ok result
-  goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
-    let state ← get
-    let .some goalState := state.goalStates[args.id]? |
-      return .error $ errorIndex s!"Invalid state index {args.id}"
-    goalStatePickle goalState args.path
-    return .ok {}
-  goal_load (args: Protocol.GoalLoad): MainM (CR Protocol.GoalLoadResult) := do
-    let (goalState, _) ← goalStateUnpickle args.path (← Lean.MonadEnv.getEnv)
-    let id ← newGoalState goalState
-    return .ok { id }
   frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
     let options := (← get).options
     try
@@ -267,38 +247,27 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
             pure $ .some invocations
           else
             pure .none
-        let sorrys ← if args.sorrys then
-            Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals })
+        let sorrys := if args.sorrys then
+            Frontend.collectSorrys step
           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) ← 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)
+            let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
+            let stateId ← newGoalState goalState
+            let goals ← goalSerialize goalState options
+            pure (.some stateId, goals)
         return {
           boundary,
-          messages,
           invocations?,
           goalStateId?,
-          goals?,
-          goalSrcBoundaries?,
-          newConstants?,
+          goals,
+          messages,
         }
       return .ok { units }
     catch e =>

Test/Common.lean

@@ -48,12 +48,6 @@ namespace Condensed
 deriving instance BEq, Repr for LocalDecl
 deriving instance BEq, Repr for Goal
 
--- Enable string interpolation
-instance : ToString FVarId where
-  toString id := id.name.toString
-instance : ToString MVarId where
-  toString id := id.name.toString
-
 protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
   {
     decl with fvarId := { name := .anonymous }
@@ -101,19 +95,19 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq)
 
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 
-def strToTermSyntax (s: String): CoreM Syntax := do
+def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do
   let .ok stx := Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := s)
-    (fileName := ← getFileName) | panic! s!"Failed to parse {s}"
+    (fileName := filename) | panic! s!"Failed to parse {s}"
   return stx
 def parseSentence (s: String): Elab.TermElabM Expr := do
   let stx ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := s)
-    (fileName := ← getFileName) with
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
   Elab.Term.elabTerm (stx := stx) .none
@@ -129,30 +123,13 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
 
 -- Monadic testing
 
-abbrev TestT := StateRefT' IO.RealWorld LSpec.TestSeq
+abbrev TestT := StateT LSpec.TestSeq
 
-section Monadic
-
-variable [Monad m] [MonadLiftT (ST IO.RealWorld) m]
-
-def addTest (test: LSpec.TestSeq) : TestT m Unit := do
+def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do
   set $ (← get) ++ test
 
-def checkEq [DecidableEq α] [Repr α] (desc : String) (lhs rhs : α) : TestT m Unit := do
-  addTest $ LSpec.check desc (lhs = rhs)
-def checkTrue (desc : String) (flag : Bool) : TestT m Unit := do
-  addTest $ LSpec.check desc flag
-def fail (desc : String) : TestT m Unit := do
-  addTest $ LSpec.check desc false
-
-def runTest (t: TestT m Unit): m LSpec.TestSeq :=
+def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq :=
   Prod.snd <$> t.run LSpec.TestSeq.done
-def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) :=
-  t.run LSpec.TestSeq.done
-def runTestCoreM (env: Environment) (coreM: TestT CoreM Unit) (options: Array String := #[]): IO LSpec.TestSeq := do
-  runCoreMSeq env (runTest coreM) options
-
-end Monadic
 
 def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
   IO LSpec.TestSeq :=

Test/Delate.lean

@@ -32,10 +32,10 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
 def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × String) := [
     -- This one contains unhygienic variable names which must be suppressed
-    ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"),
+    ("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"),
     -- These ones are normal and easy
     ("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"),
-    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :i) :i)"),
+    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"),
     -- Handling of higher order types
     ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
     ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
@@ -50,8 +50,8 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × (List Name) × String) := [
     ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
     ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
-    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
-    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
+    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
+    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
     ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
   ]
   entries.foldlM (λ suites (source, levels, target) =>
@@ -77,7 +77,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
             .default)
         .implicit)
       .implicit,
-      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)"
+      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :implicit) :implicit)"
     ),
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do

Test/Environment.lean

@@ -97,26 +97,11 @@ def test_inspect: IO LSpec.TestSeq := do
     ) LSpec.TestSeq.done
   runCoreMSeq env inner
 
-def test_symbol_location : TestT IO Unit := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
-  addTest $ ← runTestCoreM env do
-    let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed"
-    checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"
-
-    -- Extraction of source doesn't work for symbols in `Init` for some reason
-    checkTrue "file" result.sourceUri?.isNone
-    checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
-    checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
-
 def suite: List (String × IO LSpec.TestSeq) :=
   [
     ("Catalog", test_catalog),
     ("Symbol Visibility", test_symbol_visibility),
     ("Inspect", test_inspect),
-    ("Symbol Location", runTest test_symbol_location),
   ]
 
 end Pantograph.Test.Environment

Test/Frontend.lean

@@ -6,18 +6,17 @@ import Test.Common
 open Lean Pantograph
 namespace Pantograph.Test.Frontend
 
-def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
-    : MetaM (List GoalState) := do
+def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
   let filename := "<anonymous>"
   let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
   let m := Frontend.mapCompilationSteps λ step => do
-    return (step.before, ← Frontend.collectSorrys step options)
+    return (step.before, Frontend.collectSorrys step)
   let li ← m.run context |>.run' state
   let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
     if sorrys.isEmpty then
       return .none
-    let { state, .. } ← Frontend.sorrysToGoalState sorrys
-    return .some state
+    let goalState ← Frontend.sorrysToGoalState sorrys
+    return .some goalState
   return goalStates
 
 def test_multiple_sorrys_in_proof : TestT MetaM Unit := do
@@ -178,58 +177,6 @@ example (n: Nat) : mystery n + 1 = n + 2 := sorry
     }
   ])
 
-def test_capture_type_mismatch : TestT MetaM Unit := do
-  let input := "
-def mystery (k: Nat) : Nat := true
-  "
-  let options := { collectTypeErrors := true }
-  let goalStates ← (collectSorrysFromSource input options).run' {}
-  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
-  checkEq "goals" ((← goalState.serializeGoals).map (·.devolatilize)) #[
-    {
-      target := { pp? := "Nat" },
-      vars := #[{
-         userName := "k",
-         type? := .some { pp? := "Nat" },
-      }],
-    }
-  ]
-
-def test_capture_type_mismatch_in_binder : TestT MetaM Unit := do
-  let input := "
-example (p: Prop) (h: (∀ (x: Prop), Nat) → p): p := h (λ (y: Nat) => 5)
-  "
-  let options := { collectTypeErrors := true }
-  let goalStates ← (collectSorrysFromSource input options).run' {}
-  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
-  checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
-  ]
-
-def collectNewConstants (source: String) : MetaM (List (List Name)) := do
-  let filename := "<anonymous>"
-  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
-  let m := Frontend.mapCompilationSteps λ step => do
-    Frontend.collectNewDefinedConstants step
-  m.run context |>.run' state
-
-def test_collect_one_constant : TestT MetaM Unit := do
-  let input := "
-def mystery : Nat := 123
-  "
-  let names ← collectNewConstants input
-  checkEq "constants" names [[`mystery]]
-def test_collect_one_theorem : TestT MetaM Unit := do
-  let input := "
-theorem mystery [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
-  match as, i with
-  | a::as, ⟨0, _⟩  => simp_arith [get]
-  | a::as, ⟨i+1, h⟩ =>
-    have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
-    apply Nat.lt_trans ih
-    simp_arith
-  "
-  let names ← collectNewConstants input
-  checkEq "constants" names [[`mystery]]
 
 def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
@@ -238,10 +185,6 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
     ("sorry_in_induction", test_sorry_in_induction),
     ("sorry_in_coupled", test_sorry_in_coupled),
     ("environment_capture", test_environment_capture),
-    ("capture_type_mismatch", test_capture_type_mismatch),
-    --("capture_type_mismatch_in_binder", test_capture_type_mismatch_in_binder),
-    ("collect_one_constant", test_collect_one_constant),
-    ("collect_one_theorem", test_collect_one_theorem),
   ]
   tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test))
 

Test/Integration.lean

@@ -72,8 +72,8 @@ def test_tactic : Test :=
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
     step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
-     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
+    step "goal.print" [("stateId", .num 1)]
+     ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
     step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
   ]
@@ -90,27 +90,27 @@ def test_automatic_mode (automatic: Bool): Test :=
     ],
   }
   let goal2l: Protocol.Goal := {
-    name := "_uniq.61",
+    name := "_uniq.59",
     userName? := .some "inl",
     target := { pp? := .some "q ∨ p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
     ],
   }
   let goal2r: Protocol.Goal := {
-    name := "_uniq.74",
+    name := "_uniq.72",
     userName? := .some "inr",
     target := { pp? := .some "q ∨ p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.62", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
+      { name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
     ],
   }
   let goal3l: Protocol.Goal := {
-    name := "_uniq.80",
+    name := "_uniq.78",
     userName? := .some "inl.h",
     target := { pp? := .some "p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
     ],
   }
   [
@@ -171,11 +171,9 @@ def test_frontend_process : Test :=
     let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
     step "frontend.process"
       [
-        ("file",              .str file),
-        ("invocations",       .bool true),
-        ("sorrys",            .bool false),
-        ("typeErrorsAsGoals", .bool false),
-        ("newConstants",      .bool false),
+        ("file", .str file),
+        ("invocations", .bool true),
+        ("sorrys", .bool false),
       ]
      ({
        units := [{
@@ -216,8 +214,6 @@ def test_frontend_process_sorry : Test :=
         ("file", .str file),
         ("invocations", .bool false),
         ("sorrys", .bool true),
-        ("typeErrorsAsGoals", .bool false),
-        ("newConstants", .bool false),
       ]
      ({
        units := [{
@@ -225,8 +221,7 @@ 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],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
     }: Protocol.FrontendProcessResult),

Test/Library.lean

@@ -24,7 +24,7 @@ def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
       },
       expr := {
         pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩",
-        sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall a 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))",
+        sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))",
       }
     }))
     return tests

Test/Main.lean

@@ -1,12 +1,11 @@
 import LSpec
-import Test.Delate
 import Test.Environment
 import Test.Frontend
 import Test.Integration
 import Test.Library
 import Test.Metavar
 import Test.Proofs
-import Test.Serial
+import Test.Delate
 import Test.Tactic
 
 -- Test running infrastructure
@@ -52,8 +51,6 @@ def main (args: List String) := do
     ("Metavar", Metavar.suite env_default),
     ("Proofs", Proofs.suite env_default),
     ("Delate", Delate.suite env_default),
-    ("Serial", Serial.suite env_default),
-    ("Tactic/Assign", Tactic.Assign.suite env_default),
     ("Tactic/Congruence", Tactic.Congruence.suite env_default),
     ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
     ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),

Test/Metavar.lean

@@ -8,7 +8,10 @@ namespace Pantograph.Test.Metavar
 open Pantograph
 open Lean
 
-abbrev TestM := TestT $ ReaderT Protocol.Options Elab.TermElabM
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
+
+def addTest (test: LSpec.TestSeq): TestM Unit := do
+  set $ (← get) ++ test
 
 -- Tests that all delay assigned mvars are instantiated
 def test_instantiate_mvar: TestM Unit := do
@@ -29,6 +32,8 @@ def test_instantiate_mvar: TestM Unit := do
     "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
   return ()
 
+
+
 def startProof (expr: String): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
   let syn? := parseTerm env expr
@@ -239,7 +244,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
     | .ok state => pure state
   addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Roundtrip
@@ -253,7 +258,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
     | .ok state => pure state
   addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Continuation should fail if the state does not exist:

Test/Proofs.lean

@@ -14,7 +14,10 @@ inductive Start where
   | copy (name: String) -- Start from some name in the environment
   | expr (expr: String) -- Start from some expression
 
-abbrev TestM := TestT $ ReaderT Protocol.Options $ Elab.TermElabM
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
+
+def addTest (test: LSpec.TestSeq): TestM Unit := do
+  set $ (← get) ++ test
 
 def startProof (start: Start): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
@@ -97,7 +100,7 @@ def test_identity: TestM Unit := do
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
     #[inner])
   let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
 
 -- Individual test cases
@@ -241,15 +244,13 @@ def test_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let [state1g0] := state1.goals | fail "Should have 1 goal"
-  let (fvP, fvQ, fvH) ← state1.withContext state1g0 do
-    let lctx ← getLCtx
-    let #[fvP, fvQ, fvH] := lctx.getFVarIds.map (toString ·.name) |
-      panic! "Incorrect number of decls"
-    pure (fvP, fvQ, fvH)
+  let fvP := "_uniq.10"
+  let fvQ := "_uniq.13"
+  let fvH := "_uniq.16"
+  let state1g0 := "_uniq.17"
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
     #[{
-      name := state1g0.name.toString,
+      name := state1g0,
       target := { pp? := .some "q ∨ p" },
       vars := #[
         { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
@@ -261,7 +262,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
 
   let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
   let tactic := "cases h"
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
@@ -271,21 +272,19 @@ def test_or_comm: TestM Unit := do
       return ()
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[branchGoal "inl" "p", branchGoal "inr" "q"])
-  let [state2g0, state2g1] := state2.goals |
-    fail s!"Should have 2 goals, but it has {state2.goals.length}"
-  let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
+  let (caseL, caseR) := ("_uniq.64", "_uniq.77")
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
     #[caseL, caseR])
   addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
   let state2parent ← state2.withParentContext do
-    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
   let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
   let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
-  let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
-  let caseL := s!"(:lambda h (:fv {fvP}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))"
-  let caseR := s!"(:lambda h (:fv {fvQ}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))"
+  let motive := s!"(:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
+  let caseL := s!"(:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))"
+  let caseR := s!"(:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))"
   let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))"
   addTest $ LSpec.test "(2 parent)" (state2parent ==
     s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
@@ -296,9 +295,8 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   let state3_1parent ← state3_1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
-  let [state3_1goal0] := state3_1.goals | fail "Should have 1 goal"
-  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
+    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
@@ -564,15 +562,12 @@ def test_nat_zero_add: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
-      fail "Incorrect number of goals"
-  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal mvarMotive.name.toString  [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal mvarMajor.name.toString   [("n", "Nat")] "Nat",
-      buildNamedGoal mvarInduct.name.toString  [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "exact n"
@@ -655,15 +650,13 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
-      fail "Incorrect number of goals"
-  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
+  let major := "_uniq.68"
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal mvarMotive.name.toString [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal mvarMajor.name.toString [("n", "Nat")] "Nat",
-      buildNamedGoal mvarInduct.name.toString [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal major [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "intro x"
@@ -680,7 +673,8 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let [eqL, eqR, eqT] := state3m2.goals | fail "Incorrect number of goals"
+  let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
+  addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
   let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
   let state2b ← match state3m2.resume [conduit] with
     | .ok state => pure state
@@ -690,86 +684,26 @@ def test_nat_zero_add_alt: TestM Unit := do
 
   let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
   let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
-  let fvN ← state2b.withContext conduit do
-    let lctx ← getLCtx
-    pure $ lctx.getFVarIds.get! 0 |>.name
+  let fvN := "_uniq.63"
   let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
-  let substOf (mvarId: MVarId) := s!"(:subst (:mv {mvarId.name}) (:fv {fvN}) (:mv {mvarMajor}))"
-  let .num _ nL := eqL.name | fail "Incorrect form of mvar id"
-  let .num _ nR := eqR.name | fail "Incorrect form of mvar id"
-  let nL' := nL + 4
-  let nR' := nR + 5
+  let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
   addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
     #[
       {
-        name := mvarConduit.name.toString,
+        name := "_uniq.70",
         userName? := .some "conduit",
         target := {
-          pp? := .some s!"(?m.{nL'} ?m.{major} = ?m.{nR'} ?m.{major}) = (n + 0 = n)",
+          pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
           sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
         },
         vars := #[{
-          name := fvN.toString,
+          name := fvN,
           userName := "n",
           type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
         }],
       }
     ])
 
-def test_tactic_failure_unresolved_goals : TestM Unit := do
-  let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
-  let tactic := "intro p"
-  let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-
-  let tactic := "exact ⟨0, by simp⟩"
-  let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
-  checkEq s!"{tactic} fails" messages #[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")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
-  let tactic := "intro p q r h"
-  let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-
-  let iex : InternalExceptionId := { idx := 4 }
-  IO.println s!"{← iex.getName}"
-  let tactic := "simpa [h] using And.imp_left h _"
-  --let state2 ← match ← state1.tacticOn 0 tactic with
-  --  | .success state => pure state
-  --  | other => do
-  --    addTest $ assertUnreachable $ other.toString
-  --    return ()
-
-  -- Volatile behaviour. This easily changes across Lean versions
-
-  --checkEq tactic ((← state2.serializeGoals).map (·.devolatilize))  #[
-  --  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 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"
-  checkEq s!"{tactic} fails" messages #[message]
-
-
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("identity", test_identity),
@@ -782,8 +716,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("calc", test_calc),
     ("Nat.zero_add", test_nat_zero_add),
     ("Nat.zero_add alt", test_nat_zero_add_alt),
-    ("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals),
-    ("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))
 

Test/Serial.lean

@@ -1,109 +0,0 @@
-import LSpec
-import Test.Common
-import Lean
-import Pantograph.Library
-
-open Lean
-
-namespace Pantograph.Test.Serial
-
-def tempPath : IO System.FilePath := do
-  Prod.snd <$> IO.FS.createTempFile
-
-structure MultiState where
-  coreContext : Core.Context
-  env: Environment
-
-abbrev TestM := TestT $ StateRefT MultiState $ IO
-
-instance : MonadEnv TestM where
-  getEnv      := return (← getThe MultiState).env
-  modifyEnv f := do modifyThe MultiState fun s => { s with env := f s.env }
-
-def runCoreM { α } (state : Core.State) (testCoreM : TestT CoreM α) : TestM (α × Core.State) := do
-  let multiState ← getThe MultiState
-  let coreM := runTestWithResult testCoreM
-  match ← (coreM.run multiState.coreContext state).toBaseIO with
-  | .error e => do
-    throw $ .userError $ ← e.toMessageData.toString
-  | .ok ((a, tests), state') => do
-    set $ (← getThe LSpec.TestSeq) ++ tests
-    return (a, state')
-
-def test_environment_pickling : TestM Unit := do
-  let coreSrc : Core.State := { env := ← getEnv }
-  let coreDst : Core.State := { env := ← getEnv }
-
-  let name := `mystery
-  let envPicklePath ← tempPath
-  let ((), _) ← runCoreM coreSrc do
-    let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
-    let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default
-    let c := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
-      (name := name)
-      (levelParams := [])
-      (type := type)
-      (value := value)
-      (hints := Lean.mkReducibilityHintsRegularEx 1)
-      (safety := Lean.DefinitionSafety.safe)
-      (all := [])
-    let env' ← match (← getEnv).addDecl (← getOptions) c with
-      | .error e => do
-        let error ← (e.toMessageData (← getOptions)).toString
-        throwError error
-      | .ok env' => pure env'
-    environmentPickle env' envPicklePath
-
-  let _ ← runCoreM coreDst do
-    let (env', _) ← environmentUnpickle envPicklePath
-    checkTrue s!"Has symbol {name}" (env'.find? name).isSome
-    let anotherName := `mystery2
-    checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone
-
-  IO.FS.removeFile envPicklePath
-
-def test_goal_state_pickling_simple : TestM Unit := do
-  let coreSrc : Core.State := { env := ← getEnv }
-  let coreDst : Core.State := { env := ← getEnv }
-  let statePath ← tempPath
-
-  let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
-  let stateGenerate : MetaM GoalState := runTermElabMInMeta do
-    GoalState.create type
-
-  let ((), _) ← runCoreM coreSrc do
-    let state ← stateGenerate.run'
-    goalStatePickle state statePath
-
-  let ((), _) ← runCoreM coreDst do
-    let (goalState, _) ← goalStateUnpickle statePath (← getEnv)
-    let metaM : MetaM (List Expr) := do
-      goalState.goals.mapM λ goal => goalState.withContext goal goal.getType
-    let types ← metaM.run'
-    checkTrue "Goals" $ types[0]!.equal type
-
-  IO.FS.removeFile statePath
-
-structure Test where
-  name : String
-  routine: TestM Unit
-
-protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do
-  -- Create the state
-  let state : MultiState := {
-    coreContext := ← createCoreContext #[],
-    env,
-  }
-  match ← ((runTest $ test.routine).run' state).toBaseIO with
-  | .ok e => return e
-  | .error e =>
-    return LSpec.check s!"Emitted exception: {e.toString}" (e.toString == "")
-
-def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
-  let tests: List Test := [
-    { name := "environment_pickling", routine := test_environment_pickling, },
-    { name := "goal_state_pickling_simple", routine := test_goal_state_pickling_simple, },
-  ]
-  tests.map (fun test => (test.name, test.run env))
-
-end Pantograph.Test.Serial

Test/Tactic.lean

@@ -1,4 +1,3 @@
-import Test.Tactic.Assign
 import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse

Test/Tactic/Assign.lean

@@ -1,33 +0,0 @@
-import Lean.Meta
-import Lean.Elab
-import LSpec
-import Test.Common
-
-open Lean
-
-namespace Pantograph.Test.Tactic.Assign
-
-def test_draft : TestT Elab.TermElabM Unit := do
-  let expr := "forall (p : Prop), (p ∨ p) ∨ p"
-  let skeleton := "by\nhave a : p ∨ p := sorry\nsorry"
-  let expr ← parseSentence expr
-  Meta.forallTelescope expr $ λ _ body => do
-    let skeleton' ← match Parser.runParserCategory
-      (env := ← MonadEnv.getEnv)
-      (catName := `term)
-      (input := skeleton)
-      (fileName := ← getFileName) with
-      | .ok syn => pure syn
-      | .error error => throwError "Failed to parse: {error}"
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.evalDraft skeleton'
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = ["p ∨ p", "(p ∨ p) ∨ p"])
-
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("draft", test_draft),
-  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
-
-end Pantograph.Test.Tactic.Assign

Test/Tactic/Congruence.lean

@@ -28,7 +28,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do
     let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse")
     addTest $ LSpec.check "apply" (results.length = 0)
     addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
-    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(List.reverse ?a₁ = List.reverse ?a₂) = (l1.reverse = l2.reverse)")
+    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")
 def test_congr_arg : TestT Elab.TermElabM Unit := do
   let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
   let expr ← parseSentence expr
@@ -37,7 +37,7 @@ def test_congr_arg : TestT Elab.TermElabM Unit := do
     let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
     addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
-        (`α, "Sort ?u.73"),
+        (`α, "Sort ?u.70"),
         (`a₁, "?α"),
         (`a₂, "?α"),
         (`f, "?α → Nat"),
@@ -52,7 +52,7 @@ def test_congr_fun : TestT Elab.TermElabM Unit := do
     let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
     addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
-        (`α, "Sort ?u.165"),
+        (`α, "Sort ?u.159"),
         (`f₁, "?α → Nat"),
         (`f₂, "?α → Nat"),
         (`h, "?f₁ = ?f₂"),

Test/Tactic/MotivatedApply.lean

@@ -28,7 +28,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "@Nat.brecOn")
-      (fileName := ← getFileName) with
+      (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
         "Nat → Prop",
         "Nat",
         "∀ (t : Nat), Nat.below t → ?motive t",
-        "?motive ?m.74 = (n + 0 = n)",
+        "?motive ?m.67 = (n + 0 = n)",
       ])
     addTest test
 
@@ -52,7 +52,7 @@ def test_list_brec_on : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "@List.brecOn")
-      (fileName := ← getFileName) with
+      (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -74,7 +74,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := "@Nat.brecOn")
-    (fileName := ← getFileName) with
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
   let expr ← parseSentence expr
@@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
     let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
-    let majorId := 74
+    let majorId := 67
     addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
       [
         "Nat → Prop",
@@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
 
     addTest $ ← conduit.withContext do
       let t := toString (← Meta.ppExpr $ ← conduit.getType)
-      return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)")
+      return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [

Test/Tactic/NoConfuse.lean

@@ -15,7 +15,7 @@ def test_nat : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "h")
-      (fileName := ← getFileName) with
+      (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -32,7 +32,7 @@ def test_nat_fail : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "h")
-      (fileName := ← getFileName) with
+      (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -52,7 +52,7 @@ def test_list : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "h")
-      (fileName := ← getFileName) with
+      (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic

Test/Tactic/Prograde.lean

@@ -15,7 +15,7 @@ def test_define : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "Or.inl h")
-      (fileName := ← getFileName) with
+      (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic

doc/icon.svg

@@ -4,17 +4,17 @@
 <svg
    width="256"
    height="256"
-   viewBox="0 0 67.733332 67.733333"
+   viewBox="0 0 55.900957 55.900957"
    version="1.1"
-   id="svg1"
+   id="svg21534"
+   xml:space="preserve"
+   inkscape:version="1.2.2 (b0a8486541, 2022-12-01)"
    sodipodi:docname="icon.svg"
-   inkscape:version="1.3.2 (091e20ef0f, 2023-11-25, custom)"
    xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
    xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
    xmlns="http://www.w3.org/2000/svg"
-   xmlns:svg="http://www.w3.org/2000/svg">
-  <sodipodi:namedview
-     id="namedview1"
+   xmlns:svg="http://www.w3.org/2000/svg"><sodipodi:namedview
+     id="namedview21536"
      pagecolor="#ffffff"
      bordercolor="#111111"
      borderopacity="1"
@@ -23,135 +23,51 @@
      inkscape:pagecheckerboard="1"
      inkscape:deskcolor="#d1d1d1"
      inkscape:document-units="px"
-     showguides="true"
-     inkscape:zoom="5.1882633"
-     inkscape:cx="81.819286"
-     inkscape:cy="132.22151"
-     inkscape:window-width="3774"
-     inkscape:window-height="2126"
+     showgrid="true"
+     inkscape:zoom="5.1754899"
+     inkscape:cx="158.82554"
+     inkscape:cy="91.682142"
+     inkscape:window-width="3777"
+     inkscape:window-height="2093"
      inkscape:window-x="0"
      inkscape:window-y="0"
      inkscape:window-maximized="1"
-     inkscape:current-layer="layer2">
-    <sodipodi:guide
-       position="33.866666,69.8437"
-       orientation="-1,0"
-       id="guide1"
-       inkscape:locked="false"
-       inkscape:label=""
-       inkscape:color="rgb(0,134,229)" />
-    <sodipodi:guide
-       position="-27.673679,33.866666"
-       orientation="0,1"
-       id="guide2"
-       inkscape:locked="false"
-       inkscape:label=""
-       inkscape:color="rgb(0,134,229)" />
-    <sodipodi:guide
-       position="16.933333,29.94582"
-       orientation="-1,0"
-       id="guide3"
-       inkscape:locked="false"
-       inkscape:label=""
-       inkscape:color="rgb(0,134,229)" />
-    <sodipodi:guide
-       position="50.799999,37.44627"
-       orientation="-1,0"
-       id="guide4"
-       inkscape:locked="false"
-       inkscape:label=""
-       inkscape:color="rgb(0,134,229)" />
-    <sodipodi:guide
-       position="31.336956,16.933333"
-       orientation="0,1"
-       id="guide5"
-       inkscape:locked="false"
-       inkscape:label=""
-       inkscape:color="rgb(0,134,229)" />
-    <sodipodi:guide
-       position="24.528038,25.4"
-       orientation="0,1"
-       id="guide6"
-       inkscape:locked="false"
-       inkscape:label=""
-       inkscape:color="rgb(0,134,229)" />
-    <sodipodi:guide
-       position="33.866666,50.799999"
-       orientation="0,1"
-       id="guide7"
-       inkscape:locked="false"
-       inkscape:label=""
-       inkscape:color="rgb(0,134,229)" />
-    <sodipodi:guide
-       position="32.770414,55.033333"
-       orientation="0,1"
-       id="guide8"
-       inkscape:locked="false"
-       inkscape:label=""
-       inkscape:color="rgb(0,134,229)" />
-    <sodipodi:guide
-       position="25.347689,33.866666"
-       orientation="1,0"
-       id="guide9"
-       inkscape:locked="false" />
-    <sodipodi:guide
-       position="25.347689,42.333333"
-       orientation="0,1"
-       id="guide10"
-       inkscape:locked="false"
-       inkscape:label=""
-       inkscape:color="rgb(0,134,229)" />
-  </sodipodi:namedview>
-  <defs
-     id="defs1" />
-  <g
+     inkscape:current-layer="layer1"><inkscape:grid
+       type="xygrid"
+       id="grid23833"
+       spacingx="3.4938098"
+       spacingy="3.4938098"
+       empspacing="4" /></sodipodi:namedview><defs
+     id="defs21531" /><g
+     inkscape:label="Layer 1"
      inkscape:groupmode="layer"
-     id="layer4"
-     inkscape:label="bg" />
-  <g
-     inkscape:groupmode="layer"
-     id="layer1"
-     inkscape:label="Circle">
-    <path
-       id="path1"
-       style="fill:#666b98;fill-rule:evenodd;stroke:#ffffff;stroke-width:0.0191989;stroke-miterlimit:3.4;fill-opacity:1"
-       d="M 33.866666 0.009818522 A 33.857067 33.857067 0 0 0 0.009818522 33.866666 A 33.857067 33.857067 0 0 0 33.866666 67.723514 A 33.857067 33.857067 0 0 0 67.723514 33.866666 A 33.857067 33.857067 0 0 0 33.866666 0.009818522 z M 33.866666 4.2416015 A 29.624933 29.624933 0 0 1 63.491731 33.866666 A 29.624933 29.624933 0 0 1 33.866666 63.491731 A 29.624933 29.624933 0 0 1 4.2416015 33.866666 A 29.624933 29.624933 0 0 1 33.866666 4.2416015 z " />
-  </g>
-  <g
-     inkscape:groupmode="layer"
-     id="layer2"
-     inkscape:label="Pantograph-Core">
-    <rect
-       style="fill:#666b98;fill-opacity:1;fill-rule:evenodd;stroke:#ffffff;stroke-width:0.01905;stroke-miterlimit:3.4"
-       id="rect8"
-       width="16.942858"
-       height="4.2257233"
-       x="33.866665"
-       y="12.7"
-       rx="0.58070719"
-       ry="0.34097314" />
-    <rect
-       style="fill:#666b98;fill-opacity:1;fill-rule:evenodd;stroke:#ffffff;stroke-width:0.01905;stroke-miterlimit:3.4"
-       id="rect1"
-       width="33.885715"
-       height="8.4211359"
-       x="16.933332"
-       y="42.333332"
-       rx="0.58070719"
-       ry="0.34097314" />
-    <path
-       style="fill:#666b98;fill-opacity:1;stroke:none;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
-       d="m 42.338095,16.925724 -16.990406,8.474275 13.121218,16.923808 -4.602241,0.0095 -4.254289,0.0015 -8.564029,-16.934789 17.310554,-8.464751 z"
-       id="path10"
-       sodipodi:nodetypes="cccccccc" />
-    <path
-       style="fill:none;stroke:#666b98;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
-       d="M 46.53445,16.925724 26.018901,26.73418"
-       id="path11" />
-    <path
-       style="fill:none;stroke:#666b98;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
-       d="m 21.048348,25.399999 4.352167,16.934808"
-       id="path12"
-       sodipodi:nodetypes="cc" />
-  </g>
-</svg>
+     id="layer1"><rect
+       style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:1.78013;stroke-miterlimit:3.4;stroke-dasharray:none"
+       id="rect26805"
+       width="11.502316"
+       height="2.2512667"
+       x="33.344425"
+       y="7.6690259"
+       ry="0.28140834"
+       rx="0.47926313" /><path
+       style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
+       d="m 35.764667,9.9513013 c 0,0 -26.8581417,13.7987337 -28.0863506,14.9501437 -1.250042,1.171878 3.2347846,3.945325 3.2347846,3.945325 l 21.34979,14.934062 6.624567,0.453105 -27.599216,-17.304358 c 0,0 -0.603209,-0.08927 -0.600411,-0.762283 0.0028,-0.673015 27.32022,-16.4227356 27.32022,-16.4227356 z"
+       id="path27381"
+       sodipodi:nodetypes="csccccscc" /><path
+       style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
+       d="M 10.97848,26.985751 40.537772,9.7943227 41.921795,9.7005084 11.210626,27.421377 Z"
+       id="path27479" /><path
+       style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
+       d="m 7.0509847,25.522367 c -0.8266141,1.386819 -2.4011783,4.48805 -2.4706357,4.90223 -0.069458,0.414182 0.4434324,0.513474 0.8491061,0.757041 C 5.835129,31.425204 19.33424,43.917182 19.33424,43.917182 l 0.324562,-0.539228 c 0,0 -14.2055729,-12.369493 -14.0644435,-12.868167 0.1411292,-0.498672 3.544896,-3.777392 3.544896,-3.777392 L 7.4596884,25.117508 Z"
+       id="path27481" /><rect
+       style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:2.11692;stroke-miterlimit:3.4;stroke-dasharray:none;stroke-opacity:1"
+       id="rect27483"
+       width="36.38942"
+       height="3.6217353"
+       x="13.953447"
+       y="43.009739"
+       rx="0.43672624"
+       ry="0.43672624" /><path
+       style="fill:none;stroke:#000000;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+       d="M -2.1119274,7.666599 H 64.179192"
+       id="path27487" /></g></svg>

doc/rationale.md

@@ -1,59 +0,0 @@
-# Design Rationale
-
-A great problem in machine learning is to use ML agents to automatically prove
-mathematical theorems. This sort of proof necessarily involves *search*.
-Compatibility for search is the main reason for creating Pantograph.  The Lean 4
-LSP interface is not conducive to search. Pantograph is designed with this in
-mind. It emphasizes the difference between 3 views of a proof:
-
-- **Presentation View**: The view of a written, polished proof. e.g. Mathlib and
-  math papers are almost always written in this form.
-- **Search View**: The view of a proof exploration trajectory. This is not
-  explicitly supported by Lean LSP.
-- **Kernel View**: The proof viewed as a set of metavariables.
-
-Pantograph enables proof agents to operate on the search view.
-
-## Name
-
-The name Pantograph is a pun. It means two things
-- A pantograph is an instrument for copying down writing. As an agent explores
-  the vast proof search space, Pantograph records the current state to ensure
-  the proof is sound.
-- A pantograph is also an equipment for an electric train. It supplies power to
-  a locomotive. In comparison the (relatively) simple Pantograph software powers
-  theorem proving projects.
-
-## Caveats and Limitations
-
-Pantograph does not exactly mimic Lean LSP's behaviour. That would not grant the
-flexibility it offers.  To support tree search means Pantograph has to act
-differently from Lean in some times, but never at the sacrifice of soundness.
-
-- When Lean LSP says "don't know how to synthesize placeholder", this indicates
-  the human operator needs to manually move the cursor to the placeholder and
-  type in the correct expression. This error therefore should not halt the proof
-  process, and the placeholder should be turned into a goal.
-- When Lean LSP says "unresolved goals", that means a proof cannot finish where
-  it is supposed to finish at the end of a `by` block. Pantograph will raise the
-  error in this case, since it indicates the termination of a proof search branch.
-- `pick_goal` or `swap` will not work since they run contrary to tree search
-  paradigms. However, if there are tactics which perform non-trivial operations
-  to multiple goals at the same time, this constrain could potentially be
-  relaxed at a cost of great bookkeeping overhead to the user.
-
-Pantograph cannot perform things that are inherently constrained by Lean. These
-include:
-
-- If a tactic loses track of metavariables, it will not be caught until the end
-  of the proof search. This is a bug in the tactic itself.
-- Timeouts for executing tactics is not available. Maybe this will change in the
-  future.
-- Interceptions of parsing errors generally cannot be turned into goals (e.g.
-  `def mystery : Nat := :=`) due to Lean's parsing system.
-
-
-## References
-
-* [Pantograph Paper](https://arxiv.org/abs/2410.16429)
-

doc/repl.md

@@ -1,68 +0,0 @@
-# REPL
-
-## Commands
-
-See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
-* `reset`: Delete all cached expressions and proof trees
-* `stat`: Display resource usage
-* `expr.echo {"expr": <expr>, "type": <optional expected type>, ["levels": [<levels>]]}`: Determine the
-  type of an expression and format it.
-* `env.catalog`: Display a list of all safe Lean symbols in the current environment
-* `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
-  given symbol; If value flag is set, the value is printed or hidden. By default
-  only the values of definitions are printed.
-* `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the
-  current environment to/from a file
-* `options.set { key: value, ... }`: Set one or more options (not Lean options; those
-  have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
-
-  One particular option for interest for machine learning researchers is the
-  automatic mode (flag: `"automaticMode"`).  By default it is turned on, with
-  all goals automatically resuming. This makes Pantograph act like a gym,
-  with no resumption necessary to manage your goals.
-* `options.print`: Display the current set of options
-* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
-  Start a new proof from a given expression or symbol
-* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
-  given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
-  - `{ "tactic": <tactic> }`: Execute an ordinary tactic
-  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
-  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
-  - `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
-    be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
-    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.
-  - `{ "goals": <names> }`: Resume the given goals
-* `goal.remove {"stateIds": [<id>]}"`: Drop the goal states specified in the list
-* `goal.print {"stateId": <id>}"`: Print a goal state
-* `goal.save { "id": <id>, "path": <fileName> }`, `goal.load { "path": <fileName> }`:
-  Save/Load a goal state to/from a file. The environment is not carried with the
-  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> }`:
-  Executes the Lean frontend on a file, collecting the tactic invocations
-  (`"invocations": true`), the sorrys and type errors into goal states
-  (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
-  `sorrys`, this command additionally outputs the position of each captured
-  `sorry`.
-
-## Errors
-
-When an error pertaining to the execution of a command happens, the returning JSON structure is
-
-``` json
-{ "error": "type", "desc": "description" }
-```
-Common error forms:
-* `command`: Indicates malformed command structure which results from either
-  invalid command or a malformed JSON structure that cannot be fed to an
-  individual command.
-* `index`: Indicates an invariant maintained by the output of one command and
-  input of another is broken. For example, attempting to query a symbol not
-  existing in the library or indexing into a non-existent proof state.

flake.lock

@@ -42,11 +42,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1736388194,
-        "narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=",
+        "lastModified": 1731711316,
+        "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2",
+        "rev": "136fc6057c48de970579e960b62421e9c295b67d",
         "type": "github"
       },
       "original": {

flake.nix

@@ -18,89 +18,80 @@
     lean4-nix,
     lspec,
     ...
-  }:
-    flake-parts.lib.mkFlake {inherit inputs;} {
-      flake = {
+  } : flake-parts.lib.mkFlake { inherit inputs; } {
+    flake = {
+    };
+    systems = [
+      "x86_64-linux"
+      "x86_64-darwin"
+    ];
+    perSystem = { system, pkgs, ... }: let
+      pkgs = import nixpkgs {
+        inherit system;
+        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
       };
-      systems = [
-        "aarch64-linux"
-        "aarch64-darwin"
-        "x86_64-linux"
-        "x86_64-darwin"
-      ];
-      perSystem = {
-        system,
-        pkgs,
-        ...
-      }: let
-        pkgs = import nixpkgs {
-          inherit system;
-          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
-        };
-        lspecLib = pkgs.lean.buildLeanPackage {
-          name = "LSpec";
-          roots = ["Main" "LSpec"];
-          src = "${lspec}";
-        };
-        project = pkgs.lean.buildLeanPackage {
-          name = "Pantograph";
-          roots = ["Pantograph"];
-          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-            src = ./.;
-            filter = path: type:
-              !(pkgs.lib.hasInfix "/Test/" path)
-              && !(pkgs.lib.hasSuffix ".md" path)
-              && !(pkgs.lib.hasSuffix "Repl.lean" path);
-          });
-        };
-        repl = pkgs.lean.buildLeanPackage {
-          name = "Repl";
-          roots = ["Main" "Repl"];
-          deps = [project];
-          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-            src = ./.;
-            filter = path: type:
-              !(pkgs.lib.hasInfix "/Test/" path)
-              && !(pkgs.lib.hasSuffix ".md" path);
-          });
-        };
-        test = pkgs.lean.buildLeanPackage {
-          name = "Test";
-          # NOTE: The src directory must be ./. since that is where the import
-          # root begins (e.g. `import Test.Environment` and not `import
-          # Environment`) and thats where `lakefile.lean` resides.
-          roots = ["Test.Main"];
-          deps = [lspecLib repl];
-          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-            src = ./.;
-            filter = path: type:
-              !(pkgs.lib.hasInfix "Pantograph" path);
-          });
-        };
-      in rec {
-        packages = {
-          inherit (pkgs.lean) lean lean-all;
-          inherit (project) sharedLib iTree;
-          inherit (repl) executable;
-          default = repl.executable;
-        };
-        legacyPackages = {
-          inherit project;
-          leanPkgs = pkgs.lean;
-        };
-        checks = {
-          test =
-            pkgs.runCommand "test" {
-              buildInputs = [test.executable pkgs.lean.lean-all];
-            } ''
-              #export LEAN_SRC_PATH="${./.}"
-              ${test.executable}/bin/test > $out
-            '';
-        };
-        formatter = pkgs.alejandra;
-        devShells.default = pkgs.mkShell {
-          buildInputs = [pkgs.lean.lean-all pkgs.lean.lean];
-        };
+      lspecLib = pkgs.lean.buildLeanPackage {
+        name = "LSpec";
+        roots = [ "Main" "LSpec" ];
+        src = "${lspec}";
+      };
+      project = pkgs.lean.buildLeanPackage {
+        name = "Pantograph";
+        roots = [ "Pantograph" ];
+        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "/Test/" path) &&
+            !(pkgs.lib.hasSuffix ".md" path) &&
+            !(pkgs.lib.hasSuffix "Repl.lean" path);
+        });
+      };
+      repl = pkgs.lean.buildLeanPackage {
+        name = "Repl";
+        roots = [ "Main" "Repl" ];
+        deps = [ project ];
+        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "/Test/" path) &&
+            !(pkgs.lib.hasSuffix ".md" path);
+        });
+      };
+      test = pkgs.lean.buildLeanPackage {
+        name = "Test";
+        # NOTE: The src directory must be ./. since that is where the import
+        # root begins (e.g. `import Test.Environment` and not `import
+        # Environment`) and thats where `lakefile.lean` resides.
+        roots = [ "Test.Main" ];
+        deps = [ lspecLib repl ];
+        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "Pantograph" path);
+        });
+      };
+    in rec {
+      packages = {
+        inherit (pkgs.lean) lean lean-all;
+        inherit (project) sharedLib iTree;
+        inherit (repl) executable;
+        default = repl.executable;
+      };
+      legacyPackages = {
+        inherit project;
+        leanPkgs = pkgs.lean;
+      };
+      checks = {
+        test = pkgs.runCommand "test" {
+          buildInputs = [ test.executable pkgs.lean.lean-all ];
+        } ''
+          #export LEAN_SRC_PATH="${./.}"
+          ${test.executable}/bin/test > $out
+        '';
+      };
+      devShells.default = pkgs.mkShell {
+        buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
       };
     };
+  };
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.12.0