Merge pull request 'chore: Update Lean to v4.18.0' (#185) from chore/version into dev

Reviewed-on: #185

.gitignore

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

Main.lean

@@ -10,23 +10,26 @@ open Pantograph.Protocol
 
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parseCommand (s: String): Except String Command := do
-  let s := s.trim
-  match s.get? 0 with
-  | .some '{' => -- Parse in Json mode
+  match s.trim.get? 0 with
+  | .some '{' =>
+    -- Parse in Json mode
     Lean.fromJson? (← Lean.Json.parse s)
-  | .some _ => -- Parse in line mode
+  | .some _ =>
+    -- Parse in line mode
     let offset := s.posOf ' ' |> s.offsetOfPos
     if offset = s.length then
       return { cmd := s.take offset, payload := Lean.Json.null }
     else
       let payload ← s.drop offset |> Lean.Json.parse
       return { cmd := s.take offset, payload := payload }
-  | .none => throw "Command is empty"
+  | .none =>
+    throw "Command is empty"
 
-partial def loop : MainM Unit := do
+partial def loop : MainM Unit := do repeat do
   let state ← get
   let command ← (← IO.getStdin).getLine
-  if command.trim.length = 0 then return ()
+  -- Halt the program if empty line is given
+  if command.trim.length = 0 then break
   match parseCommand command with
   | .error error =>
     let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
@@ -40,32 +43,27 @@ partial def loop : MainM Unit := do
         | false => ret.compress
       IO.println str
     catch e =>
-      let message ← e.toMessageData.toString
+      let message := e.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
       IO.println error.compress
-  loop
 
 
 unsafe def main (args: List String): IO Unit := do
   -- NOTE: A more sophisticated scheme of command line argument handling is needed.
-  -- Separate imports and options
   if args == ["--version"] then do
     IO.println s!"{Pantograph.version}"
     return
 
   Pantograph.initSearch ""
 
-  let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
-    |>.toArray |> Pantograph.createCoreContext
-  let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
+  -- Separate imports and options
+  let (options, imports) := args.partition (·.startsWith "--")
+  let coreContext ← options.map (·.drop 2) |>.toArray |> Pantograph.createCoreContext
   let coreState ← Pantograph.createCoreState imports.toArray
-  let context: Context := {
-    imports
-  }
   try
-    let coreM := loop.run context |>.run' {}
+    let mainM := loop.run { coreContext } |>.run' { env := coreState.env }
     IO.println "ready."
-    discard <| coreM.toIO coreContext coreState
+    mainM
   catch ex =>
     let message := ex.toString
     let error  := Lean.toJson ({ error := "io", desc := message }: InteractionError)

Pantograph/Delate.lean

@@ -12,31 +12,72 @@ open Lean
 
 namespace Pantograph
 
-structure ProjectionApplication where
-  projector: Name
-  numParams: Nat
-  inner: Expr
+inductive Projection where
+  -- Normal field case
+  | field (projector : Name) (numParams : Nat)
+  -- Singular inductive case
+  | singular (recursor : Name) (numParams : Nat) (numFields : Nat)
+
+/-- Converts a `.proj` expression to a form suitable for exporting/transpilation -/
+@[export pantograph_analyze_projection]
+def analyzeProjection (env: Environment) (e: Expr): Projection :=
+  let (typeName, idx, _) := match e with
+    | .proj typeName idx struct => (typeName, idx, struct)
+    | _ => panic! "Argument must be proj"
+  if (getStructureInfo? env typeName).isSome then
+    let ctor := getStructureCtor env typeName
+    let fieldName := (getStructureFields env typeName)[idx]!
+    let projector := getProjFnForField? env typeName fieldName |>.get!
+    .field projector ctor.numParams
+  else
+    let recursor := mkRecOnName typeName
+    let ctor := getStructureCtor env typeName
+    .singular recursor ctor.numParams ctor.numFields
+
+def anonymousLevel : Level := .mvar ⟨.anonymous⟩
 
 @[export pantograph_expr_proj_to_app]
-def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
-  let (typeName, idx, inner) := match e with
-    | .proj typeName idx inner => (typeName, idx, inner)
-    | _ => panic! "Argument must be proj"
-  let ctor := getStructureCtor env typeName
-  let fieldName := getStructureFields env typeName |>.get! idx
-  let projector := getProjFnForField? env typeName fieldName |>.get!
-  {
-    projector,
-    numParams := ctor.numParams,
-    inner,
-  }
+def exprProjToApp (env : Environment) (e : Expr) : Expr :=
+  let anon : Expr := .mvar ⟨.anonymous⟩
+  match analyzeProjection env e with
+  | .field projector numParams =>
+    let info := match env.find? projector with
+      | .some info => info
+      | _ => panic! "Illegal projector"
+    let callee := .const projector $ List.replicate info.numLevelParams anonymousLevel
+    let args := (List.replicate numParams anon) ++ [e.projExpr!]
+    mkAppN callee args.toArray
+  | .singular recursor numParams numFields =>
+    let info := match env.find? recursor with
+      | .some info => info
+      | _ => panic! "Illegal recursor"
+    let callee := .const recursor $ List.replicate info.numLevelParams anonymousLevel
+    let typeArgs := List.replicate numParams anon
+    -- Motive type can be inferred directly
+    let motive := .lam .anonymous anon anon .default
+    let major := e.projExpr!
+    -- Generate a lambda of `numFields` parameters, and returns the `e.projIdx!` one.
+    let induct := List.foldl
+      (λ acc _ => .lam .anonymous anon acc .default)
+      (.bvar $ (numFields - e.projIdx! - 1))
+      (List.range numFields)
+    mkAppN callee (typeArgs ++ [motive, major, induct]).toArray
 
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-@[export pantograph_unfold_aux_lemmas]
-def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
-  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
+@[export pantograph_unfold_aux_lemmas_m]
+def unfoldAuxLemmas : Expr → CoreM Expr :=
+  (Meta.deltaExpand · Lean.Name.isAuxLemma)
+/-- Unfold all matcher applications -/
+@[export pantograph_unfold_matchers_m]
+def unfoldMatchers (expr : Expr) : CoreM Expr :=
+  Core.transform expr λ e => do
+    let .some mapp ← Meta.matchMatcherApp? e | return .continue e
+    let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist"
+    let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList
+    let mdata := KVMap.empty.insert `matcher (DataValue.ofName mapp.matcherName)
+    return .visit $ .mdata mdata (f.betaRev e.getAppRevArgs (useZeta := true))
 
 /--
 Force the instantiation of delayed metavariables even if they cannot be fully
@@ -53,91 +94,93 @@ This function ensures any metavariable in the result is either
 1. Delayed assigned with its pending mvar not assigned in any form
 2. Not assigned (delay or not)
  -/
-partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
-  --let padding := String.join $ List.replicate level "│ "
-  --IO.println s!"{padding}Starting {toString eOrig}"
-  let mut result ← Meta.transform (← instantiateMVars eOrig)
-    (pre := fun e => e.withApp fun f args => do
-      let .mvar mvarId := f | return .continue
-      --IO.println s!"{padding}├V {e}"
-      let mvarDecl ← mvarId.getDecl
+partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
+  withTraceNode `Pantograph.Delate (λ _ex => return m!":= {← Meta.ppExpr expr}") do
+  let mut result ← Meta.transform (← instantiateMVars expr)
+    λ e => e.withApp fun f args => do
+    let .mvar mvarId := f | return .continue
+    trace[Pantograph.Delate] "V {e}"
+    let mvarDecl ← mvarId.getDecl
 
-      -- This is critical to maintaining the interdependency of metavariables.
-      -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
-      -- system will not make the necessary delayed assigned mvars in case of
-      -- nested mvars.
-      mvarId.setKind .syntheticOpaque
+    -- This is critical to maintaining the interdependency of metavariables.
+    -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
+    -- system will not make the necessary delayed assigned mvars in case of
+    -- nested mvars.
+    mvarId.setKind .syntheticOpaque
 
-      mvarId.withContext do
-        let lctx ← MonadLCtx.getLCtx
-        if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
-          let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
-            | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
-            | .none => acc) []
-          panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
+    mvarId.withContext do
+      let lctx ← MonadLCtx.getLCtx
+      if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
+        let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
+          | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
+          | .none => acc) []
+        panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
 
-        if let .some assign ← getExprMVarAssignment? mvarId then
-          --IO.println s!"{padding}├A ?{mvarId.name}"
-          assert! !(← mvarId.isDelayedAssigned)
-          return .visit (mkAppN assign args)
-        else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
-          --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
-          --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
+      if let .some assign ← getExprMVarAssignment? mvarId then
+        trace[Pantograph.Delate] "A ?{mvarId.name}"
+        assert! !(← mvarId.isDelayedAssigned)
+        return .visit (mkAppN assign args)
+      else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
+        if ← isTracingEnabledFor `Pantograph.Delate then
+          let substTableStr := ",".intercalate $
+            Array.zipWith (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") fvars args |>.toList
+          trace[Pantograph.Delate]"MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
 
-          if args.size < fvars.size then
-            throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
-          --if !args.isEmpty then
-            --IO.println s!"{padding}├── Arguments Begin"
-          let args ← args.mapM self
-          --if !args.isEmpty then
-            --IO.println s!"{padding}├── Arguments End"
-          if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
-            --IO.println s!"{padding}├T1"
-            let result := mkAppN f args
-            return .done result
-
-          let pending ← mvarIdPending.withContext do
-            let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
-            --IO.println s!"{padding}├Pre: {inner}"
-            pure <| (← inner.abstractM fvars).instantiateRev args
-
-          -- Tail arguments
-          let result := mkAppRange pending fvars.size args.size args
-          --IO.println s!"{padding}├MD {result}"
+        if args.size < fvars.size then
+          throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString expr}"
+        if !args.isEmpty then
+          trace[Pantograph.Delate] "─ Arguments Begin"
+        let args ← args.mapM self
+        if !args.isEmpty then
+          trace[Pantograph.Delate] "─ Arguments End"
+        if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
+          trace[Pantograph.Delate] "T1"
+          let result := mkAppN f args
           return .done result
-        else
-          assert! !(← mvarId.isAssigned)
-          assert! !(← mvarId.isDelayedAssigned)
-          --if !args.isEmpty then
-          --  IO.println s!"{padding}├── Arguments Begin"
-          let args ← args.mapM self
-          --if !args.isEmpty then
-          --  IO.println s!"{padding}├── Arguments End"
 
-          --IO.println s!"{padding}├M ?{mvarId.name}"
-          return .done (mkAppN f args))
-  --IO.println s!"{padding}└Result {result}"
+        let pending ← mvarIdPending.withContext do
+          let inner ← instantiateDelayedMVars (.mvar mvarIdPending)
+          trace[Pantograph.Delate] "Pre: {inner}"
+          pure <| (← inner.abstractM fvars).instantiateRev args
+
+        -- Tail arguments
+        let result := mkAppRange pending fvars.size args.size args
+        trace[Pantograph.Delate] "MD {result}"
+        return .done result
+      else
+        assert! !(← mvarId.isAssigned)
+        assert! !(← mvarId.isDelayedAssigned)
+        if !args.isEmpty then
+          trace[Pantograph.Delate] "─ Arguments Begin"
+        let args ← args.mapM self
+        if !args.isEmpty then
+          trace[Pantograph.Delate] "─ Arguments End"
+
+        trace[Pantograph.Delate] "M ?{mvarId.name}"
+        return .done (mkAppN f args)
+  trace[Pantoraph.Delate] "Result {result}"
   return result
   where
-  self e := instantiateDelayedMVars e --(level := level + 1)
+  self e := instantiateDelayedMVars e
 
 /--
 Convert an expression to an equiavlent form with
 1. No nested delayed assigned mvars
-2. No aux lemmas
+2. No aux lemmas or matchers
 3. No assigned mvars
  -/
 @[export pantograph_instantiate_all_m]
-def instantiateAll (e: Expr): MetaM Expr := do
+def instantiateAll (e : Expr) : MetaM Expr := do
   let e ← instantiateDelayedMVars e
   let e ← unfoldAuxLemmas e
+  let e ← unfoldMatchers e
   return e
 
 structure DelayedMVarInvocation where
-  mvarIdPending: MVarId
-  args: Array (FVarId × (Option Expr))
+  mvarIdPending : MVarId
+  args : Array (FVarId × (Option Expr))
   -- Extra arguments applied to the result of this substitution
-  tail: Array Expr
+  tail : Array Expr
 
 -- The pending mvar of any delayed assigned mvar must not be assigned in any way.
 @[export pantograph_to_delayed_mvar_invocation_m]
@@ -264,38 +307,36 @@ 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) (sanitize: Bool): String :=
+partial def serializeSortLevel (level: Level) : 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 sanitize
-      let w := serializeSortLevel w sanitize
+      let v := serializeSortLevel v
+      let w := serializeSortLevel w
       s!"(:max {v} {w})"
     | .imax v w =>
-      let v := serializeSortLevel v sanitize
-      let w := serializeSortLevel w sanitize
+      let v := serializeSortLevel v
+      let w := serializeSortLevel w
       s!"(:imax {v} {w})"
     | .param name =>
-      let name := serializeName name sanitize
       s!"{name}"
     | .mvar id =>
-      let name := serializeName id.name sanitize
+      let name := id.name
       s!"(:mv {name})"
   match k, u with
   | 0, _ => u_str
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
 
-
 /--
  Completely serializes an expression tree. Json not used due to compactness
 
 A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 -/
-partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
+partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
   self expr
   where
   delayedMVarToSexp (e: Expr): MetaM (Option String) := do
@@ -334,9 +375,10 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
         let name := mvarId.name
         pure s!"(:{pref} {name})"
     | .sort level =>
-      let level := serializeSortLevel level sanitize
+      let level := serializeSortLevel level
       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})"
@@ -369,24 +411,29 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       -- is wrapped in a :lit sexp.
       let v' := match v with
         | .natVal val => toString val
-        | .strVal val => s!"\"{val}\""
+        | .strVal val => IR.EmitC.quoteString val
       pure s!"(:lit {v'})"
     | .mdata _ inner =>
       -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
       -- It may become necessary to incorporate the metadata.
       self inner
-    | .proj _ _ _ => do
+    | .proj typeName idx inner => do
       let env ← getEnv
-      let projApp := exprProjToApp env e
-      let autos := String.intercalate " " (List.replicate projApp.numParams "_")
-      let inner ← self projApp.inner
-      pure s!"((:c {projApp.projector}) {autos} {inner})"
+      match analyzeProjection env e with
+      | .field projector numParams =>
+        let autos := String.intercalate " " (List.replicate numParams "_")
+        let inner' ← self inner
+        pure s!"((:c {projector}) {autos} {inner'})"
+      | .singular _ _ _ =>
+        let typeName' := serializeName typeName (sanitize := false)
+        let e' ← self e
+        pure s!"(:proj {typeName'} {idx} {e'})"
   -- Elides all unhygenic names
   binderInfoSexp : Lean.BinderInfo → String
     | .default => ""
-    | .implicit => " :implicit"
-    | .strictImplicit => " :strictImplicit"
-    | .instImplicit => " :instImplicit"
+    | .implicit => " :i"
+    | .strictImplicit => " :si"
+    | .instImplicit => " :ii"
 
 def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
   let pp?: Option String ← match options.printExprPretty with
@@ -532,7 +579,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 (sanitize := false)
+          let sexp ← serializeExpressionSexp type
           pure <| " " ++ sexp
         else
           pure ""
@@ -558,4 +605,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
       | other => s!"[{other}]"
     parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
 
+initialize
+  registerTraceClass `Pantograph.Delate
+
 end Pantograph

Pantograph/Elab.lean

@@ -6,7 +6,8 @@ namespace Pantograph
 -- Functions for creating contexts and states
 @[export pantograph_default_elab_context]
 def defaultElabContext: Elab.Term.Context := {
-    errToSorry := false
+    declName? := .some `mystery,
+    errToSorry := false,
   }
 
 /-- Read syntax object from string -/

Pantograph/Environment.lean

@@ -24,8 +24,11 @@ def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[
 
 @[export pantograph_environment_module_of_name]
 def module_of_name (env: Environment) (name: Name): Option Name := do
-  let moduleId ←  env.getModuleIdxFor? name
-  return env.allImportedModuleNames.get! moduleId.toNat
+  let moduleId ← env.getModuleIdxFor? name
+  if h : moduleId.toNat < env.allImportedModuleNames.size then
+    return env.allImportedModuleNames[moduleId.toNat]
+  else
+    .none
 
 def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
   let pref := match info with
@@ -43,6 +46,22 @@ def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
   if isNameInternal n || info.isUnsafe
   then Option.none
   else Option.some <| toCompactSymbolName n info
+def describe (_: Protocol.EnvDescribe): CoreM Protocol.EnvDescribeResult := do
+  let env ← Lean.MonadEnv.getEnv
+  return {
+    imports := env.header.imports.map toString,
+    modules := env.header.moduleNames.map (·.toString),
+  }
+def moduleRead (args: Protocol.EnvModuleRead): CoreM Protocol.EnvModuleReadResult := do
+  let env ← Lean.MonadEnv.getEnv
+  let .some i := env.header.moduleNames.findIdx? (· == args.module.toName) |
+    throwError s!"Module not found {args.module}"
+  let data := env.header.moduleData[i]!
+  return {
+    imports := data.imports.map toString,
+    constNames := data.constNames.map (·.toString),
+    extraConstNames := data.extraConstNames.map (·.toString),
+  }
 def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
   let env ← Lean.MonadEnv.getEnv
   let names := env.constants.fold (init := #[]) (λ acc name info =>
@@ -50,15 +69,13 @@ def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
     | .some x => acc.push x
     | .none => acc)
   return { symbols := names }
-def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
+def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.FallibleT CoreM Protocol.EnvInspectResult := do
   let env ← Lean.MonadEnv.getEnv
   let name :=  args.name.toName
   let info? := env.find? name
-  let info ← match info? with
-    | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
-    | some info => pure info
+  let .some info := info? | Protocol.throw $ Protocol.errorIndex s!"Symbol not found {args.name}"
   let module? := env.getModuleIdxFor? name >>=
-    (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
+    (λ idx => env.allImportedModuleNames[idx.toNat]?)
   let value? := match args.value?, info with
     | .some true, _ => info.value?
     | .some false, _ => .none
@@ -72,7 +89,6 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     isUnsafe := info.isUnsafe,
     value? := ← value?.mapM (λ v => serializeExpression options v |>.run'),
     publicName? := Lean.privateToUserName? name |>.map (·.toString),
-    -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
     typeDependency? := if args.dependency?.getD false
       then .some <| type.getUsedConstants.map (λ n => serializeName n)
       else .none,
@@ -80,7 +96,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?
+    module? := module?.map (·.toString)
   }
   let result ← match info with
     | .inductInfo induct => pure { core with inductInfo? := .some {
@@ -113,44 +129,70 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           k := r.k,
       } }
     | _ => pure core
-  return .ok result
-def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
+  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 result
+/-- Elaborates and adds a declaration to the `CoreM` environment. -/
+@[export pantograph_env_add_m]
+def addDecl (name: String) (levels: Array String := #[]) (type?: Option String) (value: String) (isTheorem: Bool)
+    : Protocol.FallibleT CoreM Protocol.EnvAddResult := do
   let env ← Lean.MonadEnv.getEnv
-  let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
-    let type ← match parseTerm env args.type with
-      | .ok syn => do
-        match ← elabTerm syn with
-        | .error e => return .error e
-        | .ok expr => pure expr
+  let levelParams := levels.toList.map (·.toName)
+  let tvM: Elab.TermElabM (Except String (Expr × Expr)) :=
+    Elab.Term.withLevelNames levelParams do do
+    let expectedType?? : Except String (Option Expr) ← ExceptT.run $ type?.mapM λ type => do
+      match parseTerm env type with
+      | .ok syn => elabTerm syn
+      | .error e => MonadExceptOf.throw e
+    let expectedType? ← match expectedType?? with
+      | .ok t? => pure t?
       | .error e => return .error e
-    let value ← match parseTerm env args.value with
+    let value ← match parseTerm env value with
       | .ok syn => do
         try
-          let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
+          let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := expectedType?)
           Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
           let expr ← instantiateMVars expr
           pure $ expr
         catch ex => return .error (← ex.toMessageData.toString)
       | .error e => return .error e
-    pure $ .ok (type, value)
+    Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    let type ← match expectedType? with
+      | .some t => pure t
+      | .none => Meta.inferType value
+    pure $ .ok (← instantiateMVars type, ← instantiateMVars value)
   let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
     | .ok t => pure t
-    | .error e => return .error $ Protocol.errorExpr e
-  let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
-    (name := args.name.toName)
-    (levelParams := [])
-    (type := type)
-    (value := value)
-    (hints := Lean.mkReducibilityHintsRegularEx 1)
-    (safety := Lean.DefinitionSafety.safe)
-    (all := [])
-  let env' ← match env.addDecl (← getOptions) constant with
-    | .error e => do
-      let options ← Lean.MonadOptions.getOptions
-      let desc ← (e.toMessageData options).toString
-      return .error $ { error := "kernel", desc }
-    | .ok env' => pure env'
-  Lean.MonadEnv.modifyEnv (λ _ => env')
-  return .ok {}
+    | .error e => Protocol.throw $ Protocol.errorExpr e
+  let decl := if isTheorem then
+    Lean.Declaration.thmDecl <| Lean.mkTheoremValEx
+      (name := name.toName)
+      (levelParams := levelParams)
+      (type := type)
+      (value := value)
+      (all := [])
+  else
+    Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
+      (name := name.toName)
+      (levelParams := levelParams)
+      (type := type)
+      (value := value)
+      (hints := Lean.mkReducibilityHintsRegularEx 1)
+      (safety := Lean.DefinitionSafety.safe)
+      (all := [])
+  Lean.addDecl decl
+  return {}
 
 end Pantograph.Environment

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,9 +30,17 @@ 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
+  scope : Elab.Command.Scope
   fileName : String
   fileMap : FileMap
   src : Substring
@@ -60,14 +68,14 @@ 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
   let msgs := s'.messages.toList.drop s.messages.toList.length
   let trees := s'.infoState.trees.drop s.infoState.trees.size
   let ⟨_, fileName, fileMap⟩  := (← read).inputCtx
-  return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
+  return ({ scope := s.scopes.head!, fileName, fileMap, src, stx, before, after, msgs, trees }, done)
 
 partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
   let (cmd, done) ← processOneCommand

Pantograph/Frontend/Elab.lean

@@ -1,87 +1,21 @@
-/- 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
@@ -131,19 +65,10 @@ 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 := findAllInfo t none fun i => match i with
+  let infos := t.findAllInfo none false fun i => match i with
     | .ofTacticInfo _ => true
     | _ => false
   infos.filterMap fun p => match p with
@@ -155,16 +80,18 @@ 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.bind λ tree => tree.filter λ
+  let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ
     | info@(.ofTacticInfo _) => info.isOriginal
     | _ => false
-  let tactics := tacticInfoTrees.bind collectTactics
+  let tactics := tacticInfoTrees.flatMap 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 {} do
-      let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
-      return t.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 usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
     return {
       goalBefore,
@@ -177,47 +104,96 @@ structure InfoWithContext where
   info: Elab.Info
   context?: Option Elab.ContextInfo := .none
 
-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
+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
     | .ofTacticInfo { stx, goalsBefore, .. } =>
       -- The `sorry` term is distinct from the `sorry` tactic
       let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry
-      isSorry ∧ !goalsBefore.isEmpty
-    | _ => false
-  infos.map fun (info, context?, _) => { info, context? }
+      return (isSorry ∧ !goalsBefore.isEmpty, ¬ isSorry)
+    | _ => return (false, true)
+  return infos.map fun (info, context?, _) => { info, context? }
 
 -- NOTE: Plural deliberately not spelled "sorries"
 @[export pantograph_frontend_collect_sorrys_m]
-def collectSorrys (step: CompilationStep) : List InfoWithContext :=
-  step.trees.bind collectSorrysInTree
-
+def collectSorrys (step: CompilationStep) (options : GoalCollectionOptions := {})
+    : IO (List InfoWithContext) := do
+  return (← step.trees.mapM $ λ tree => collectSorrysInTree tree options).flatten
 
+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`.
+
+WARNING: Behaviour is unstable when there are multiple `sorry`s. Consider using
+the draft tactic instead.
 -/
-@[export pantograph_frontend_sorrys_to_goal_state]
-def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
+@[export pantograph_frontend_sorrys_to_goal_state_m]
+def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
+  let env := sorrys.head? >>= (·.context?) |>.map (·.env) |>.getD (← getEnv)
   assert! !sorrys.isEmpty
-  let goalsM := sorrys.mapM λ i => do
-    match i.info with
-    | .ofTermInfo termInfo  => do
-      let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
-      return [mvarId]
-    | .ofTacticInfo tacticInfo => do
-      MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
-    | _ => panic! "Invalid info"
-  let goals := List.join (← goalsM.run {} |>.run' {})
-  let root := match goals with
-    | [] => panic! "No MVars generated"
-    | [g] => g
-    | _ => { name := .anonymous }
-  GoalState.createFromMVars goals root
+  withEnv env do
+    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)]
+      | .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)
+      | _ => panic! "Invalid info"
+    let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
+    let goals := annotatedGoals.map Prod.fst
+    let srcBoundaries := annotatedGoals.map Prod.snd
+    let root := match goals with
+      | [] => panic! "No MVars generated"
+      | [g] => g
+      | _ => { name := .anonymous }
+    let state ← GoalState.createFromMVars goals root
+    return { state, srcBoundaries }
 
 
+@[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

@@ -0,0 +1,157 @@
+/- 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
+  | .ofChoiceInfo         info => info.stx
+  | .ofPartialTermInfo    info => info.stx
+  | .ofDelabTermInfo      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]"
+      | .ofChoiceInfo _ => pure "[choice]"
+      | .ofPartialTermInfo  _ => pure "[partial_term]"
+      | .ofDelabTermInfo _ => pure "[delab_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

@@ -62,13 +62,14 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
   let sourceMCtx ← getSourceMCtx
   -- We want to create as few mvars as possible
   let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr
-  --IO.println s!"Transform src: {srcExpr}"
+  trace[Pantograph.Frontend.MetaTranslate] "Transform src: {srcExpr}"
   let result ← Core.transform srcExpr λ e => do
     let state ← get
     match e with
     | .fvar fvarId =>
       let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
-      assert! (← getLCtx).contains fvarId'
+      -- Delegating this to `Meta.check` later
+      --assert! (← getLCtx).contains fvarId'
       return .done $ .fvar fvarId'
     | .mvar mvarId => do
       -- Must not be assigned
@@ -99,10 +100,10 @@ partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalD
   addTranslatedFVar srcLocalDecl.fvarId fvarId
   match srcLocalDecl with
   | .cdecl index _ userName type bi kind => do
-    --IO.println s!"[CD] {userName} {toString type}"
+    trace[Pantograph.Frontend.MetaTranslate] "[CD] {userName} {toString type}"
     return .cdecl index fvarId userName (← translateExpr type) bi kind
   | .ldecl index _ userName type value nonDep kind => do
-    --IO.println s!"[LD] {toString type} := {toString value}"
+    trace[Pantograph.Frontend.MetaTranslate] "[LD] {toString type} := {toString value}"
     return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind
 
 partial def translateLCtx : MetaTranslateM LocalContext := do
@@ -161,4 +162,7 @@ end MetaTranslate
 
 export MetaTranslate (MetaTranslateM)
 
+initialize
+  registerTraceClass `Pantograph.Frontend.MetaTranslate
+
 end Pantograph.Frontend

Pantograph/Goal.lean

@@ -10,8 +10,6 @@ import Lean
 namespace Pantograph
 open Lean
 
-def filename: String := "<pantograph>"
-
 /--
 Represents an interconnected set of metavariables, or a state in proof search
  -/
@@ -73,28 +71,38 @@ 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
+protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
   mvarId.withContext m |>.run' (← read) state.metaState
-
+protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α :=
+  Meta.mapMetaM <| state.withContext' mvarId
 protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
-  Meta.mapMetaM <| state.withContext state.parentMVar?.get!
+  Meta.mapMetaM <| state.withContext' state.parentMVar?.get!
 protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
-  Meta.mapMetaM <| state.withContext state.root
+  Meta.mapMetaM <| state.withContext' state.root
 
 private def GoalState.mvars (state: GoalState): SSet MVarId :=
   state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
-protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
+-- Restore the name generator and macro scopes of the core state
+protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := do
+  let savedCore := state.coreState
+  modifyGetThe Core.State (fun st => ((),
+    { st with nextMacroScope := savedCore.nextMacroScope, ngen := savedCore.ngen }))
+protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := do
+  state.restoreCoreMExtra
   state.savedState.term.meta.restore
-protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
+protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := do
+  state.restoreCoreMExtra
   state.savedState.term.restore
 private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
-  state.savedState.restore
+  state.restoreElabM
   Elab.Tactic.setGoals [goal]
 
 @[export pantograph_goal_state_focus]
 protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
-  let goal ← state.savedState.tactic.goals.get? goalId
+  let goal ← state.savedState.tactic.goals[goalId]?
   return {
     state with
     savedState := {
@@ -177,16 +185,52 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI
 
 --- Tactic execution functions ---
 
-protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
+-- 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)
   : Elab.TermElabM GoalState := do
   unless (← getMCtx).decls.contains goal do
     throwError s!"Goal is not in context: {goal.name}"
   goal.checkNotAssigned `GoalState.step
-  let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
+  let (_, { goals }) ← 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 := newGoals },
+    savedState := { term := nextElabState, tactic := { goals }, },
     parentMVar? := .some goal,
     calcPrevRhs? := .none,
   }
@@ -202,16 +246,37 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message: String)
 
-/-- 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
+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
   try
-    let nextState ← state.step goal tacticM
+    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
     return .success nextState
   catch exception =>
-    return .failure #[← exception.toMessageData.toString]
+    match exception with
+    | .internal _ => return .failure $ ← dumpMessageLog prevMessageLength
+    | _ => 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
@@ -219,10 +284,11 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
     (env := ← MonadEnv.getEnv)
     (catName := if state.isConv then `conv else `tactic)
     (input := tactic)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  state.tryTacticM goal $ Elab.Tactic.evalTactic tactic
+  assert! ¬ (← goal.isAssigned)
+  state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true
 
 protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
       Elab.TermElabM TacticResult := do
@@ -231,7 +297,7 @@ protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: Strin
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := expr)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.tryTacticM goal $ Tactic.evalAssign expr
@@ -245,7 +311,7 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := type)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.tryTacticM goal $ Tactic.evalLet binderName.toName type
@@ -332,7 +398,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
     (env := state.env)
     (catName := `term)
     (input := pred)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   goal.checkNotAssigned `GoalState.tryCalc
@@ -353,7 +419,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

@@ -3,6 +3,7 @@ import Pantograph.Goal
 import Pantograph.Protocol
 import Pantograph.Delate
 import Pantograph.Version
+
 import Lean
 
 namespace Lean
@@ -40,8 +41,6 @@ namespace Pantograph
 
 def runMetaM { α } (metaM: MetaM α): CoreM α :=
   metaM.run'
-def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
-  termElabM.run' (ctx := defaultElabContext) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
 
@@ -75,130 +74,110 @@ def createCoreState (imports: Array String): IO Core.State := do
     (trustLevel := 1)
   return { env := env }
 
-@[export pantograph_env_add_m]
-def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
-    CoreM (Protocol.CR Protocol.EnvAddResult) :=
-  Environment.addDecl { name, type, value, isTheorem }
-
 @[export pantograph_parse_elab_type_m]
-def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
+def parseElabType (type: String): Protocol.FallibleT Elab.TermElabM Expr := do
   let env ← MonadEnv.getEnv
   let syn ← match parseTerm env type with
-    | .error str => return .error $ errorI "parsing" str
+    | .error str => Protocol.throw $ errorI "parsing" str
     | .ok syn => pure syn
   match ← elabType syn with
-  | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok (← instantiateMVars expr)
+  | .error str => Protocol.throw $ errorI "elab" str
+  | .ok expr => return (← instantiateMVars expr)
 
 /-- This must be a TermElabM since the parsed expr contains extra information -/
 @[export pantograph_parse_elab_expr_m]
-def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
+def parseElabExpr (expr: String) (expectedType?: Option String := .none): Protocol.FallibleT Elab.TermElabM Expr := do
   let env ← MonadEnv.getEnv
-  let expectedType? ← match ← expectedType?.mapM parseElabType with
-    | .none => pure $ .none
-    | .some (.ok t) => pure $ .some t
-    | .some (.error e) => return .error e
+  let expectedType? ← expectedType?.mapM parseElabType
   let syn ← match parseTerm env expr with
-    | .error str => return .error $ errorI "parsing" str
+    | .error str => Protocol.throw $ errorI "parsing" str
     | .ok syn => pure syn
   match ← elabTerm syn expectedType? with
-  | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok (← instantiateMVars expr)
+  | .error str => Protocol.throw $ errorI "elab" str
+  | .ok expr => return (← instantiateMVars expr)
 
 @[export pantograph_expr_echo_m]
-def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[])  (options: @&Protocol.Options := {}):
-    CoreM (Protocol.CR Protocol.ExprEchoResult) :=
-  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
-    let expr ← match ← parseElabExpr expr expectedType? with
-      | .error e => return .error e
-      | .ok expr => pure expr
-    try
-      let type ← unfoldAuxLemmas (← Meta.inferType expr)
-      return .ok {
-          type := (← serializeExpression options type),
-          expr := (← serializeExpression options expr)
-      }
-    catch exception =>
-      return .error $ errorI "typing" (← exception.toMessageData.toString)
+def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options := {}):
+    Protocol.FallibleT Elab.TermElabM Protocol.ExprEchoResult := do
+  let expr ← parseElabExpr expr expectedType?
+  try
+    let type ← unfoldAuxLemmas (← Meta.inferType expr)
+    return {
+        type := (← serializeExpression options type),
+        expr := (← serializeExpression options expr),
+    }
+  catch exception =>
+    Protocol.throw $ errorI "typing" (← exception.toMessageData.toString)
 
 @[export pantograph_goal_start_expr_m]
-def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR GoalState) :=
-  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
-    let expr ← match ← parseElabType expr with
-      | .error e => return .error e
-      | .ok expr => pure $ expr
-    return .ok $ ← GoalState.create expr
-
-@[export pantograph_goal_resume]
-def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
-  target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
+def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState := do
+  let t ← parseElabType expr
+  GoalState.create t
 
 @[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
   runMetaM <| state.serializeGoals (parent := .none) options
 
 @[export pantograph_goal_print_m]
-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)),
-    }
+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,
+  }
 
-@[export pantograph_goal_tactic_m]
-def goalTactic (state: GoalState) (goal:  MVarId) (tactic: String): CoreM TacticResult :=
-  runTermElabM <| state.tryTactic goal tactic
-@[export pantograph_goal_assign_m]
-def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult :=
-  runTermElabM <| state.tryAssign goal expr
 @[export pantograph_goal_have_m]
-protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do
+protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
   let type ← match (← parseTermM type) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  runTermElabM do
-    state.restoreElabM
-    state.tryTacticM goal $ Tactic.evalHave binderName.toName type
+  state.restoreElabM
+  state.tryTacticM goal $ Tactic.evalHave binderName.toName type
 @[export pantograph_goal_try_define_m]
-protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do
+protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): Elab.TermElabM 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.evalDefine binderName.toName expr)
-@[export pantograph_goal_try_motivated_apply_m]
-protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
-      Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let recursor ← match (← parseTermM recursor) with
+  state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
+@[export pantograph_goal_try_draft_m]
+protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): Elab.TermElabM TacticResult := do
+  let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
-@[export pantograph_goal_try_no_confuse_m]
-protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
-      Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let eq ← match (← parseTermM eq) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
-@[export pantograph_goal_let_m]
-def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
-  runTermElabM <| state.tryLet goal binderName type
-@[export pantograph_goal_conv_m]
-def goalConv (state: GoalState) (goal: MVarId): CoreM TacticResult :=
-  runTermElabM <| state.conv goal
-@[export pantograph_goal_conv_exit_m]
-def goalConvExit (state: GoalState): CoreM TacticResult :=
-  runTermElabM <| state.convExit
-@[export pantograph_goal_calc_m]
-def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResult :=
-  runTermElabM <| state.tryCalc goal pred
+  state.tryTacticM goal (Tactic.evalDraft expr)
+
+-- Cancel the token after a timeout.
+@[export pantograph_run_cancel_token_with_timeout_m]
+def runCancelTokenWithTimeout (cancelToken : IO.CancelToken) (timeout : UInt32) : IO Unit := do
+  let _ ← EIO.asTask do
+    IO.sleep timeout
+    cancelToken.set
+  return ()
 
 end Pantograph

Pantograph/Protocol.lean

@@ -5,6 +5,7 @@ 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
 
@@ -29,6 +30,8 @@ structure Options where
   printImplementationDetailHyps: Bool := false
   -- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption
   automaticMode: Bool := true
+  -- Timeout for tactics and operations that could potentially execute a tactic
+  timeout: Nat := 0
   deriving Lean.ToJson
 
 abbrev OptionsT := ReaderT Options
@@ -102,15 +105,33 @@ structure StatResult where
 -- Return the type of an expression
 structure ExprEcho where
   expr: String
-  type?: Option String
+  type?: Option String := .none
   -- universe levels
-  levels: Option (Array String) := .none
+  levels?: Option (Array String) := .none
   deriving Lean.FromJson
 structure ExprEchoResult where
   expr: Expression
   type: Expression
   deriving Lean.ToJson
 
+-- Describe the current state of the environment
+structure EnvDescribe where
+  deriving Lean.FromJson
+structure EnvDescribeResult where
+  imports : Array String
+  modules : Array String
+  deriving Lean.ToJson
+
+-- Describe a module
+structure EnvModuleRead where
+  module : String
+  deriving Lean.FromJson
+structure EnvModuleReadResult where
+  imports: Array String
+  constNames: Array String
+  extraConstNames: Array String
+  deriving Lean.ToJson
+
 -- Print all symbols in environment
 structure EnvCatalog where
   deriving Lean.FromJson
@@ -121,11 +142,13 @@ structure EnvCatalogResult where
 -- Print the type of a symbol
 structure EnvInspect where
   name: String
-  -- If true/false, show/hide the value expressions; By default definitions
-  -- values are shown and theorem values are hidden.
+  -- Show the value expressions; By default definitions values are shown and
+  -- theorem values are hidden.
   value?: Option Bool := .some false
-  -- If true, show the type and value dependencies
+  -- 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
@@ -172,13 +195,19 @@ 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
   name: String
-  type: String
+  levels?: Option (Array String) := .none
+  type?: Option String := .none
   value: String
-  isTheorem: Bool
+  isTheorem: Bool := false
   deriving Lean.FromJson
 structure EnvAddResult where
   deriving Lean.ToJson
@@ -191,14 +220,15 @@ structure EnvSaveLoadResult where
 
 /-- Set options; See `Options` struct above for meanings -/
 structure OptionsSet where
-  printJsonPretty?: Option Bool
-  printExprPretty?: Option Bool
-  printExprAST?: Option Bool
-  printDependentMVars?: Option Bool
-  noRepeat?: Option Bool
-  printAuxDecls?: Option Bool
-  printImplementationDetailHyps?: Option Bool
-  automaticMode?: Option Bool
+  printJsonPretty?: Option Bool := .none
+  printExprPretty?: Option Bool := .none
+  printExprAST?: Option Bool := .none
+  printDependentMVars?: Option Bool := .none
+  noRepeat?: Option Bool := .none
+  printAuxDecls?: Option Bool := .none
+  printImplementationDetailHyps?: Option Bool := .none
+  automaticMode?: Option Bool := .none
+  timeout?: Option Nat := .none
   deriving Lean.FromJson
 structure OptionsSetResult where
   deriving Lean.ToJson
@@ -209,8 +239,8 @@ structure GoalStart where
   -- Only one of the fields below may be populated.
   expr: Option String     -- Directly parse in an expression
   -- universe levels
-  levels: Option (Array String) := .none
-  copyFrom: Option String -- Copy the type from a theorem in the environment
+  levels?: Option (Array String) := .none
+  copyFrom: Option String := .none -- Copy the type from a theorem in the environment
   deriving Lean.FromJson
 structure GoalStartResult where
   stateId: Nat := 0
@@ -229,6 +259,7 @@ 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
@@ -271,12 +302,23 @@ 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
+  parent?: Option Expression := .none
+  goals: Array Goal := #[]
+  extraMVars: Array Expression := #[]
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL
@@ -308,10 +350,18 @@ 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
-  -- If set to true, collect tactic invocations
+  -- Whether to read the header
+  readHeader : Bool := false
+  -- Alter the REPL environment after the compilation units.
+  inheritEnv : Bool := false
+  -- collect tactic invocations
   invocations: Bool := false
-  -- If set to true, collect `sorry`s
+  -- 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
@@ -325,16 +375,24 @@ structure InvokedTactic where
 structure CompilationUnit where
   -- String boundaries of compilation units
   boundary: (Nat × Nat)
+  messages: Array String := #[]
   -- Tactic invocations
   invocations?: Option (List InvokedTactic) := .none
   goalStateId?: Option Nat := .none
-  goals: Array Goal := #[]
-  messages: Array String := #[]
+  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
   deriving Lean.ToJson
 structure FrontendProcessResult where
   units: List CompilationUnit
   deriving Lean.ToJson
 
-abbrev CR α := Except InteractionError α
+abbrev FallibleT := ExceptT InteractionError
+
+abbrev throw {m : Type v → Type w} [MonadExceptOf InteractionError m] {α : Type v} (e : InteractionError) : m α :=
+  throwThe InteractionError e
 
 end Pantograph.Protocol

Pantograph/Serial.lean

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

Pantograph/Tactic.lean

@@ -1,5 +1,2 @@
 import Pantograph.Tactic.Assign
-import Pantograph.Tactic.Congruence
-import Pantograph.Tactic.MotivatedApply
-import Pantograph.Tactic.NoConfuse
 import Pantograph.Tactic.Prograde

Pantograph/Tactic/Assign.lean

@@ -27,5 +27,39 @@ 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 λ expr =>
+    if expr.isSorry then do
+      let type ← instantiateMVars (expr.getArg! 0 |>.bindingBody!)
+      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
+    else
+      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/Congruence.lean

@@ -1,98 +0,0 @@
-import Lean
-
-open Lean
-
-namespace Pantograph.Tactic
-
-def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
-  mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg
-  let target ← mvarId.getType
-  let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
-  let userName := (← mvarId.getDecl).userName
-
-  let u ← Meta.mkFreshLevelMVar
-  let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
-    (tag := userName ++ `α)
-  let f ← Meta.mkFreshExprSyntheticOpaqueMVar (.forallE .anonymous α β .default)
-    (tag := userName ++ `f)
-  let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
-    (tag := userName ++ `a₁)
-  let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
-    (tag := userName ++ `a₂)
-  let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
-    (tag := userName ++ `h)
-  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target
-  let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
-    (tag := userName ++ `conduit)
-  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
-  let result := [α, a₁, a₂, f,  h, conduit]
-  return result.map (·.mvarId!)
-
-def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
-  let goal ← Elab.Tactic.getMainGoal
-  let nextGoals ← congruenceArg goal
-  Elab.Tactic.replaceMainGoal nextGoals
-
-def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
-  mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
-  let target ← mvarId.getType
-  let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
-  let userName := (← mvarId.getDecl).userName
-  let u ← Meta.mkFreshLevelMVar
-  let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
-    (tag := userName ++ `α)
-  let fType := .forallE .anonymous α β .default
-  let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
-    (tag := userName ++ `f₁)
-  let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
-    (tag := userName ++ `f₂)
-  let a ← Meta.mkFreshExprSyntheticOpaqueMVar α
-    (tag := userName ++ `a)
-  let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂)
-    (tag := userName ++ `h)
-  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target
-  let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
-    (tag := userName ++ `conduit)
-  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
-  let result := [α, f₁, f₂, h, a, conduit]
-  return result.map (·.mvarId!)
-
-def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
-  let goal ← Elab.Tactic.getMainGoal
-  let nextGoals ← congruenceFun goal
-  Elab.Tactic.replaceMainGoal nextGoals
-
-def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
-  mvarId.checkNotAssigned `Pantograph.Tactic.congruence
-  let target ← mvarId.getType
-  let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
-  let userName := (← mvarId.getDecl).userName
-  let u ← Meta.mkFreshLevelMVar
-  let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
-    (tag := userName ++ `α)
-  let fType := .forallE .anonymous α β .default
-  let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
-    (tag := userName ++ `f₁)
-  let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
-    (tag := userName ++ `f₂)
-  let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
-    (tag := userName ++ `a₁)
-  let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
-    (tag := userName ++ `a₂)
-  let h₁ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂)
-    (tag := userName ++ `h₁)
-  let h₂ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
-    (tag := userName ++ `h₂)
-  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target
-  let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
-    (tag := userName ++ `conduit)
-  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
-  let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
-  return result.map (·.mvarId!)
-
-def evalCongruence: Elab.Tactic.TacticM Unit := do
-  let goal ← Elab.Tactic.getMainGoal
-  let nextGoals ← congruence goal
-  Elab.Tactic.replaceMainGoal nextGoals
-
-end Pantograph.Tactic

Pantograph/Tactic/MotivatedApply.lean

@@ -1,106 +0,0 @@
-import Lean
-
-open Lean
-
-namespace Pantograph.Tactic
-
-def getForallArgsBody: Expr → List Expr × Expr
-  | .forallE _ d b _ =>
-    let (innerArgs, innerBody) := getForallArgsBody b
-    (d :: innerArgs, innerBody)
-  | e => ([], e)
-
-def replaceForallBody: Expr → Expr → Expr
-  | .forallE param domain body binderInfo, target =>
-    let body := replaceForallBody body target
-    .forallE param domain body binderInfo
-  | _, target => target
-
-structure RecursorWithMotive where
-  args: List Expr
-  body: Expr
-
-  -- .bvar index for the motive and major from the body
-  iMotive: Nat
-
-namespace RecursorWithMotive
-
-protected def nArgs (info: RecursorWithMotive): Nat := info.args.length
-
-protected def getMotiveType (info: RecursorWithMotive): Expr :=
-  let level := info.nArgs - info.iMotive - 1
-  let a := info.args.get! level
-  a
-
-protected def surrogateMotiveType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
-  let motiveType := Expr.instantiateRev info.getMotiveType mvars
-  let resultantType ← Meta.inferType resultant
-  return replaceForallBody motiveType resultantType
-
-protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
-  let motiveCall := Expr.instantiateRev info.body mvars
-  Meta.mkEq motiveCall resultant
-
-end RecursorWithMotive
-
-def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do
-  let (args, body) := getForallArgsBody recursorType
-  if ¬ body.isApp then
-    .none
-  let iMotive ← match body.getAppFn with
-    | .bvar iMotive => pure iMotive
-    | _ => .none
-  return {
-    args,
-    body,
-    iMotive,
-  }
-
-def collectMotiveArguments (forallBody: Expr): SSet Nat :=
-  match forallBody with
-  | .app (.bvar i) _ => SSet.empty.insert i
-  | _ => SSet.empty
-
-/-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
-def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do
-  mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
-  let recursorType ← Meta.inferType recursor
-  let resultant ← mvarId.getType
-  let tag ← mvarId.getTag
-
-  let info ← match getRecursorInformation recursorType with
-    | .some info => pure info
-    | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}"
-
-  let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
-    if i ≥ info.nArgs then
-      return prev
-    else
-      let argType := info.args.get! i
-      -- If `argType` has motive references, its goal needs to be placed in it
-      let argType := argType.instantiateRev prev
-      let bvarIndex := info.nArgs - i - 1
-      let argGoal ← if bvarIndex = info.iMotive then
-          let surrogateMotiveType ← info.surrogateMotiveType prev resultant
-          Meta.mkFreshExprSyntheticOpaqueMVar surrogateMotiveType (tag := tag ++ `motive)
-        else
-          Meta.mkFreshExprSyntheticOpaqueMVar argType (tag := .anonymous)
-      let prev :=  prev ++ [argGoal]
-      go (i + 1) prev
-    termination_by info.nArgs - i
-  let mut newMVars ← go 0 #[]
-
-  -- Create the conduit type which proves the result of the motive is equal to the goal
-  let conduitType ← info.conduitType newMVars resultant
-  let goalConduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType (tag := `conduit)
-  mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
-  newMVars := newMVars ++ [goalConduit]
-
-  return newMVars.map (λ mvar => { mvarId := mvar.mvarId!})
-
-def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
-  let recursor ← Elab.Term.elabTerm (stx := stx) .none
-  let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
-  Elab.Tactic.replaceMainGoal $ nextGoals.toList.map (·.mvarId)
-
-end Pantograph.Tactic

Pantograph/Tactic/NoConfuse.lean

@@ -1,22 +0,0 @@
-import Lean
-
-open Lean
-
-namespace Pantograph.Tactic
-
-def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do
-  mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse
-  let target ← mvarId.getType
-  let noConfusion ← Meta.mkNoConfusion (target := target) (h := h)
-
-  unless ← Meta.isDefEq (← Meta.inferType noConfusion) target do
-    throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr target}"
-  mvarId.assign noConfusion
-
-def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
-  let goal ← Elab.Tactic.getMainGoal
-  let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
-  noConfuse goal h
-  Elab.Tactic.replaceMainGoal []
-
-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 ←
-    withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
+    Meta.withLCtx 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.19"
+def version := "0.3.0"
 
 end Pantograph

README.md

@@ -7,6 +7,8 @@ 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
@@ -15,7 +17,9 @@ nix build .#{sharedLib,executable}
 ```
 to build either the shared library or executable.
 
-Install `elan` and `lake`, and run
+Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and
+run
+
 ``` sh
 lake build
 ```
@@ -24,9 +28,12 @@ This builds the executable in `.lake/build/bin/pantograph-repl`.
 ## Executable Usage
 
 ``` sh
-pantograph MODULES|LEAN_OPTIONS
+pantograph-repl 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
@@ -37,8 +44,6 @@ 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)
 ```
@@ -75,7 +80,7 @@ the environment might be setup like this:
 
 ``` sh
 LIB="../lib"
-LIB_MATHLIB="$LIB/mathlib4/lake-packages"
+LIB_MATHLIB="$LIB/mathlib4/.lake"
 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

@@ -3,17 +3,30 @@ import Pantograph
 
 namespace Pantograph.Repl
 
+open Lean
+
 structure Context where
-  imports: List String
+  coreContext : Core.Context
 
 /-- Stores state of the REPL -/
 structure State where
-  options: Protocol.Options := {}
-  nextId: Nat := 0
-  goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
+  options : Protocol.Options := {}
+  nextId : Nat := 0
+  goalStates : Std.HashMap Nat GoalState := Std.HashMap.empty
 
-/-- Main state monad for executing commands -/
-abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
+  env : Environment
+  -- Parser state
+  scope : Elab.Command.Scope := { header := "" }
+
+/-- Main monad for executing commands -/
+abbrev MainM := ReaderT Context $ StateRefT State IO
+/-- Main with possible exception -/
+abbrev EMainM := Protocol.FallibleT $ ReaderT Context $ StateRefT State IO
+def getMainState : MainM State := get
+
+instance : MonadEnv MainM where
+  getEnv := return (← get).env
+  modifyEnv f := modify fun s => { s with env := f s.env  }
 
 def newGoalState (goalState: GoalState) : MainM Nat := do
   let state ← get
@@ -24,87 +37,221 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
   }
   return stateId
 
+def runCoreM { α } (coreM : CoreM α) : EMainM α := do
+  let scope := (← get).scope
+  let options :=(← get).options
+  let cancelTk? ← match options.timeout with
+    | 0 => pure .none
+    | _ => .some <$> IO.CancelToken.new
+  let coreCtx : Core.Context := {
+    (← read).coreContext with
+    currNamespace      := scope.currNamespace,
+    openDecls          := scope.openDecls,
+    options            := scope.opts,
+    initHeartbeats     :=  ← IO.getNumHeartbeats,
+    cancelTk?,
+  }
+  let coreState : Core.State := {
+    env := (← get).env
+  }
+  -- Remap the coreM to capture every exception
+  let coreM' : CoreM _ :=
+    try
+      Except.ok <$> coreM
+    catch ex =>
+      let desc ← ex.toMessageData.toString
+      return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError)
+  if let .some token := cancelTk? then
+    runCancelTokenWithTimeout token (timeout := .ofBitVec options.timeout)
+  let (result, state') ← match ← (coreM'.run coreCtx coreState).toIO' with
+    | Except.error (Exception.error _ msg)   => Protocol.throw $ { error := "core", desc := ← msg.toString }
+    | Except.error (Exception.internal id _) => Protocol.throw $ { error := "internal", desc := (← id.getName).toString }
+    | Except.ok a                            => pure a
+  if result matches .ok _ then
+    modifyEnv λ _ => state'.env
+  liftExcept result
 
--- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
--- certain monadic features in `MainM`
-abbrev CR α := Except Protocol.InteractionError α
+def runCoreM' { α } (coreM : Protocol.FallibleT CoreM α) : EMainM α := do
+  liftExcept $ ← runCoreM coreM.run
 
-def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
-  metaM.run'
-def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
-  termElabM.run' (ctx := defaultElabContext) |>.run'
+
+def liftMetaM { α } (metaM : MetaM α): EMainM α :=
+  runCoreM metaM.run'
+def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name := [])
+    : EMainM α := do
+  let scope := (← get).scope
+  let context := {
+    isNoncomputableSection := scope.isNoncomputable,
+  }
+  let state := {
+    levelNames := scope.levelNames ++ levelNames,
+  }
+  runCoreM $ termElabM.run' context state |>.run'
+
+section Frontend
+
+structure CompilationUnit where
+  -- Should be the penultimate environment, but this is ok
+  env : Environment
+  boundary : Nat × Nat
+  invocations : List Protocol.InvokedTactic
+  sorrys : List Frontend.InfoWithContext
+  messages : Array String
+  newConstants : List Name
+
+def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
+  let options := (← getMainState).options
+  let (fileName, file) ← match args.fileName?, args.file? with
+    | .some fileName, .none => do
+      let file ← IO.FS.readFile fileName
+      pure (fileName, file)
+    | .none, .some file =>
+      pure ("<anonymous>", file)
+    | _, _ => Protocol.throw $ errorI "arguments" "Exactly one of {fileName, file} must be supplied"
+  let env?: Option Environment ← if args.readHeader then
+      pure .none
+    else do
+      .some <$> getEnv
+  let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
+  let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) :=
+    Frontend.mapCompilationSteps λ step => do
+    let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
+    let invocations: Option (List Protocol.InvokedTactic) ← if args.invocations then
+        Frontend.collectTacticsFromCompilationStep step
+      else
+        pure []
+    let sorrys ← if args.sorrys then
+        Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals })
+      else
+        pure []
+    let messages ← step.messageStrings
+    let newConstants ← if args.newConstants then
+        Frontend.collectNewDefinedConstants step
+      else
+        pure []
+    return {
+      env := step.before,
+      boundary,
+      invocations,
+      sorrys,
+      messages,
+      newConstants
+    }
+  let (li, state') ← frontendM.run context |>.run state
+  if args.inheritEnv then
+    setEnv state'.commandState.env
+    if let .some scope := state'.commandState.scopes.head? then
+      -- modify the scope
+      set { ← getMainState with scope }
+  let units ← li.mapM λ step => withEnv step.env do
+    let newConstants? := if args.newConstants then
+        .some $ step.newConstants.toArray.map λ name => name.toString
+      else
+        .none
+    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then do
+        pure (.none, .none, .none)
+      else do
+        let ({ state, srcBoundaries }, goals) ← liftMetaM do
+          let result@{state, .. } ← Frontend.sorrysToGoalState step.sorrys
+          let goals ← goalSerialize state options
+          pure (result, goals)
+        let stateId ← newGoalState state
+        let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
+        pure (.some stateId, .some goals, .some srcBoundaries)
+    let invocations? := if args.invocations then .some step.invocations else .none
+    return {
+      boundary := step.boundary,
+      messages := step.messages,
+      invocations?,
+      goalStateId?,
+      goals?,
+      goalSrcBoundaries?,
+      newConstants?,
+    }
+  return { units }
+
+end Frontend
 
 /-- Main loop command of the REPL -/
-def execute (command: Protocol.Command): MainM Lean.Json := do
-  let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
-    match Lean.fromJson? command.payload with
-    | .ok args => do
-      match (← comm args) with
-      | .ok result =>  return Lean.toJson result
-      | .error ierror => return Lean.toJson ierror
-    | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
-  try
-    match command.cmd with
-    | "reset"         => run reset
-    | "stat"          => run stat
-    | "expr.echo"     => run expr_echo
-    | "env.catalog"   => run env_catalog
-    | "env.inspect"   => run env_inspect
-    | "env.add"       => run env_add
-    | "env.save"      => run env_save
-    | "env.load"      => run env_load
-    | "options.set"   => run options_set
-    | "options.print" => run options_print
-    | "goal.start"    => run goal_start
-    | "goal.tactic"   => run goal_tactic
-    | "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 :=
-        errorCommand s!"Unknown command {cmd}"
-      return Lean.toJson error
-  catch ex => do
-    let error ← ex.toMessageData.toString
-    return Lean.toJson $ errorIO error
+def execute (command: Protocol.Command): MainM Json := do
+  let run { α β: Type } [FromJson α] [ToJson β] (comm: α → EMainM β): MainM Json :=
+    try
+      match fromJson? command.payload with
+      | .ok args => do
+        match (← comm args |>.run) with
+        | .ok result =>  return toJson result
+        | .error ierror => return toJson ierror
+      | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}"
+    catch ex : IO.Error =>
+      let error : Protocol.InteractionError := { error := "io", desc := ex.toString }
+      return toJson error
+  match command.cmd with
+  | "reset"         => run reset
+  | "stat"          => run stat
+  | "expr.echo"     => run expr_echo
+  | "env.describe"  => run env_describe
+  | "env.module_read" => run env_module_read
+  | "env.catalog"   => run env_catalog
+  | "env.inspect"   => run env_inspect
+  | "env.add"       => run env_add
+  | "env.save"      => run env_save
+  | "env.load"      => run env_load
+  | "options.set"   => run options_set
+  | "options.print" => run options_print
+  | "goal.start"    => run goal_start
+  | "goal.tactic"   => run goal_tactic
+  | "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 :=
+      errorCommand s!"Unknown command {cmd}"
+    return toJson error
   where
   errorCommand := errorI "command"
   errorIndex := errorI "index"
   errorIO := errorI "io"
   -- Command Functions
-  reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
-    let state ← get
+  reset (_: Protocol.Reset): EMainM Protocol.StatResult := do
+    let state ← getMainState
     let nGoals := state.goalStates.size
     set { state with nextId := 0, goalStates := .empty }
-    return .ok { nGoals }
-  stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
-    let state ← get
+    return { nGoals }
+  stat (_: Protocol.Stat): EMainM Protocol.StatResult := do
+    let state ← getMainState
     let nGoals := state.goalStates.size
-    return .ok { nGoals }
-  env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
-    let result ← Environment.catalog args
-    return .ok result
-  env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
-    let state ← get
-    Environment.inspect args state.options
-  env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
-    Environment.addDecl args
-  env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
-    let env ← Lean.MonadEnv.getEnv
+    return { nGoals }
+  env_describe (args: Protocol.EnvDescribe): EMainM Protocol.EnvDescribeResult := do
+    let result ← runCoreM $ Environment.describe args
+    return result
+  env_module_read (args: Protocol.EnvModuleRead): EMainM Protocol.EnvModuleReadResult := do
+    runCoreM $ Environment.moduleRead args
+  env_catalog (args: Protocol.EnvCatalog): EMainM Protocol.EnvCatalogResult := do
+    let result ← runCoreM $ Environment.catalog args
+    return result
+  env_inspect (args: Protocol.EnvInspect): EMainM Protocol.EnvInspectResult := do
+    let state ← getMainState
+    runCoreM' $ Environment.inspect args state.options
+  env_add (args: Protocol.EnvAdd): EMainM Protocol.EnvAddResult := do
+    runCoreM' $ Environment.addDecl args.name (args.levels?.getD #[]) args.type? args.value args.isTheorem
+  env_save (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
+    let env ← MonadEnv.getEnv
     environmentPickle env args.path
-    return .ok {}
-  env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
+    return {}
+  env_load (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
     let (env, _) ← environmentUnpickle args.path
-    Lean.setEnv env
-    return .ok {}
-  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
-    let state ← get
-    exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
-  options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
-    let state ← get
+    setEnv env
+    return {}
+  expr_echo (args: Protocol.ExprEcho): EMainM Protocol.ExprEchoResult := do
+    let state ← getMainState
+    let levelNames := (args.levels?.getD #[]).toList.map (·.toName)
+    liftExcept $ ← liftTermElabM (levelNames := levelNames) do
+      (exprEcho args.expr (expectedType? := args.type?) (options := state.options)).run
+  options_set (args: Protocol.OptionsSet): EMainM Protocol.OptionsSetResult := do
+    let state ← getMainState
     let options := state.options
     set { state with
       options := {
@@ -117,170 +264,136 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
         printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
         automaticMode := args.automaticMode?.getD options.automaticMode,
+        timeout := args.timeout?.getD options.timeout,
       }
     }
-    return .ok {  }
-  options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
-    return .ok (← get).options
-  goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
-    let env ← Lean.MonadEnv.getEnv
-    let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
-      | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
-      | .none, .some copyFrom =>
-        (match env.find? <| copyFrom.toName with
+    return {  }
+  options_print (_: Protocol.OptionsPrint): EMainM Protocol.Options := do
+    return (← getMainState).options
+  goal_start (args: Protocol.GoalStart): EMainM Protocol.GoalStartResult := do
+    let levelNames := (args.levels?.getD #[]).toList.map (·.toName)
+    let expr?: Except _ GoalState ← liftTermElabM (levelNames := levelNames) do
+      match args.expr, args.copyFrom with
+      | .some expr, .none => goalStartExpr expr |>.run
+      | .none, .some copyFrom => do
+        (match (← getEnv).find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
         | .some cInfo => return .ok (← GoalState.create cInfo.type))
       | _, _ =>
-        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
+        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied"
     match expr? with
-    | .error error => return .error error
+    | .error error => Protocol.throw error
     | .ok goalState =>
       let stateId ← newGoalState goalState
-      return .ok { stateId, root := goalState.root.name.toString }
-  goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
-    let state ← get
+      return { stateId, root := goalState.root.name.toString }
+  goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
+    let state ← getMainState
     let .some goalState := state.goalStates[args.stateId]? |
-      return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let .some goal := goalState.goals.get? args.goalId |
-      return .error $ errorIndex s!"Invalid goal index {args.goalId}"
-    let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
-      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?  with
-      | .some tactic, .none, .none, .none, .none, .none => do
+      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
+    let .some goal := goalState.goals[args.goalId]? |
+      Protocol.throw $ errorIndex s!"Invalid goal index {args.goalId}"
+    let nextGoalState?: Except _ TacticResult ← liftTermElabM 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
         pure <| Except.ok <| ← goalState.tryTactic goal tactic
-      | .none, .some expr, .none, .none, .none, .none => do
+      | .none, .some expr, .none, .none, .none, .none, .none => do
         pure <| Except.ok <| ← goalState.tryAssign goal expr
-      | .none, .none, .some type, .none, .none, .none => do
+      | .none, .none, .some type, .none, .none, .none, .none => do
         let binderName := args.binderName?.getD ""
         pure <| Except.ok <| ← goalState.tryHave goal binderName type
-      | .none, .none, .none, .some type, .none, .none => do
+      | .none, .none, .none, .some type, .none, .none, .none => do
         let binderName := args.binderName?.getD ""
         pure <| Except.ok <| ← goalState.tryLet goal binderName type
-      | .none, .none, .none, .none, .some pred, .none => do
+      | .none, .none, .none, .none, .some pred, .none, .none => do
         pure <| Except.ok <| ← goalState.tryCalc goal pred
-      | .none, .none, .none, .none, .none, .some true => do
+      | .none, .none, .none, .none, .none, .some true, .none => do
         pure <| Except.ok <| ← goalState.conv goal
-      | .none, .none, .none, .none, .none, .some false => do
+      | .none, .none, .none, .none, .none, .some false, .none => do
         pure <| Except.ok <| ← goalState.convExit
-      | _, _, _, _, _, _ =>
-        let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
-        pure $ Except.error $ error
+      | .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, let, calc, conv, draft} must be supplied"
+        pure $ .error error
     match nextGoalState? with
-    | .error error => return .error error
+    | .error error => Protocol.throw error
     | .ok (.success nextGoalState) => do
       let nextGoalState ← match state.options.automaticMode, args.conv? with
         | true, .none => do
           let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
-            throwError "Resuming known goals"
+            Protocol.throw $ errorIO "Resuming known goals"
           pure result
         | true, .some true => pure nextGoalState
         | true, .some false => do
           let .some (_, _, dormantGoals) := goalState.convMVar? |
-            throwError "If conv exit succeeded this should not fail"
+            Protocol.throw $ errorIO "If conv exit succeeded this should not fail"
           let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
-            throwError "Resuming known goals"
+            Protocol.throw $ errorIO "Resuming known goals"
           pure result
         | false, _ => pure nextGoalState
       let nextStateId ← newGoalState nextGoalState
-      let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
-      return .ok {
+      let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
+      return {
         nextStateId? := .some nextStateId,
         goals? := .some goals,
       }
     | .ok (.parseError message) =>
-      return .ok { parseError? := .some message }
+      return { parseError? := .some message }
     | .ok (.invalidAction message) =>
-      return .error $ errorI "invalid" message
+      Protocol.throw $ errorI "invalid" message
     | .ok (.failure messages) =>
-      return .ok { tacticErrors? := .some messages }
-  goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
-    let state ← get
+      return { tacticErrors? := .some messages }
+  goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
+    let state ← getMainState
     let .some target := state.goalStates[args.target]? |
-      return .error $ errorIndex s!"Invalid state index {args.target}"
-    let nextState? ← match args.branch?, args.goals? with
+      Protocol.throw $ errorIndex s!"Invalid state index {args.target}"
+    let nextGoalState? : GoalState  ← match args.branch?, args.goals? with
       | .some branchId, .none => do
         match state.goalStates[branchId]? with
-        | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
+        | .none => Protocol.throw $ errorIndex s!"Invalid state index {branchId}"
         | .some branch => pure $ target.continue branch
       | .none, .some goals =>
-        pure $ goalResume target goals
-      | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
-    match nextState? with
-    | .error error => return .error <| errorI "structure" error
+        let goals := goals.toList.map (λ n => { name := n.toName })
+        pure $ target.resume goals
+      | _, _ => Protocol.throw $ errorI "arguments" "Exactly one of {branch, goals} must be supplied"
+    match nextGoalState? with
+    | .error error => Protocol.throw $ errorI "structure" error
     | .ok nextGoalState =>
       let nextStateId ← newGoalState nextGoalState
-      let goals ← goalSerialize nextGoalState (options := state.options)
-      return .ok {
+      let goals ← liftMetaM $ goalSerialize nextGoalState (options := state.options)
+      return {
         nextStateId,
         goals,
       }
-  goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
-    let state ← get
+  goal_delete (args: Protocol.GoalDelete): EMainM Protocol.GoalDeleteResult := do
+    let state ← getMainState
     let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
     set { state with goalStates }
-    return .ok {}
-  goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
-    let state ← get
+    return {}
+  goal_print (args: Protocol.GoalPrint): EMainM Protocol.GoalPrintResult := do
+    let state ← getMainState
     let .some goalState := state.goalStates[args.stateId]? |
-      return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← runMetaInMainM <| goalPrint goalState state.options
-    return .ok result
-  goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
-    let state ← get
+      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
+    let result ← liftMetaM <| goalPrint
+        goalState
+        (rootExpr := args.rootExpr?.getD False)
+        (parentExpr := args.parentExpr?.getD False)
+        (goals := args.goals?.getD False)
+        (extraMVars := args.extraMVars?.getD #[])
+        (options := state.options)
+    return result
+  goal_save (args: Protocol.GoalSave): EMainM Protocol.GoalSaveResult := do
+    let state ← getMainState
     let .some goalState := state.goalStates[args.id]? |
-      return .error $ errorIndex s!"Invalid state index {args.id}"
+      Protocol.throw $ 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)
+    return {}
+  goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do
+    let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
     let id ← newGoalState goalState
-    return .ok { id }
-  frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
-    let options := (← get).options
-    try
-      let (fileName, file) ← match args.fileName?, args.file? with
-        | .some fileName, .none => do
-          let file ← IO.FS.readFile fileName
-          pure (fileName, file)
-        | .none, .some file =>
-          pure ("<anonymous>", file)
-        | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
-      let env?: Option Lean.Environment ← if args.fileName?.isSome then
-          pure .none
-        else do
-          let env ← Lean.MonadEnv.getEnv
-          pure <| .some env
-      let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
-      let frontendM := Frontend.mapCompilationSteps λ step => do
-        let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
-        let invocations?: Option (List Protocol.InvokedTactic) ← if args.invocations then
-            let invocations ← Frontend.collectTacticsFromCompilationStep step
-            pure $ .some invocations
-          else
-            pure .none
-        let sorrys := if args.sorrys then
-            Frontend.collectSorrys step
-          else
-            []
-        let messages ← step.messageStrings
-        return (step.before, boundary, invocations?, sorrys, messages)
-      let li ← frontendM.run context |>.run' state
-      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 goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
-            let stateId ← newGoalState goalState
-            let goals ← goalSerialize goalState options
-            pure (.some stateId, goals)
-        return {
-          boundary,
-          invocations?,
-          goalStateId?,
-          goals,
-          messages,
-        }
-      return .ok { units }
-    catch e =>
-      return .error $ errorI "frontend" (← e.toMessageData.toString)
+    return { id }
+  frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
+    frontend_process_inner args
 
 end Pantograph.Repl

Test/Common.lean

@@ -48,6 +48,12 @@ 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 }
@@ -61,8 +67,8 @@ protected def Goal.devolatilize (goal: Goal): Goal :=
 
 end Condensed
 
-def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals.get! i
-def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.goals.get! goalId) tactic
+def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
+def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
 
 def TacticResult.toString : TacticResult → String
   | .success state => s!".success ({state.goals.length} goals)"
@@ -95,22 +101,22 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq)
 
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 
-def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do
+def strToTermSyntax (s: String): CoreM Syntax := do
   let .ok stx := Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := s)
-    (fileName := filename) | panic! s!"Failed to parse {s}"
+    (fileName := ← getFileName) | panic! s!"Failed to parse {s}"
   return stx
-def parseSentence (s: String): Elab.TermElabM Expr := do
+def parseSentence (s : String) (expectedType? : Option Expr := .none) : Elab.TermElabM Expr := do
   let stx ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := s)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
-  Elab.Term.elabTerm (stx := stx) .none
+  Elab.Term.elabTerm (stx := stx) expectedType?
 
 def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
     let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
@@ -123,22 +129,30 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
 
 -- Monadic testing
 
-abbrev TestT := StateT LSpec.TestSeq
+abbrev TestT := StateRefT' IO.RealWorld LSpec.TestSeq
 
-def addTest [Monad m] (test: LSpec.TestSeq) : TestT m Unit := do
+section Monadic
+
+variable [Monad m] [MonadLiftT (ST IO.RealWorld) m]
+
+def addTest (test: LSpec.TestSeq) : TestT m Unit := do
   set $ (← get) ++ test
 
-def checkEq [Monad m] [DecidableEq α] (desc : String) (lhs rhs : α) : TestT m Unit := do
-  addTest $ LSpec.check desc (lhs == rhs)
-def checkTrue [Monad m] (desc : String) (flag : Bool) : TestT m Unit := do
+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 [Monad m] (desc : String) : TestT m Unit := do
+def fail (desc : String) : TestT m Unit := do
   addTest $ LSpec.check desc false
 
-def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq :=
+def runTest (t: TestT m Unit): m LSpec.TestSeq :=
   Prod.snd <$> t.run LSpec.TestSeq.done
-def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) :=
+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

@@ -3,10 +3,9 @@ import Pantograph.Delate
 import Test.Common
 import Lean
 
-open Lean
-namespace Pantograph.Test.Delate
+open Lean Pantograph
 
-open Pantograph
+namespace Pantograph.Test.Delate
 
 deriving instance Repr, DecidableEq for Protocol.BoundExpression
 
@@ -35,7 +34,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
     ("Nat.add", "(:forall a (:c Nat) (:forall a (: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)) :implicit) :implicit)"),
+    ("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)"),
     -- 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 +49,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) :implicit)"),
-    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
+    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
+    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
     ("(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 +76,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)) :implicit) :implicit)"
+      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)"
     ),
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
@@ -96,6 +95,30 @@ def test_instance (env: Environment): IO LSpec.TestSeq :=
     let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
     return LSpec.TestSeq.done
 
+def test_projection_prod (env: Environment) : IO LSpec.TestSeq:= runTest do
+  let struct := .app (.bvar 1) (.bvar 0)
+  let expr := .proj `Prod 1 struct
+  let .field projector numParams := analyzeProjection env expr |
+    fail "`Prod has fields"
+  checkEq "projector" projector `Prod.snd
+  checkEq "numParams" numParams 2
+
+def test_projection_exists (env: Environment) : IO LSpec.TestSeq:= runTest do
+  let struct := .app (.bvar 1) (.bvar 0)
+  let expr := .proj `Exists 1 struct
+  let .singular recursor numParams numFields := analyzeProjection env expr |
+    fail "`Exists has no projectors"
+  checkEq "recursor" recursor `Exists.recOn
+  checkEq "numParams" numParams 2
+  checkEq "numFields" numFields 2
+
+def test_matcher : TestT Elab.TermElabM Unit := do
+  let t ← parseSentence "Nat → Nat"
+  let e ← parseSentence "fun (n : Nat) => match n with | 0 => 0 | k => k" (.some t)
+  let .some _ ← Meta.matchMatcherApp? e.bindingBody! | fail "Must be a matcher app"
+  let e' ← instantiateAll e
+  checkTrue "ok" <| ← Meta.isTypeCorrect e'
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("serializeName", do pure test_serializeName),
@@ -104,6 +127,9 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Sexp from elaborated expr", test_sexp_of_elab env),
     ("Sexp from expr", test_sexp_of_expr env),
     ("Instance", test_instance env),
+    ("Projection Prod", test_projection_prod env),
+    ("Projection Exists", test_projection_exists env),
+    ("Matcher", runTestTermElabM env test_matcher),
   ]
 
 end Pantograph.Test.Delate

Test/Environment.lean

@@ -97,11 +97,37 @@ 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 := {})).run | 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
+    let { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩
+    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
+    checkTrue "constNames" $ constNames.contains "Nat.succ_add"
+
+def test_matcher : TestT IO Unit := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
+  checkTrue "not matcher" $ ¬ Meta.isMatcherCore env `Nat.strongRecOn
+
 def suite: List (String × IO LSpec.TestSeq) :=
   [
     ("Catalog", test_catalog),
     ("Symbol Visibility", test_symbol_visibility),
     ("Inspect", test_inspect),
+    ("Symbol Location", runTest test_symbol_location),
+    ("Matcher", runTest test_matcher),
   ]
 
 end Pantograph.Test.Environment

Test/Frontend.lean

@@ -1,22 +1,40 @@
-import LSpec
 import Pantograph
 import Repl
 import Test.Common
 
+import LSpec
+
 open Lean Pantograph
 namespace Pantograph.Test.Frontend
 
-def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
+def runFrontend { α } (source: String) (f : Frontend.CompilationStep → IO α) : MetaM (List α) := do
+  let filename := "<anonymous>"
+  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
+  let m := Frontend.mapCompilationSteps f
+  m.run context |>.run' state
+
+def test_open : TestT MetaM Unit := do
+  let sketch := "
+open Nat
+example : ∀ (n : Nat), n + 1 = Nat.succ n := by
+  intro
+  apply add_one
+  "
+  let errors ← runFrontend sketch λ step => step.msgs.mapM (·.toString)
+  checkEq "errors" errors [[], []]
+
+def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
+    : 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)
+    return (step.before, ← Frontend.collectSorrys step options)
   let li ← m.run context |>.run' state
   let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
     if sorrys.isEmpty then
       return .none
-    let goalState ← Frontend.sorrysToGoalState sorrys
-    return .some goalState
+    let { state, .. } ← Frontend.sorrysToGoalState sorrys
+    return .some state
   return goalStates
 
 def test_multiple_sorrys_in_proof : TestT MetaM Unit := do
@@ -177,14 +195,71 @@ 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 := [
+    ("open", test_open),
     ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
     ("sorry_in_middle", test_sorry_in_middle),
     ("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

@@ -8,23 +8,33 @@ import Test.Common
 namespace Pantograph.Test.Integration
 open Pantograph.Repl
 
-def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json))
-    (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do
-  let payload := Lean.Json.mkObj payload
+deriving instance Lean.ToJson for Protocol.EnvInspect
+deriving instance Lean.ToJson for Protocol.EnvAdd
+deriving instance Lean.ToJson for Protocol.ExprEcho
+deriving instance Lean.ToJson for Protocol.OptionsSet
+deriving instance Lean.ToJson for Protocol.OptionsPrint
+deriving instance Lean.ToJson for Protocol.GoalStart
+deriving instance Lean.ToJson for Protocol.GoalPrint
+deriving instance Lean.ToJson for Protocol.GoalTactic
+deriving instance Lean.ToJson for Protocol.FrontendProcess
+
+def step { α β } [Lean.ToJson α] [Lean.ToJson β] (cmd: String) (payload: α)
+    (expected: β) (name? : Option String := .none): MainM LSpec.TestSeq := do
+  let payload := Lean.toJson payload
   let name := name?.getD s!"{cmd} {payload.compress}"
   let result ← Repl.execute { cmd, payload }
-  return LSpec.test name (toString result = toString (Lean.toJson expected))
+  return LSpec.test name (result.pretty = (Lean.toJson expected).pretty)
 
 abbrev Test := List (MainM LSpec.TestSeq)
 
-def test_elab : Test :=
+def test_expr_echo : Test :=
   [
     step "expr.echo"
-      [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
-     (Lean.toJson ({
+     ({ expr := "λ {α : Sort (u + 1)} => List α", levels? := .some #["u"]}: Protocol.ExprEcho)
+     ({
        type := { pp? := .some "{α : Type u} → Type u" },
        expr := { pp? := .some "fun {α} => List α" }
-     }: Protocol.ExprEchoResult)),
+     }: Protocol.ExprEchoResult),
   ]
 
 def test_option_modify : Test :=
@@ -33,50 +43,72 @@ def test_option_modify : Test :=
   let module? := Option.some "Init.Data.Nat.Basic"
   let options: Protocol.Options := {}
   [
-    step "env.inspect" [("name", .str "Nat.add_one")]
+    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
      ({ type := { pp? }, module? }: Protocol.EnvInspectResult),
-    step "options.set" [("printExprAST", .bool true)]
+    step "options.set" ({ printExprAST? := .some true } : Protocol.OptionsSet)
      ({ }: Protocol.OptionsSetResult),
-    step "env.inspect" [("name", .str "Nat.add_one")]
+    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
      ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
-    step "options.print" []
+    step "options.print" ({} : Protocol.OptionsPrint)
      ({ options with printExprAST := true }: Protocol.Options),
   ]
 def test_malformed_command : Test :=
   let invalid := "invalid"
   [
-    step invalid [("name", .str "Nat.add_one")]
+    step invalid ({ name := "Nat.add_one" }: Protocol.EnvInspect)
      ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
      (name? := .some "Invalid Command"),
-    step "expr.echo" [(invalid, .str "Random garbage data")]
+    step "expr.echo" (Lean.Json.mkObj [(invalid, .str "Random garbage data")])
      ({ error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected" }:
       Protocol.InteractionError)
     (name? := .some "JSON Deserialization")
   ]
 def test_tactic : Test :=
+  let varX := { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}
   let goal1: Protocol.Goal := {
     name := "_uniq.11",
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
-    vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}],
+    vars := #[varX],
   }
   let goal2: Protocol.Goal := {
-    name := "_uniq.17",
+    name := "_uniq.14",
     target := { pp? := .some "x ∨ y → y ∨ x" },
     vars := #[
-      { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
+      varX,
+      { name := "_uniq.13", userName := "y", type? := .some { pp? := .some "Prop" }}
     ],
   }
   [
-    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p" }: Protocol.GoalStart)
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
-    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    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")]
+    step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
+     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
+     ({ tacticErrors? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
+      Protocol.GoalTacticResult)
   ]
+example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
+  simp
+def test_tactic_timeout : Test :=
+  [
+    step "goal.start" ({ expr := "(1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3" }: Protocol.GoalStart)
+     ({ stateId := 0, root := "_uniq.319" }: Protocol.GoalStartResult),
+    -- timeout of 10 milliseconds
+    step "options.set" ({ timeout? := .some 10 } : Protocol.OptionsSet)
+     ({ }: Protocol.OptionsSetResult),
+    step "goal.tactic" ({ stateId := 0, expr? := .some "by\nsleep 1000; simp" }: Protocol.GoalTactic)
+     ({ error := "internal", desc := "interrupt" }: Protocol.InteractionError),
+    -- ensure graceful recovery
+    step "options.set" ({ timeout? := .some 0 } : Protocol.OptionsSet)
+     ({ }: Protocol.OptionsSetResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "simp" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 1, goals? := .some #[], }: Protocol.GoalTacticResult),
+  ]
+
 def test_automatic_mode (automatic: Bool): Test :=
   let varsPQ := #[
     { name := "_uniq.10", userName := "p", type? := .some { pp? := .some "Prop" }},
@@ -90,75 +122,89 @@ def test_automatic_mode (automatic: Bool): Test :=
     ],
   }
   let goal2l: Protocol.Goal := {
-    name := "_uniq.59",
+    name := "_uniq.61",
     userName? := .some "inl",
     target := { pp? := .some "q ∨ p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
     ],
   }
   let goal2r: Protocol.Goal := {
-    name := "_uniq.72",
+    name := "_uniq.74",
     userName? := .some "inr",
     target := { pp? := .some "q ∨ p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
+      { name := "_uniq.62", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
     ],
   }
   let goal3l: Protocol.Goal := {
-    name := "_uniq.78",
+    name := "_uniq.80",
     userName? := .some "inl.h",
     target := { pp? := .some "p" },
     vars := varsPQ ++ #[
-      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
     ],
   }
   [
-    step "options.set" [("automaticMode", .bool automatic)]
+    step "options.set" ({automaticMode? := .some automatic}: Protocol.OptionsSet)
      ({}: Protocol.OptionsSetResult),
-    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p"} : Protocol.GoalStart)
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
-    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")]
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro p q h" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")]
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "cases h" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult),
     let goals? := if automatic then #[goal3l, goal2r] else #[goal3l]
-    step "goal.tactic" [("stateId", .num 2), ("goalId", .num 0), ("tactic", .str "apply Or.inr")]
+    step "goal.tactic" ({ stateId := 2, tactic? := .some "apply Or.inr" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult),
   ]
 
 def test_env_add_inspect : Test :=
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
+  let name3 := "Pantograph.mystery3"
   [
     step "env.add"
-      [
-        ("name", .str name1),
-        ("type", .str "Prop → Prop → Prop"),
-        ("value", .str "λ (a b: Prop) => Or a b"),
-        ("isTheorem", .bool false)
-      ]
+      ({
+        name := name1,
+        value := "λ (a b: Prop) => Or a b",
+        isTheorem := false
+      }: Protocol.EnvAdd)
      ({}: Protocol.EnvAddResult),
-    step "env.inspect" [("name", .str name1)]
+    step "env.inspect" ({name := name1, value? := .some true} : Protocol.EnvInspect)
      ({
        value? := .some { pp? := .some "fun a b => a ∨ b" },
        type := { pp? := .some "Prop → Prop → Prop" },
      }:
       Protocol.EnvInspectResult),
     step "env.add"
-      [
-        ("name", .str name2),
-        ("type", .str "Nat → Int"),
-        ("value", .str "λ (a: Nat) => a + 1"),
-        ("isTheorem", .bool false)
-      ]
+      ({
+        name := name2,
+        type? := "Nat → Int",
+        value := "λ (a: Nat) => a + 1",
+        isTheorem := false
+      }: Protocol.EnvAdd)
      ({}: Protocol.EnvAddResult),
-    step "env.inspect" [("name", .str name2)]
+    step "env.inspect" ({name := name2, value? := .some true} : Protocol.EnvInspect)
      ({
        value? := .some { pp? := .some "fun a => ↑a + 1" },
        type := { pp? := .some "Nat → Int" },
      }:
-      Protocol.EnvInspectResult)
+      Protocol.EnvInspectResult),
+    step "env.add"
+      ({
+        name := name3,
+        levels? := .some #["u"]
+        type? := "(α : Type u) → α → (α × α)",
+        value := "λ (α : Type u) (x : α) => (x, x)",
+        isTheorem := false
+      }: Protocol.EnvAdd)
+     ({}: Protocol.EnvAddResult),
+    step "env.inspect" ({name := name3} : Protocol.EnvInspect)
+     ({
+       type := { pp? := .some "(α : Type u) → α → α × α" },
+     }:
+      Protocol.EnvInspectResult),
   ]
 
 example : ∀ (p: Prop), p → p := by
@@ -166,15 +212,14 @@ example : ∀ (p: Prop), p → p := by
   exact h
 
 def test_frontend_process : Test :=
+  let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
+  let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
   [
-    let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
-    let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
     step "frontend.process"
-      [
-        ("file", .str file),
-        ("invocations", .bool true),
-        ("sorrys", .bool false),
-      ]
+      ({
+        file? := .some file,
+        invocations := true,
+      }: Protocol.FrontendProcess)
      ({
        units := [{
          boundary := (0, file.utf8ByteSize),
@@ -210,47 +255,73 @@ def test_frontend_process_sorry : Test :=
       vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
     }
     step "frontend.process"
-      [
-        ("file", .str file),
-        ("invocations", .bool false),
-        ("sorrys", .bool true),
-      ]
+      ({
+        file? := .some file,
+        sorrys := true,
+      }: Protocol.FrontendProcess)
      ({
        units := [{
          boundary := (0, solved.utf8ByteSize),
        }, {
          boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
          goalStateId? := .some 0,
-         goals := #[goal1],
+         goals? := .some #[goal1],
+         goalSrcBoundaries? := .some #[(57, 62)],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
-    }: Protocol.FrontendProcessResult),
+     }: Protocol.FrontendProcessResult),
   ]
 
+def test_import_open : Test :=
+  let header := "import Init\nopen Nat\nuniverse u"
+  let goal1: Protocol.Goal := {
+    name := "_uniq.67",
+    target := { pp? := .some "n + 1 = n.succ" },
+    vars := #[{ name := "_uniq.66", userName := "n", type? := .some { pp? := .some "Nat" }}],
+  }
+  [
+    step "frontend.process"
+      ({
+        file? := .some header,
+        readHeader := true,
+        inheritEnv := true,
+      }: Protocol.FrontendProcess)
+     ({
+       units := [
+         { boundary := (12, 21) },
+         { boundary := (21, header.utf8ByteSize) },
+       ],
+     }: Protocol.FrontendProcessResult),
+    step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart)
+     ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro n" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 2, goals? := .some #[], }: Protocol.GoalTacticResult),
+    step "goal.start" ({ expr := "∀ (x : Sort u), Sort (u + 1)"} : Protocol.GoalStart)
+     ({ stateId := 3, root := "_uniq.5" }: Protocol.GoalStartResult),
+  ]
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
-  let context: Context := {
-    imports := ["Init"]
-  }
-  let commands: MainM LSpec.TestSeq :=
-    steps.foldlM (λ suite step => do
-      let result ← step
-      return suite ++ result) LSpec.TestSeq.done
-  runCoreMSeq env <| commands.run context |>.run' {}
-
+  let coreContext ← createCoreContext #[]
+  let mainM : MainM LSpec.TestSeq :=
+    steps.foldlM (λ suite step => do return suite ++ (← step)) LSpec.TestSeq.done
+  mainM.run { coreContext } |>.run' { env }
 
 def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
-    ("expr.echo", test_elab),
+    ("expr.echo", test_expr_echo),
     ("options.set options.print", test_option_modify),
     ("Malformed command", test_malformed_command),
     ("Tactic", test_tactic),
+    ("Tactic Timeout", test_tactic_timeout),
     ("Manual Mode", test_automatic_mode false),
     ("Automatic Mode", test_automatic_mode true),
     ("env.add env.inspect", test_env_add_inspect),
     ("frontend.process invocation", test_frontend_process),
     ("frontend.process sorry", test_frontend_process_sorry),
+    ("frontend.process import", test_import_open),
   ]
   tests.map (fun (name, test) => (name, runTest env test))
 

Test/Library.lean

@@ -8,15 +8,18 @@ open Pantograph
 
 namespace Pantograph.Test.Library
 
+def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
+  termElabM.run' (ctx := defaultElabContext) |>.run'
+
 def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
   let inner: CoreM LSpec.TestSeq := do
     let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
     let tests := LSpec.TestSeq.done
-    let echoResult ← exprEcho prop_and_proof (options := {})
+    let echoResult ← runTermElabM $ exprEcho prop_and_proof (options := {})
     let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
       type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
     }))
-    let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
+    let echoResult ← runTermElabM $ exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
     let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
       type := {
         pp? := "(p : Prop) ×' p",

Test/Main.lean

@@ -17,9 +17,9 @@ def addPrefix (pref: String) (tests: List (String × α)): List (String  × α)
   tests.map (λ (name, x) => (pref ++ "/" ++ name, x))
 
 /-- Runs test in parallel. Filters test name if given -/
-def runTestGroup (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
-  let tests: List (String × IO LSpec.TestSeq) := match filter with
-    | .some filter => tests.filter (λ (name, _) => filter.isPrefixOf name)
+def runTestGroup (nameFilter?: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
+  let tests: List (String × IO LSpec.TestSeq) := match nameFilter? with
+    | .some nameFilter => tests.filter (λ (name, _) => nameFilter.isPrefixOf name)
     | .none => tests
   let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do
     return (name, ← EIO.asTask task))
@@ -37,7 +37,7 @@ open Pantograph.Test
 
 /-- Main entry of tests; Provide an argument to filter tests by prefix -/
 def main (args: List String) := do
-  let name_filter := args.head?
+  let nameFilter? := args.head?
   Lean.initSearchPath (← Lean.findSysroot)
   let env_default: Lean.Environment ← Lean.importModules
     (imports := #[`Init])
@@ -53,10 +53,8 @@ def main (args: List String) := do
     ("Proofs", Proofs.suite env_default),
     ("Delate", Delate.suite env_default),
     ("Serial", Serial.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),
+    ("Tactic/Assign", Tactic.Assign.suite env_default),
     ("Tactic/Prograde", Tactic.Prograde.suite env_default),
   ]
   let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
-  LSpec.lspecIO (← runTestGroup name_filter tests)
+  LSpec.lspecEachIO [()] (λ () => runTestGroup nameFilter? tests)

Test/Metavar.lean

@@ -8,10 +8,7 @@ namespace Pantograph.Test.Metavar
 open Pantograph
 open Lean
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
-
-def addTest (test: LSpec.TestSeq): TestM Unit := do
-  set $ (← get) ++ test
+abbrev TestM := TestT $ ReaderT Protocol.Options Elab.TermElabM
 
 -- Tests that all delay assigned mvars are instantiated
 def test_instantiate_mvar: TestM Unit := do
@@ -32,8 +29,6 @@ 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
@@ -197,7 +192,7 @@ def test_proposition_generation: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "?m.29 x"])
+    #[.some "?m.30 x"])
   addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
 
   let assign := "Eq.refl x"
@@ -244,7 +239,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 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Roundtrip
@@ -258,7 +253,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 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
 
   -- Continuation should fail if the state does not exist:

Test/Proofs.lean

@@ -14,10 +14,7 @@ inductive Start where
   | copy (name: String) -- Start from some name in the environment
   | expr (expr: String) -- Start from some expression
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
-
-def addTest (test: LSpec.TestSeq): TestM Unit := do
-  set $ (← get) ++ test
+abbrev TestM := TestT $ ReaderT Protocol.Options $ Elab.TermElabM
 
 def startProof (start: Start): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
@@ -100,7 +97,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!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
 
 -- Individual test cases
@@ -244,13 +241,15 @@ def test_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let fvP := "_uniq.10"
-  let fvQ := "_uniq.13"
-  let fvH := "_uniq.16"
-  let state1g0 := "_uniq.17"
+  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)
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
     #[{
-      name := state1g0,
+      name := state1g0.name.toString,
       target := { pp? := .some "q ∨ p" },
       vars := #[
         { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
@@ -262,7 +261,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!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
   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
@@ -272,14 +271,16 @@ 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 (caseL, caseR) := ("_uniq.64", "_uniq.77")
+  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)
   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!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
   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}))"
@@ -295,8 +296,9 @@ 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!) (sanitize := false)
-  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
+    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}))")
   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
@@ -326,7 +328,7 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
+  addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals[0]!])
   let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
     | other => do
@@ -541,168 +543,76 @@ def test_calc: TestM Unit := do
         ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
       buildGoal free target userName?
 
-def test_nat_zero_add: TestM Unit := do
-  let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
+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 n"
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[buildGoal [("n", "Nat")] "n + 0 = n"])
-  let recursor := "@Nat.brecOn"
-  let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
-    #[
-      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"
-  let state3b ← match ← state2.tacticOn (goalId := 1) (tactic := tactic) with
+  let tactic := "intro p"
+  let state1 ← match ← state0.tacticOn 0 tactic with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check tactic ((← state3b.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-  let state2b ← match state3b.continue state2 with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
-  let tactic := "exact (λ x => x + 0 = x)"
-  let state3c ← match ← state2b.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state3c.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-  let state2c ← match state3c.continue state2b with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
-  let tactic := "intro t h"
-  let state3 ← match ← state2c.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
 
-  let tactic := "simp"
-  let state3d ← match ← state3.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  let state2d ← match state3d.continue state2c with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
-  let tactic := "rfl"
-  let stateF ← match ← state2d.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) =
-    #[])
+  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"]
 
-  let expr := stateF.mctx.eAssignment.find! stateF.root
-  let (expr, _) := instantiateMVarsCore (mctx := stateF.mctx) (e := expr)
-  addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome
-
-def test_nat_zero_add_alt: TestM Unit := do
-  let state? ← startProof (.expr "∀ (n: Nat), n + 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 n"
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[buildGoal [("n", "Nat")] "n + 0 = n"])
-  let recursor := "@Nat.brecOn"
-  let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  let major := "_uniq.68"
-  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
-    #[
-      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"
-  let state3m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
+  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 ()
-  addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")])
-  let tactic := "apply Eq"
-  let state3m2 ← match ← state3m.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  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
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
 
-  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 := "_uniq.63"
-  let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
-  let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
-  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
+  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 test_deconstruct : TestM Unit := do
+  let state? ← startProof (.expr "∀ (p q : Prop) (h : And p q), And q p")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro p q ⟨hp, hq⟩"
+  let state1 ← match ← state0.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      fail other.toString
+      return ()
+  checkEq tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize))
     #[
-      {
-        name := "_uniq.70",
-        userName? := .some "conduit",
-        target := {
-          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,
-          userName := "n",
-          type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
-        }],
-      }
-    ])
+      buildGoal [("p", "Prop"), ("q", "Prop"), ("hp", "p"), ("hq", "q")] "q ∧ p"
+    ]
+
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
@@ -714,8 +624,9 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Or.comm", test_or_comm),
     ("conv", test_conv),
     ("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),
+    ("deconstruct", test_deconstruct),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))
 

Test/Serial.lean

@@ -47,12 +47,8 @@ def test_environment_pickling : TestM Unit := do
       (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
+    addDecl c
+    environmentPickle (← getEnv) envPicklePath
 
   let _ ← runCoreM coreDst do
     let (env', _) ← environmentUnpickle envPicklePath

Test/Tactic.lean

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

Test/Tactic/Assign.lean

@@ -0,0 +1,33 @@
+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

@@ -1,88 +0,0 @@
-import LSpec
-import Lean
-import Test.Common
-
-open Lean
-open Pantograph
-
-namespace Pantograph.Test.Tactic.Congruence
-
-def test_congr_arg_list : TestT Elab.TermElabM Unit := do
-  let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
-  let expr ← parseSentence expr
-  Meta.lambdaTelescope expr $ λ _ body => do
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-      [
-        (`α, "Sort ?u.30"),
-        (`a₁, "?α"),
-        (`a₂, "?α"),
-        (`f, "?α → List α"),
-        (`h, "?a₁ = ?a₂"),
-        (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
-      ])
-    let f := newGoals.get! 3
-    let h := newGoals.get! 4
-    let c := newGoals.get! 5
-    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) = "(?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
-  Meta.lambdaTelescope expr $ λ _ body => do
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
-    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-      [
-        (`α, "Sort ?u.70"),
-        (`a₁, "?α"),
-        (`a₂, "?α"),
-        (`f, "?α → Nat"),
-        (`h, "?a₁ = ?a₂"),
-        (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
-      ])
-def test_congr_fun : TestT Elab.TermElabM Unit := do
-  let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
-  let expr ← parseSentence expr
-  Meta.lambdaTelescope expr $ λ _ body => do
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-      [
-        (`α, "Sort ?u.159"),
-        (`f₁, "?α → Nat"),
-        (`f₂, "?α → Nat"),
-        (`h, "?f₁ = ?f₂"),
-        (`a, "?α"),
-        (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
-      ])
-def test_congr : TestT Elab.TermElabM Unit := do
-  let expr := "λ (a b: Nat) => a = b"
-  let expr ← parseSentence expr
-  Meta.lambdaTelescope expr $ λ _ body => do
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let newGoals ← runTacticOnMVar Tactic.evalCongruence target.mvarId!
-    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-      [
-        (`α, "Sort ?u.10"),
-        (`f₁, "?α → Nat"),
-        (`f₂, "?α → Nat"),
-        (`a₁, "?α"),
-        (`a₂, "?α"),
-        (`h₁, "?f₁ = ?f₂"),
-        (`h₂, "?a₁ = ?a₂"),
-        (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
-      ])
-
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("congrArg List.reverse", test_congr_arg_list),
-    ("congrArg", test_congr_arg),
-    ("congrFun", test_congr_fun),
-    ("congr", test_congr),
-  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
-
-end Pantograph.Test.Tactic.Congruence

Test/Tactic/MotivatedApply.lean

@@ -1,113 +0,0 @@
-import LSpec
-import Lean
-import Test.Common
-
-open Lean
-open Pantograph
-
-namespace Pantograph.Test.Tactic.MotivatedApply
-
-def test_type_extract : TestT Elab.TermElabM Unit := do
-  let recursor ← parseSentence "@Nat.brecOn"
-  let recursorType ← Meta.inferType recursor
-  addTest $ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
-    (← exprToStr recursorType))
-  let info ← match Tactic.getRecursorInformation recursorType with
-    | .some info => pure info
-    | .none => throwError "Failed to extract recursor info"
-  addTest $ LSpec.check "iMotive" (info.iMotive = 2)
-  let motiveType := info.getMotiveType
-  addTest $ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
-    (← exprToStr motiveType))
-
-def test_nat_brec_on : TestT Elab.TermElabM Unit := do
-  let expr := "λ (n t: Nat) => n + 0 = n"
-  let expr ← parseSentence expr
-  Meta.lambdaTelescope expr $ λ _ body => do
-    let recursor ← match Parser.runParserCategory
-      (env := ← MonadEnv.getEnv)
-      (catName := `term)
-      (input := "@Nat.brecOn")
-      (fileName := filename) with
-      | .ok syn => pure syn
-      | .error error => throwError "Failed to parse: {error}"
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.evalMotivatedApply recursor
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    let test :=  LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-      [
-        "Nat → Prop",
-        "Nat",
-        "∀ (t : Nat), Nat.below t → ?motive t",
-        "?motive ?m.67 = (n + 0 = n)",
-      ])
-    addTest test
-
-def test_list_brec_on : TestT Elab.TermElabM Unit := do
-  let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
-  let expr ← parseSentence expr
-  Meta.lambdaTelescope expr $ λ _ body => do
-    let recursor ← match Parser.runParserCategory
-      (env := ← MonadEnv.getEnv)
-      (catName := `term)
-      (input := "@List.brecOn")
-      (fileName := filename) with
-      | .ok syn => pure syn
-      | .error error => throwError "Failed to parse: {error}"
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.evalMotivatedApply recursor
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-      [
-        "Type ?u.90",
-        "List ?m.92 → Prop",
-        "List ?m.92",
-        "∀ (t : List ?m.92), List.below t → ?motive t",
-        "?motive ?m.94 = (l ++ [] = [] ++ l)",
-      ])
-
-def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
-  let expr := "λ (n t: Nat) => n + 0 = n"
-  let recursor ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `term)
-    (input := "@Nat.brecOn")
-    (fileName := filename) with
-    | .ok syn => pure syn
-    | .error error => throwError "Failed to parse: {error}"
-  let expr ← parseSentence expr
-  Meta.lambdaTelescope expr $ λ _ body => do
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.evalMotivatedApply recursor
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    let majorId := 67
-    addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-      [
-        "Nat → Prop",
-        "Nat",
-        "∀ (t : Nat), Nat.below t → ?motive t",
-        s!"?motive ?m.{majorId} = (n + 0 = n)",
-      ]))
-    let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number"
-    addTest $ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
-
-    -- Assign motive to `λ x => x + _`
-    let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
-    motive.assign motive_assign
-
-    addTest $ ← conduit.withContext do
-      let t := toString (← Meta.ppExpr $ ← conduit.getType)
-      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) :=
-  [
-    ("type_extract", test_type_extract),
-    ("Nat.brecOn", test_nat_brec_on),
-    ("List.brecOn", test_list_brec_on),
-    ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation),
-  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
-
-end Pantograph.Test.Tactic.MotivatedApply

Test/Tactic/NoConfuse.lean

@@ -1,72 +0,0 @@
-import LSpec
-import Lean
-import Test.Common
-
-open Lean
-open Pantograph
-
-namespace Pantograph.Test.Tactic.NoConfuse
-
-def test_nat : TestT Elab.TermElabM Unit := do
-  let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
-  let expr ← parseSentence expr
-  Meta.lambdaTelescope expr $ λ _ body => do
-    let recursor ← match Parser.runParserCategory
-      (env := ← MonadEnv.getEnv)
-      (catName := `term)
-      (input := "h")
-      (fileName := filename) with
-      | .ok syn => pure syn
-      | .error error => throwError "Failed to parse: {error}"
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.evalNoConfuse recursor
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
-
-def test_nat_fail : TestT Elab.TermElabM Unit := do
-  let expr := "λ (n: Nat) (h: n = n) => False"
-  let expr ← parseSentence expr
-  Meta.lambdaTelescope expr $ λ _ body => do
-    let recursor ← match Parser.runParserCategory
-      (env := ← MonadEnv.getEnv)
-      (catName := `term)
-      (input := "h")
-      (fileName := filename) with
-      | .ok syn => pure syn
-      | .error error => throwError "Failed to parse: {error}"
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    try
-      let tactic := Tactic.evalNoConfuse recursor
-      let _ ← runTacticOnMVar tactic target.mvarId!
-      addTest $ assertUnreachable "Tactic should fail"
-    catch _ =>
-      addTest $ LSpec.check "Tactic should fail" true
-
-def test_list : TestT Elab.TermElabM Unit := do
-  let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
-  let expr ← parseSentence expr
-  Meta.lambdaTelescope expr $ λ _ body => do
-    let recursor ← match Parser.runParserCategory
-      (env := ← MonadEnv.getEnv)
-      (catName := `term)
-      (input := "h")
-      (fileName := filename) with
-      | .ok syn => pure syn
-      | .error error => throwError "Failed to parse: {error}"
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.evalNoConfuse recursor
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    addTest $ LSpec.check "goals"
-      ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
-
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("Nat", test_nat),
-    ("Nat fail", test_nat_fail),
-    ("List", test_list),
-  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
-
-end Pantograph.Test.Tactic.NoConfuse

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 := filename) with
+      (fileName := ← getFileName) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -87,7 +87,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
         { userName := "q", type? := .some { pp? := .some "Prop" } },
         { userName := "h", type? := .some { pp? := .some "p" } },
         { userName := "y",
-          type? := .some { pp? := .some "p ∨ ?m.25" },
+          type? := .some { pp? := .some "p ∨ ?m.19" },
           value? := .some { pp? := .some "Or.inl h" },
         }
       ]

doc/icon.svg

@@ -4,17 +4,17 @@
 <svg
    width="256"
    height="256"
-   viewBox="0 0 55.900957 55.900957"
+   viewBox="0 0 67.733332 67.733333"
    version="1.1"
-   id="svg21534"
-   xml:space="preserve"
-   inkscape:version="1.2.2 (b0a8486541, 2022-12-01)"
+   id="svg1"
    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="namedview21536"
+   xmlns:svg="http://www.w3.org/2000/svg">
+  <sodipodi:namedview
+     id="namedview1"
      pagecolor="#ffffff"
      bordercolor="#111111"
      borderopacity="1"
@@ -23,51 +23,135 @@
      inkscape:pagecheckerboard="1"
      inkscape:deskcolor="#d1d1d1"
      inkscape:document-units="px"
-     showgrid="true"
-     inkscape:zoom="5.1754899"
-     inkscape:cx="158.82554"
-     inkscape:cy="91.682142"
-     inkscape:window-width="3777"
-     inkscape:window-height="2093"
+     showguides="true"
+     inkscape:zoom="5.1882633"
+     inkscape:cx="81.819286"
+     inkscape:cy="132.22151"
+     inkscape:window-width="3774"
+     inkscape:window-height="2126"
      inkscape:window-x="0"
      inkscape:window-y="0"
      inkscape:window-maximized="1"
-     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: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:groupmode="layer"
-     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>
+     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>

doc/rationale.md

@@ -0,0 +1,59 @@
+# 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

@@ -11,8 +11,10 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
 * `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 }`, `env.load { path }`: Save/Load the current environment
-  to/from a file
+* `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the
+  current environment to/from a file
+* `env.module_read { "module": <name }`: Reads a list of symbols from a module
+* `env.describe {}`: Describes the imports and modules in the current environment
 * `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`
 
@@ -20,6 +22,9 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   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.
+
+  Set `timeout` to a non-zero number to specify timeout (milliseconds) for all `CoreM`
+  operations.
 * `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
@@ -33,19 +38,26 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
     to the previous `rhs`.
   - `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
     exit, the goal id is ignored.
+  - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
   Execute continuation/resumption
   - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.
   - `{ "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, path }`, `goal.load { path }`: 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> }`: Executes the Lean frontend on a file, collecting
-  either the tactic invocations (`"invocations": true`) or the sorrys into goal
-  states (`"sorrys": true`)
+* `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>], readHeader: <bool>, inheritEnv: <bool>, 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`. Conditionally inherit the environment from executing the file.
+  Warning: Behaviour is unstable in case of multiple `sorry`s. Use the draft
+  tactic if possible.
 
 ## Errors
 

flake.lock

@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1730504689,
-        "narHash": "sha256-hgmguH29K2fvs9szpq2r3pz2/8cJd2LPS+b4tfNFCwE=",
+        "lastModified": 1743550720,
+        "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "506278e768c2a08bec68eb62932193e341f55c90",
+        "rev": "c621e8422220273271f52058f618c94e405bb0f5",
         "type": "github"
       },
       "original": {
@@ -39,14 +39,16 @@
     "lean4-nix": {
       "inputs": {
         "flake-parts": "flake-parts_2",
-        "nixpkgs": "nixpkgs"
+        "nixpkgs": [
+          "nixpkgs"
+        ]
       },
       "locked": {
-        "lastModified": 1731711316,
-        "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
+        "lastModified": 1743534244,
+        "narHash": "sha256-WnoYs2iyrfgh35eXErCOyos8E2YbW3LT1xm/EtT88/k=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "136fc6057c48de970579e960b62421e9c295b67d",
+        "rev": "5eb7f03be257e327fdb3cca9465392e68dc28a4d",
         "type": "github"
       },
       "original": {
@@ -55,49 +57,35 @@
         "type": "github"
       }
     },
-    "lspec": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1728279187,
-        "narHash": "sha256-ZMqbvCqR/gHXRuIkuo7b0Yp9N1vOQR7xnrcy/SeIBoQ=",
-        "owner": "argumentcomputer",
-        "repo": "LSpec",
-        "rev": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
-        "type": "github"
-      },
-      "original": {
-        "owner": "argumentcomputer",
-        "ref": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
-        "repo": "LSpec",
-        "type": "github"
-      }
-    },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1728500571,
-        "narHash": "sha256-dOymOQ3AfNI4Z337yEwHGohrVQb4yPODCW9MDUyAc4w=",
+        "lastModified": 1743975612,
+        "narHash": "sha256-o4FjFOUmjSRMK7dn0TFdAT0RRWUWD+WsspPHa+qEQT8=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "d51c28603def282a24fa034bcb007e2bcb5b5dd0",
+        "rev": "a880f49904d68b5e53338d1e8c7bf80f59903928",
         "type": "github"
       },
       "original": {
         "owner": "nixos",
-        "ref": "nixos-24.05",
+        "ref": "nixos-24.11",
         "repo": "nixpkgs",
         "type": "github"
       }
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1730504152,
-        "narHash": "sha256-lXvH/vOfb4aGYyvFmZK/HlsNsr/0CVWlwYvo2rxJk3s=",
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
+        "lastModified": 1743296961,
+        "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=",
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa",
+        "type": "github"
       },
       "original": {
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "type": "github"
       }
     },
     "nixpkgs-lib_2": {
@@ -112,28 +100,11 @@
         "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
       }
     },
-    "nixpkgs_2": {
-      "locked": {
-        "lastModified": 1731386116,
-        "narHash": "sha256-lKA770aUmjPHdTaJWnP3yQ9OI1TigenUqVC3wweqZuI=",
-        "owner": "nixos",
-        "repo": "nixpkgs",
-        "rev": "689fed12a013f56d4c4d3f612489634267d86529",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nixos",
-        "ref": "nixos-24.05",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
     "root": {
       "inputs": {
         "flake-parts": "flake-parts",
         "lean4-nix": "lean4-nix",
-        "lspec": "lspec",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs"
       }
     }
   },

flake.nix

@@ -2,12 +2,11 @@
   description = "Pantograph";
 
   inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix.url = "github:lenianiva/lean4-nix";
-    lspec = {
-      url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
-      flake = false;
+    lean4-nix = {
+      url = "github:lenianiva/lean4-nix";
+      inputs.nixpkgs.follows = "nixpkgs";
     };
   };
 
@@ -16,82 +15,111 @@
     nixpkgs,
     flake-parts,
     lean4-nix,
-    lspec,
     ...
-  } : 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) ];
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      flake = {
       };
-      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 ];
+      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)];
+        };
+        manifest = pkgs.lib.importJSON ./lake-manifest.json;
+        manifest-lspec = builtins.head manifest.packages;
+        lspecLib = pkgs.lean.buildLeanPackage {
+          name = "LSpec";
+          roots = ["LSpec"];
+          src = builtins.fetchGit {inherit (manifest-lspec) url rev;};
+        };
+        inherit (pkgs.lib.fileset) unions toSource fileFilter;
+        src = ./.;
+        set-project = unions [
+          ./Pantograph.lean
+          (fileFilter (file: file.hasExt "lean") ./Pantograph)
+        ];
+        set-repl = unions [
+          ./Main.lean
+          ./Repl.lean
+        ];
+        set-test = unions [
+          (fileFilter (file: file.hasExt "lean") ./Test)
+        ];
+        src-project = toSource {
+          root = src;
+          fileset = unions [
+            set-project
+          ];
+        };
+        src-repl = toSource {
+          root = src;
+          fileset = unions [
+            set-project
+            set-repl
+          ];
+        };
+        src-test = toSource {
+          root = src;
+          fileset = unions [
+            set-project
+            set-repl
+            set-test
+          ];
+        };
+        project = pkgs.lean.buildLeanPackage {
+          name = "Pantograph";
+          roots = ["Pantograph"];
+          src = src-project;
+        };
+        repl = pkgs.lean.buildLeanPackage {
+          name = "Repl";
+          roots = ["Main" "Repl"];
+          deps = [project];
+          src = src-repl;
+        };
+        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 = src-test;
+        };
+      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];
+        };
       };
     };
-  };
 }

lake-manifest.json

@@ -1,15 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/lenianiva/LSpec.git",
+ [{"url": "https://github.com/argumentcomputer/LSpec.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
+   "rev": "a6652a48b5c67b0d8dd3930fad6390a97d127e8d",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
+   "inputRev": "a6652a48b5c67b0d8dd3930fad6390a97d127e8d",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.toml"}],
  "name": "pantograph",
  "lakeDir": ".lake"}

lakefile.lean

@@ -18,7 +18,7 @@ lean_exe repl {
 }
 
 require LSpec from git
-  "https://github.com/lenianiva/LSpec.git" @ "c492cecd0bc473e2f9c8b94d545d02cc0056034f"
+  "https://github.com/argumentcomputer/LSpec.git" @ "a6652a48b5c67b0d8dd3930fad6390a97d127e8d"
 lean_lib Test {
 }
 @[test_driver]

lean-toolchain

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