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

Reviewed-on: #185

.gitignore

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

LICENSE

@@ -0,0 +1,190 @@
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   Copyright 2024 Leni Aniva
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.

Main.lean

@@ -1,4 +1,70 @@
-import Pantograph
+import Lean.Data.Json
+import Lean.Environment
 
-def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
+import Pantograph
+import Repl
+
+-- Main IO functions
+open Pantograph.Repl
+open Pantograph.Protocol
+
+/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
+def parseCommand (s: String): Except String Command := do
+  match s.trim.get? 0 with
+  | .some '{' =>
+    -- Parse in Json mode
+    Lean.fromJson? (← Lean.Json.parse s)
+  | .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"
+
+partial def loop : MainM Unit := do repeat do
+  let state ← get
+  let command ← (← IO.getStdin).getLine
+  -- 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)
+    -- Using `Lean.Json.compress` here to prevent newline
+    IO.println error.compress
+  | .ok command =>
+    try
+      let ret ← execute command
+      let str := match state.options.printJsonPretty with
+        | true => ret.pretty
+        | false => ret.compress
+      IO.println str
+    catch e =>
+      let message := e.toString
+      let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
+      IO.println error.compress
+
+
+unsafe def main (args: List String): IO Unit := do
+  -- NOTE: A more sophisticated scheme of command line argument handling is needed.
+  if args == ["--version"] then do
+    IO.println s!"{Pantograph.version}"
+    return
+
+  Pantograph.initSearch ""
+
+  -- 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
+  try
+    let mainM := loop.run { coreContext } |>.run' { env := coreState.env }
+    IO.println "ready."
+    mainM
+  catch ex =>
+    let message := ex.toString
+    let error  := Lean.toJson ({ error := "io", desc := message }: InteractionError)
+    IO.println error.compress

Pantograph.lean

@@ -1 +1,9 @@
-def hello := "world"
+import Pantograph.Delate
+import Pantograph.Elab
+import Pantograph.Environment
+import Pantograph.Frontend
+import Pantograph.Goal
+import Pantograph.Library
+import Pantograph.Protocol
+import Pantograph.Serial
+import Pantograph.Version

Pantograph/Delate.lean

@@ -0,0 +1,611 @@
+/-
+This file handles "Delation": The conversion of Kernel view into Search view.
+-/
+import Lean
+import Std.Data.HashMap
+import Pantograph.Goal
+import Pantograph.Protocol
+
+open Lean
+
+-- Symbol processing functions --
+
+namespace Pantograph
+
+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) : 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_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
+instantiated. This is used during resumption to provide diagnostic data about
+the current goal.
+
+Since Lean 4 does not have an `Expr` constructor corresponding to delayed
+metavariables, any delayed metavariables must be recursively handled by this
+function to ensure that nested delayed metavariables can be properly processed.
+The caveat is this recursive call will lead to infinite recursion if a loop
+between metavariable assignment exists.
+
+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 (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
+
+    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
+        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 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
+
+        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
+
+/--
+Convert an expression to an equiavlent form with
+1. No nested delayed assigned mvars
+2. No aux lemmas or matchers
+3. No assigned mvars
+ -/
+@[export pantograph_instantiate_all_m]
+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))
+  -- Extra arguments applied to the result of this substitution
+  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]
+def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
+  let .mvar mvarId := e.getAppFn | return .none
+  let .some decl ← getDelayedMVarAssignment? mvarId | return .none
+  let mvarIdPending := decl.mvarIdPending
+  let mvarDecl ← mvarIdPending.getDecl
+  -- Print the function application e. See Lean's `withOverApp`
+  let args := e.getAppArgs
+
+  assert! args.size ≥ decl.fvars.size
+  assert! !(← mvarIdPending.isAssigned)
+  assert! !(← mvarIdPending.isDelayedAssigned)
+  let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
+  let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
+    let fvarId := localDecl.fvarId
+    let a := fvarArgMap[fvarId]?
+    return acc ++ [(fvarId, a)]
+
+  assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
+
+  return .some {
+    mvarIdPending,
+    args := subst.toArray,
+    tail := args.toList.drop decl.fvars.size |>.toArray,
+  }
+
+-- Condensed representation
+
+namespace Condensed
+
+-- Mirrors Lean's LocalDecl
+structure LocalDecl where
+  -- Default value is for testing
+  fvarId: FVarId := { name := .anonymous }
+  userName: Name
+
+  -- Normalized expression
+  type : Expr
+  value? : Option Expr := .none
+
+structure Goal where
+  mvarId: MVarId := { name := .anonymous }
+  userName: Name := .anonymous
+  context: Array LocalDecl
+  target: Expr
+
+@[export pantograph_goal_is_lhs]
+def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
+
+end Condensed
+
+-- Get the list of visible (by default) free variables from a goal
+@[export pantograph_visible_fvars_of_mvar]
+protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
+  let mvarDecl ← mctx.findDecl? mvarId
+  let lctx := mvarDecl.lctx
+  return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
+    | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
+    | none      => r
+
+@[export pantograph_to_condensed_goal_m]
+def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
+  let ppAuxDecls     := Meta.pp.auxDecls.get (← getOptions)
+  let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
+  let mvarDecl ← mvarId.getDecl
+  let lctx     := mvarDecl.lctx
+  let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
+  Meta.withLCtx lctx mvarDecl.localInstances do
+    let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
+      match localDecl with
+      | .cdecl _ fvarId userName type _ _ =>
+        let type ← instantiate type
+        return { fvarId, userName, type }
+      | .ldecl _ fvarId userName type value _ _ => do
+        let userName := userName.simpMacroScopes
+        let type ← instantiate type
+        let value ← instantiate value
+        return { fvarId, userName, type, value? := .some value }
+    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
+      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
+        !ppImplDetailHyps && localDecl.isImplementationDetail
+      if skip then
+        return acc
+      else
+        let var ← ppVar localDecl
+        return var::acc
+    return {
+        mvarId,
+        userName := mvarDecl.userName,
+        context := vars.reverse.toArray,
+        target := ← instantiate mvarDecl.type
+    }
+  where
+  instantiate := instantiateAll
+
+@[export pantograph_goal_state_to_condensed_m]
+protected def GoalState.toCondensed (state: GoalState):
+    CoreM (Array Condensed.Goal):= do
+  let metaM := do
+    let goals := state.goals.toArray
+    goals.mapM fun goal => do
+      match state.mctx.findDecl? goal with
+      | .some _ =>
+        let serializedGoal ← toCondensedGoal goal
+        pure serializedGoal
+      | .none => throwError s!"Metavariable does not exist in context {goal.name}"
+  metaM.run' (s := state.savedState.term.meta.meta)
+
+def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
+  Meta.forallTelescope expr fun arr body => do
+    let binders ← arr.mapM fun fvar => do
+      return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
+    return { binders, target := toString (← Meta.ppExpr body) }
+
+def serializeName (name: Name) (sanitize: Bool := true): String :=
+  let internal := name.isInaccessibleUserName || name.hasMacroScopes
+  if sanitize && internal then "_"
+  else toString name |> addQuotes
+  where
+  addQuotes (n: String) :=
+    let quote := "\""
+    if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
+
+/-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
+partial def serializeSortLevel (level: Level) : String :=
+  let k := level.getOffset
+  let u := level.getLevelOffset
+  let u_str := match u with
+    | .zero => "0"
+    | .succ _ => panic! "getLevelOffset should not return .succ"
+    | .max v w =>
+      let v := serializeSortLevel v
+      let w := serializeSortLevel w
+      s!"(:max {v} {w})"
+    | .imax v w =>
+      let v := serializeSortLevel v
+      let w := serializeSortLevel w
+      s!"(:imax {v} {w})"
+    | .param name =>
+      s!"{name}"
+    | .mvar id =>
+      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) : MetaM String := do
+  self expr
+  where
+  delayedMVarToSexp (e: Expr): MetaM (Option String) := do
+    let .some invocation ← toDelayedMVarInvocation e | return .none
+    let callee ← self $ .mvar invocation.mvarIdPending
+    let sites ← invocation.args.mapM (λ (fvarId, arg) => do
+        let arg := match arg with
+          | .some arg => arg
+          | .none => .fvar fvarId
+        self arg
+      )
+    let tailArgs ← invocation.tail.mapM self
+
+    let sites := " ".intercalate sites.toList
+    let result := if tailArgs.isEmpty then
+        s!"(:subst {callee} {sites})"
+      else
+        let tailArgs := " ".intercalate tailArgs.toList
+        s!"((:subst {callee} {sites}) {tailArgs})"
+    return .some result
+
+  self (e: Expr): MetaM String := do
+    if let .some result ← delayedMVarToSexp e then
+      return result
+    match e with
+    | .bvar deBruijnIndex =>
+      -- This is very common so the index alone is shown. Literals are handled below.
+      -- The raw de Bruijn index should never appear in an unbound setting. In
+      -- Lean these are handled using a `#` prefix.
+      pure s!"{deBruijnIndex}"
+    | .fvar fvarId =>
+      let name := fvarId.name
+      pure s!"(:fv {name})"
+    | .mvar mvarId => do
+        let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
+        let name := mvarId.name
+        pure s!"(:{pref} {name})"
+    | .sort level =>
+      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})"
+    | .app _ _ => do
+      let fn' ← self e.getAppFn
+      let args := (← e.getAppArgs.mapM self) |>.toList
+      let args := " ".intercalate args
+      pure s!"({fn'} {args})"
+    | .lam binderName binderType body binderInfo => do
+      let binderName' := binderName.eraseMacroScopes
+      let binderType' ← self binderType
+      let body' ← self body
+      let binderInfo' := binderInfoSexp binderInfo
+      pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
+    | .forallE binderName binderType body binderInfo => do
+      let binderName' := binderName.eraseMacroScopes
+      let binderType' ← self binderType
+      let body' ← self body
+      let binderInfo' := binderInfoSexp binderInfo
+      pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
+    | .letE name type value body _ => do
+      -- Dependent boolean flag diacarded
+      let name' := name.eraseMacroScopes
+      let type' ← self type
+      let value' ← self value
+      let body' ← self body
+      pure s!"(:let {name'} {type'} {value'} {body'})"
+    | .lit v =>
+      -- To not burden the downstream parser who needs to handle this, the literal
+      -- is wrapped in a :lit sexp.
+      let v' := match v with
+        | .natVal val => toString 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 typeName idx inner => do
+      let env ← getEnv
+      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 => " :i"
+    | .strictImplicit => " :si"
+    | .instImplicit => " :ii"
+
+def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
+  let pp?: Option String ← match options.printExprPretty with
+    | true => pure $ .some $ toString $ ← Meta.ppExpr e
+    | false => pure $ .none
+  let sexp?: Option String ← match options.printExprAST with
+    | true => pure $ .some $ ← serializeExpressionSexp e
+    | false => pure $ .none
+  let dependentMVars? ← match options.printDependentMVars with
+    | true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
+    | false => pure $ .none
+  return {
+    pp?,
+    sexp?
+    dependentMVars?,
+  }
+
+
+/-- Adapted from ppGoal -/
+def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
+      : MetaM Protocol.Goal := do
+  -- Options for printing; See Meta.ppGoal for details
+  let showLetValues  := true
+  let ppAuxDecls     := options.printAuxDecls
+  let ppImplDetailHyps := options.printImplementationDetailHyps
+  let lctx           := mvarDecl.lctx
+  let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
+  Meta.withLCtx lctx mvarDecl.localInstances do
+    let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
+      match localDecl with
+      | .cdecl _ fvarId userName _ _ _ =>
+        return {
+          name := fvarId.name.toString,
+          userName:= ofName userName.simpMacroScopes,
+          isInaccessible := userName.isInaccessibleUserName
+        }
+      | .ldecl _ fvarId userName _ _ _ _ => do
+        return {
+          name := fvarId.name.toString,
+          userName := toString userName.simpMacroScopes,
+          isInaccessible := userName.isInaccessibleUserName
+        }
+    let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
+      match localDecl with
+      | .cdecl _ fvarId userName type _ _ =>
+        let userName := userName.simpMacroScopes
+        let type ← instantiate type
+        return {
+          name := fvarId.name.toString,
+          userName:= ofName userName,
+          isInaccessible := userName.isInaccessibleUserName
+          type? := .some (← serializeExpression options type)
+        }
+      | .ldecl _ fvarId userName type val _ _ => do
+        let userName := userName.simpMacroScopes
+        let type ← instantiate type
+        let value? ← if showLetValues then
+          let val ← instantiate val
+          pure $ .some (← serializeExpression options val)
+        else
+          pure $ .none
+        return {
+          name := fvarId.name.toString,
+          userName:= ofName userName,
+          isInaccessible := userName.isInaccessibleUserName
+          type? := .some (← serializeExpression options type)
+          value? := value?
+        }
+    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
+      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
+        !ppImplDetailHyps && localDecl.isImplementationDetail
+      if skip then
+        return acc
+      else
+        let nameOnly := options.noRepeat && (parentDecl?.map
+          (λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
+        let var ← match nameOnly with
+          | true => ppVarNameOnly localDecl
+          | false => ppVar localDecl
+        return var::acc
+    return {
+      name := goal.name.toString,
+      userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
+      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
+      target := (← serializeExpression options (← instantiate mvarDecl.type)),
+      vars := vars.reverse.toArray
+    }
+  where
+  instantiate := instantiateAll
+  ofName (n: Name) := serializeName n (sanitize := false)
+
+protected def GoalState.serializeGoals
+      (state: GoalState)
+      (parent: Option GoalState := .none)
+      (options: @&Protocol.Options := {}):
+    MetaM (Array Protocol.Goal):= do
+  state.restoreMetaM
+  let goals := state.goals.toArray
+  let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
+  goals.mapM fun goal => do
+    match state.mctx.findDecl? goal with
+    | .some mvarDecl =>
+      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
+      pure serializedGoal
+    | .none => throwError s!"Metavariable does not exist in context {goal.name}"
+
+/-- Print the metavariables in a readable format -/
+@[export pantograph_goal_state_diag_m]
+protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
+  let metaM: MetaM String := do
+    goalState.restoreMetaM
+    let savedState := goalState.savedState
+    let goals := savedState.tactic.goals
+    let mctx ← getMCtx
+    let root := goalState.root
+    -- Print the root
+    let result: String ← match mctx.decls.find? root with
+      | .some decl => printMVar ">" root decl
+      | .none => pure s!">{root.name}: ??"
+    let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
+      match mctx.decls.find? mvarId with
+      | .some decl => printMVar "⊢" mvarId decl
+      | .none => pure s!"⊢{mvarId.name}: ??"
+    )
+    let goals := goals.toSSet
+    let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
+        !(goals.contains mvarId || mvarId == root) && options.printAll)
+        |>.mapM (fun (mvarId, decl) => do
+          let pref := if parentHasMVar mvarId then " " else "~"
+          printMVar pref mvarId decl
+        )
+    pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
+  metaM.run' {}
+  where
+    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
+      let resultFVars: List String ←
+        if options.printContext then
+          decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
+            do pure $ (← printFVar fvarId decl) ++ "\n")
+        else
+          pure []
+      let type ← if options.instantiate
+        then instantiateAll decl.type
+        else pure $ decl.type
+      let type_sexp ← if options.printSexp then
+          let sexp ← serializeExpressionSexp type
+          pure <| " " ++ sexp
+        else
+          pure ""
+      let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
+      let resultValue: String ←
+        if options.printValue then
+          if let .some value ← getExprMVarAssignment? mvarId then
+            let value ← if options.instantiate
+              then instantiateAll value
+              else pure $ value
+            pure s!"\n := {← Meta.ppExpr value}"
+          else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
+            pure s!"\n ::= {mvarIdPending.name}"
+          else
+            pure ""
+        else
+          pure ""
+      pure $ (String.join resultFVars) ++ resultMain ++ resultValue
+    printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do
+      pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
+    userNameToString : Name → String
+      | .anonymous => ""
+      | 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

@@ -0,0 +1,41 @@
+import Lean
+open Lean
+
+namespace Pantograph
+
+-- Functions for creating contexts and states
+@[export pantograph_default_elab_context]
+def defaultElabContext: Elab.Term.Context := {
+    declName? := .some `mystery,
+    errToSorry := false,
+  }
+
+/-- Read syntax object from string -/
+def parseTerm (env: Environment) (s: String): Except String Syntax :=
+  Parser.runParserCategory
+    (env := env)
+    (catName := `term)
+    (input := s)
+    (fileName := "<stdin>")
+
+def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
+  return Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := s)
+    (fileName := "<stdin>")
+
+/-- Parse a syntax object. May generate additional metavariables! -/
+def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
+  try
+    let expr ← Elab.Term.elabType syn
+    return .ok expr
+  catch ex => return .error (← ex.toMessageData.toString)
+def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
+  try
+    let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
+    return .ok expr
+  catch ex => return .error (← ex.toMessageData.toString)
+
+
+end Pantograph

Pantograph/Environment.lean

@@ -0,0 +1,198 @@
+import Pantograph.Delate
+import Pantograph.Elab
+import Pantograph.Protocol
+import Pantograph.Serial
+import Lean.Environment
+import Lean.Replay
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Environment
+
+@[export pantograph_is_name_internal]
+def isNameInternal (n: Name): Bool :=
+  -- Returns true if the name is an implementation detail which should not be shown to the user.
+  n.isAuxLemma ∨ n.hasMacroScopes
+
+/-- Catalog all the non-internal and safe names -/
+@[export pantograph_environment_catalog]
+def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ =>
+  match isNameInternal name with
+  | false => acc.push name
+  | true => acc)
+
+@[export pantograph_environment_module_of_name]
+def module_of_name (env: Environment) (name: Name): Option Name := do
+  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
+  | .axiomInfo  _ => "a"
+  | .defnInfo   _ => "d"
+  | .thmInfo    _ => "t"
+  | .opaqueInfo _ => "o"
+  | .quotInfo   _ => "q"
+  | .inductInfo _ => "i"
+  | .ctorInfo   _ => "c"
+  | .recInfo    _ => "r"
+  s!"{pref}{toString n}"
+
+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 =>
+    match toFilteredSymbol name info with
+    | .some x => acc.push x
+    | .none => acc)
+  return { symbols := names }
+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 .some info := info? | Protocol.throw $ Protocol.errorIndex s!"Symbol not found {args.name}"
+  let module? := env.getModuleIdxFor? name >>=
+    (λ idx => env.allImportedModuleNames[idx.toNat]?)
+  let value? := match args.value?, info with
+    | .some true, _ => info.value?
+    | .some false, _ => .none
+    | .none, .defnInfo _ => info.value?
+    | .none, _ => .none
+  let type ← unfoldAuxLemmas info.type
+  let value? ← value?.mapM (λ v => unfoldAuxLemmas v)
+  -- Information common to all symbols
+  let core := {
+    type := ← (serializeExpression options type).run',
+    isUnsafe := info.isUnsafe,
+    value? := ← value?.mapM (λ v => serializeExpression options v |>.run'),
+    publicName? := Lean.privateToUserName? name |>.map (·.toString),
+    typeDependency? := if args.dependency?.getD false
+      then .some <| type.getUsedConstants.map (λ n => serializeName n)
+      else .none,
+    valueDependency? := if args.dependency?.getD false
+      then value?.map (λ e =>
+        e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
+      else .none,
+    module? := module?.map (·.toString)
+  }
+  let result ← match info with
+    | .inductInfo induct => pure { core with inductInfo? := .some {
+          numParams := induct.numParams,
+          numIndices := induct.numIndices,
+          all := induct.all.toArray.map (·.toString),
+          ctors := induct.ctors.toArray.map (·.toString),
+          isRec := induct.isRec,
+          isReflexive := induct.isReflexive,
+          isNested := induct.isNested,
+      } }
+    | .ctorInfo ctor => pure { core with constructorInfo? := .some {
+          induct := ctor.induct.toString,
+          cidx := ctor.cidx,
+          numParams := ctor.numParams,
+          numFields := ctor.numFields,
+      } }
+    | .recInfo r => pure { core with recursorInfo? := .some {
+          all := r.all.toArray.map (·.toString),
+          numParams := r.numParams,
+          numIndices := r.numIndices,
+          numMotives := r.numMotives,
+          numMinors := r.numMinors,
+          rules := ← r.rules.toArray.mapM (λ rule => do
+              pure {
+                ctor := rule.ctor.toString,
+                nFields := rule.nfields,
+                rhs := ← (serializeExpression options rule.rhs).run',
+              })
+          k := r.k,
+      } }
+    | _ => pure core
+  let result ← if args.source?.getD false then
+      let srcSearchPath ← initSrcSearchPath
+      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
+      let declRange? ← findDeclarationRanges? name
+      let sourceStart? := declRange?.map (·.range.pos)
+      let sourceEnd? := declRange?.map (·.range.endPos)
+      .pure {
+        result with
+        sourceUri?,
+        sourceStart?,
+        sourceEnd?,
+      }
+    else
+      .pure result
+  return 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 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 value with
+      | .ok syn => do
+        try
+          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
+    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 => 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

@@ -0,0 +1,4 @@
+import Pantograph.Frontend.Basic
+import Pantograph.Frontend.Elab
+import Pantograph.Frontend.InfoTree
+import Pantograph.Frontend.MetaTranslate

Pantograph/Frontend/Basic.lean

@@ -0,0 +1,128 @@
+import Lean.Parser
+import Lean.Elab.Frontend
+
+open Lean
+
+namespace Lean.FileMap
+
+/-- Extract the range of a `Syntax` expressed as lines and columns. -/
+-- Extracted from the private declaration `Lean.Elab.formatStxRange`,
+-- in `Lean.Elab.InfoTree.Main`.
+@[export pantograph_frontend_stx_range]
+protected def stxRange (fileMap : FileMap) (stx : Syntax) : Position × Position :=
+  let pos    := stx.getPos?.getD 0
+  let endPos := stx.getTailPos?.getD pos
+  (fileMap.toPosition pos, fileMap.toPosition endPos)
+
+end Lean.FileMap
+namespace Lean.PersistentArray
+
+/--
+Drop the first `n` elements of a `PersistentArray`, returning the results as a `List`.
+-/
+-- We can't remove the `[Inhabited α]` hypotheses here until
+-- `PersistentArray`'s `GetElem` instance also does.
+protected def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α :=
+  List.range (t.size - n) |>.map fun i => t.get! (n + i)
+
+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
+  stx : Syntax
+  before : Environment
+  after : Environment
+  msgs : List Message
+  trees : List Elab.InfoTree
+
+namespace CompilationStep
+
+@[export pantograph_frontend_compilation_step_message_strings_m]
+def messageStrings (step: CompilationStep) : IO (Array String) := do
+  List.toArray <$> step.msgs.mapM (·.toString)
+
+end CompilationStep
+
+
+/--
+Process one command, returning a `CompilationStep` and
+`done : Bool`, indicating whether this was the last command.
+-/
+@[export pantograph_frontend_process_one_command_m]
+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 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 ({ 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
+  if done then
+    if cmd.src.isEmpty then
+      return []
+    else
+      return [← f cmd]
+  else
+    return (← f cmd) :: (← mapCompilationSteps f)
+
+
+@[export pantograph_frontend_find_source_path_m]
+def findSourcePath (module : Name) : IO System.FilePath := do
+  return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean"
+
+/--
+Use with
+```lean
+let m: FrontendM α := ...
+let (context, state) ← createContextStateFromFile ...
+m.run context |>.run' state
+```
+-/
+@[export pantograph_frontend_create_context_state_from_file_m]
+def createContextStateFromFile
+    (file : String) -- Content of the file
+    (fileName : String := "<anonymous>")
+    (env? : Option Lean.Environment := .none) -- If set to true, assume there's no header.
+    (opts : Options := {})
+    : IO (Elab.Frontend.Context × Elab.Frontend.State) := unsafe do
+  --let file ← IO.FS.readFile (← findSourcePath module)
+  let inputCtx := Parser.mkInputContext file fileName
+
+  let (env, parserState, messages) ← match env? with
+    | .some env => pure (env, {}, .empty)
+    | .none =>
+      let (header, parserState, messages) ← Parser.parseHeader inputCtx
+      let (env, messages) ← Elab.processHeader header opts messages inputCtx
+      pure (env, parserState, messages)
+  let commandState := Elab.Command.mkState env messages opts
+  let context: Elab.Frontend.Context := { inputCtx }
+  let state: Elab.Frontend.State := {
+    commandState := { commandState with infoState.enabled := true },
+    parserState,
+    cmdPos := parserState.pos
+  }
+  return (context, state)
+
+end Pantograph.Frontend

Pantograph/Frontend/Elab.lean

@@ -0,0 +1,199 @@
+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 Pantograph.Frontend
+
+-- Info tree filtering functions
+
+/- Adapted from lean-training-data -/
+structure TacticInvocation where
+  info : Elab.TacticInfo
+  ctx : Elab.ContextInfo
+  children : PersistentArray Elab.InfoTree
+namespace TacticInvocation
+
+/-- Return the range of the tactic, as a pair of file positions. -/
+@[export pantograph_frontend_tactic_invocation_range]
+protected def range (t : TacticInvocation) : Position × Position := t.ctx.fileMap.stxRange t.info.stx
+
+/-- Pretty print a tactic. -/
+protected def pp (t : TacticInvocation) : IO Format :=
+  t.ctx.runMetaM {} try
+    Lean.PrettyPrinter.ppTactic ⟨t.info.stx⟩
+  catch _ =>
+    pure "<failed to pretty print>"
+
+/-- Run a tactic on the goals stored in a `TacticInvocation`. -/
+protected def runMetaMGoalsBefore (t : TacticInvocation) (x : List MVarId → MetaM α) : IO α := do
+  t.ctx.runMetaM {} <| Meta.withMCtx t.info.mctxBefore <| x t.info.goalsBefore
+
+/-- Run a tactic on the after goals stored in a `TacticInvocation`. -/
+protected def runMetaMGoalsAfter (t : TacticInvocation) (x : List MVarId → MetaM α) : IO α := do
+  t.ctx.runMetaM {} <| Meta.withMCtx t.info.mctxAfter <| x t.info.goalsAfter
+
+/-- Run a tactic on the main goal stored in a `TacticInvocation`. -/
+protected def runMetaM (t : TacticInvocation) (x : MVarId → MetaM α) : IO α := do
+  match t.info.goalsBefore.head? with
+  | none => throw <| IO.userError s!"No goals at {← t.pp}"
+  | some g => t.runMetaMGoalsBefore fun _ => do g.withContext <| x g
+
+protected def goalState (t : TacticInvocation) : IO (List Format) := do
+  t.runMetaMGoalsBefore (fun gs => gs.mapM fun g => do Meta.ppGoal g)
+
+protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
+  t.runMetaMGoalsAfter (fun gs => gs.mapM fun g => do Meta.ppGoal g)
+
+protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
+  t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
+
+protected def usedConstants (t: TacticInvocation) : NameSet :=
+  let info := t.info
+  info.goalsBefore
+    |>.filterMap info.mctxAfter.getExprAssignmentCore?
+    |>.map Expr.getUsedConstantsAsSet
+    |>.foldl .union .empty
+
+end TacticInvocation
+
+/-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
+each equipped with its relevant `ContextInfo`, and any children info trees. -/
+private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
+  let infos := t.findAllInfo none false fun i => match i with
+    | .ofTacticInfo _ => true
+    | _ => false
+  infos.filterMap fun p => match p with
+    | (.ofTacticInfo i, some ctx, children) => .some ⟨i, ctx, children⟩
+    | _ => none
+
+def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
+  collectTacticNodes t |>.filter fun i => i.info.isSubstantive
+
+@[export pantograph_frontend_collect_tactics_from_compilation_step_m]
+def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
+  let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ
+    | info@(.ofTacticInfo _) => info.isOriginal
+    | _ => false
+  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 {} <| 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,
+      goalAfter,
+      tactic,
+      usedConstants,
+    }
+
+structure InfoWithContext where
+  info: Elab.Info
+  context?: Option Elab.ContextInfo := .none
+
+structure GoalCollectionOptions where
+  collectTypeErrors : Bool := false
+
+private def collectSorrysInTree (t : Elab.InfoTree) (options : GoalCollectionOptions := {})
+    : IO (List InfoWithContext) := do
+  let infos ← t.findAllInfoM none fun i ctx? => match i with
+    | .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
+      let .some ctx := ctx? | return (false, true)
+      if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
+        if expectedType?.isNone then
+          throw $ .userError "Sorry of indeterminant type is not allowed"
+        return (true, false)
+      unless options.collectTypeErrors do
+        return (false, true)
+      let .some expectedType := expectedType? | return (false, true)
+      let typeMatch ← ctx.runMetaM lctx do
+        let type ← Meta.inferType expr
+        Meta.isExprDefEqGuarded type expectedType
+      return match typeMatch, expr.hasSorry with
+      | false, true => (true, false) -- Types mismatch but has sorry -> collect, halt
+      | false, false => (true, false) -- Types mistmatch but no sorry -> collect, halt
+      | true, true => (false, true) -- Types match but has sorry -> continue
+      | true, false => (false, false) -- Types match but no sorries -> halt
+    | .ofTacticInfo { stx, goalsBefore, .. } =>
+      -- The `sorry` term is distinct from the `sorry` tactic
+      let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry
+      return (isSorry ∧ !goalsBefore.isEmpty, ¬ isSorry)
+    | _ => return (false, true)
+  return infos.map fun (info, context?, _) => { info, context? }
+
+-- NOTE: Plural deliberately not spelled "sorries"
+@[export pantograph_frontend_collect_sorrys_m]
+def collectSorrys (step: CompilationStep) (options : GoalCollectionOptions := {})
+    : IO (List InfoWithContext) := do
+  return (← step.trees.mapM $ λ tree => collectSorrysInTree tree options).flatten
+
+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_m]
+def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
+  let env := sorrys.head? >>= (·.context?) |>.map (·.env) |>.getD (← getEnv)
+  assert! !sorrys.isEmpty
+  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

@@ -0,0 +1,168 @@
+import Lean.Meta
+import Std.Data.HashMap
+
+open Lean
+
+namespace Pantograph.Frontend
+
+namespace MetaTranslate
+
+structure Context where
+  sourceMCtx : MetavarContext := {}
+  sourceLCtx : LocalContext := {}
+
+abbrev FVarMap := Std.HashMap FVarId FVarId
+
+structure State where
+  -- Stores mapping from old to new mvar/fvars
+  mvarMap: Std.HashMap MVarId MVarId := {}
+  fvarMap: Std.HashMap FVarId FVarId := {}
+
+/-
+Monadic state for translating a frozen meta state. The underlying `MetaM`
+operates in the "target" context and state.
+-/
+abbrev MetaTranslateM := ReaderT Context StateRefT State MetaM
+
+def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx
+def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx
+def addTranslatedFVar (src dst: FVarId) : MetaTranslateM Unit := do
+  modifyGet λ state => ((), { state with fvarMap := state.fvarMap.insert src dst })
+def addTranslatedMVar (src dst: MVarId) : MetaTranslateM Unit := do
+  modifyGet λ state => ((), { state with mvarMap := state.mvarMap.insert src dst })
+
+def saveFVarMap : MetaTranslateM FVarMap := do
+  return (← get).fvarMap
+def restoreFVarMap (map: FVarMap) : MetaTranslateM Unit := do
+  modifyGet λ state => ((), { state with fvarMap := map })
+def resetFVarMap : MetaTranslateM Unit := do
+  modifyGet λ state => ((), { state with fvarMap := {} })
+
+mutual
+private partial def translateLevel (srcLevel: Level) : MetaTranslateM Level := do
+  let sourceMCtx ← getSourceMCtx
+  let (_, level) := instantiateLevelMVarsImp sourceMCtx srcLevel
+  match level with
+  | .zero => return .zero
+  | .succ inner => do
+    let inner' ← translateLevel inner
+    return .succ inner'
+  | .max l1 l2 => do
+    let l1' ← translateLevel l1
+    let l2' ← translateLevel l2
+    return .max l1' l2'
+  | .imax l1 l2 => do
+    let l1' ← translateLevel l1
+    let l2' ← translateLevel l2
+    return .imax l1' l2'
+  | .param p => return .param p
+  | .mvar _ =>
+    Meta.mkFreshLevelMVar
+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
+  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}"
+      -- Delegating this to `Meta.check` later
+      --assert! (← getLCtx).contains fvarId'
+      return .done $ .fvar fvarId'
+    | .mvar mvarId => do
+      -- Must not be assigned
+      assert! !(sourceMCtx.eAssignment.contains mvarId)
+      match state.mvarMap[mvarId]? with
+      | .some mvarId' => do
+        return .done $ .mvar mvarId'
+      | .none => do
+        -- Entering another LCtx, must save the current one
+        let fvarMap ← saveFVarMap
+        let mvarId' ← translateMVarId mvarId
+        restoreFVarMap fvarMap
+        return .done $ .mvar mvarId'
+    | .sort level => do
+      let level' ← translateLevel level
+      return .done $ .sort level'
+    | _ => return .continue
+  Meta.check result
+  return result
+
+partial def translateLocalInstance (srcInstance: LocalInstance) : MetaTranslateM LocalInstance := do
+  return {
+    className := srcInstance.className,
+    fvar := ← translateExpr srcInstance.fvar
+  }
+partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do
+  let fvarId ← mkFreshFVarId
+  addTranslatedFVar srcLocalDecl.fvarId fvarId
+  match srcLocalDecl with
+  | .cdecl index _ userName type bi kind => do
+    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
+    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
+  resetFVarMap
+  let lctx ← MonadLCtx.getLCtx
+  assert! lctx.isEmpty
+  (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
+    let localDecl ← Meta.withLCtx lctx #[] do
+      translateLocalDecl srcLocalDecl
+    pure $ lctx.addDecl localDecl
+  ) lctx
+
+partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
+  if let .some mvarId' := (← get).mvarMap[srcMVarId]? then
+    return mvarId'
+  let mvarId' ← Meta.withLCtx .empty #[] do
+    let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
+    withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do
+      let lctx' ← translateLCtx
+      let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
+      Meta.withLCtx lctx' localInstances' do
+        let target' ← translateExpr srcDecl.type
+        let mvar' ← Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName
+        let mvarId' := mvar'.mvarId!
+        if let .some { fvars, mvarIdPending }:= (← getSourceMCtx).getDelayedMVarAssignmentExp srcMVarId then
+          -- Map the fvars in the pending context.
+          let mvarIdPending' ← translateMVarId mvarIdPending
+          let fvars' ← mvarIdPending'.withContext $ fvars.mapM translateExpr
+          assignDelayedMVar mvarId' fvars' mvarIdPending'
+        pure mvarId'
+  addTranslatedMVar srcMVarId mvarId'
+  return mvarId'
+end
+
+def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo)
+    : MetaTranslateM MVarId := do
+  withTheReader Context (λ ctx => { ctx with
+    sourceMCtx := context?.map (·.mctx) |>.getD {},
+    sourceLCtx := termInfo.lctx,
+  }) do
+    let type := termInfo.expectedType?.get!
+    let lctx' ← translateLCtx
+    let mvar ← Meta.withLCtx lctx' #[] do
+      let type' ← translateExpr type
+      Meta.mkFreshExprSyntheticOpaqueMVar type'
+    return mvar.mvarId!
+
+
+def translateMVarFromTacticInfoBefore (tacticInfo : Elab.TacticInfo) (_context? : Option Elab.ContextInfo)
+    : MetaTranslateM (List MVarId) := do
+  withTheReader Context (λ ctx => { ctx with sourceMCtx := tacticInfo.mctxBefore }) do
+    tacticInfo.goalsBefore.mapM translateMVarId
+
+
+end MetaTranslate
+
+export MetaTranslate (MetaTranslateM)
+
+initialize
+  registerTraceClass `Pantograph.Frontend.MetaTranslate
+
+end Pantograph.Frontend

Pantograph/Goal.lean

@@ -0,0 +1,463 @@
+/-
+Functions for handling metavariables
+
+All the functions starting with `try` resume their inner monadic state.
+-/
+import Pantograph.Tactic
+import Lean
+
+
+namespace Pantograph
+open Lean
+
+/--
+Represents an interconnected set of metavariables, or a state in proof search
+ -/
+structure GoalState where
+  savedState : Elab.Tactic.SavedState
+
+  -- The root hole which is the search target
+  root: MVarId
+
+  -- Parent state metavariable source
+  parentMVar?: Option MVarId
+
+  -- Existence of this field shows that we are currently in `conv` mode.
+  -- (convRhs, goal, dormant)
+  convMVar?: Option (MVarId × MVarId × List MVarId) := .none
+  -- Previous RHS for calc, so we don't have to repeat it every time
+  -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
+  calcPrevRhs?: Option (MVarId × Expr) := .none
+
+@[export pantograph_goal_state_create_m]
+protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
+  -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
+  -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
+
+  --Elab.Term.synthesizeSyntheticMVarsNoPostponing
+  --let expr ← instantiateMVars expr
+  let root ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)
+  let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
+  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root.mvarId!]}
+  return {
+    root := root.mvarId!,
+    savedState,
+    parentMVar? := .none,
+  }
+@[export pantograph_goal_state_create_from_mvars_m]
+protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do
+  let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
+  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals } |>.run' {}
+  return {
+    root,
+    savedState,
+    parentMVar? := .none,
+  }
+@[export pantograph_goal_state_is_conv]
+protected def GoalState.isConv (state: GoalState): Bool :=
+  state.convMVar?.isSome
+protected def GoalState.goals (state: GoalState): List MVarId :=
+  state.savedState.tactic.goals
+@[export pantograph_goal_state_goals]
+protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
+protected def GoalState.mctx (state: GoalState): MetavarContext :=
+  state.savedState.term.meta.meta.mctx
+protected def GoalState.env (state: GoalState): Environment :=
+  state.savedState.term.meta.core.env
+
+@[export pantograph_goal_state_meta_context_of_goal]
+protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
+  let mvarDecl ← state.mctx.findDecl? mvarId
+  return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
+protected def GoalState.metaState (state: GoalState): Meta.State :=
+  state.savedState.term.meta.meta
+protected def GoalState.coreState (state: GoalState): Core.SavedState :=
+  state.savedState.term.meta.core
+
+protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
+  mvarId.withContext m |>.run' (← read) state.metaState
+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!
+protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
+  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
+-- 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 := do
+  state.restoreCoreMExtra
+  state.savedState.term.restore
+private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
+  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[goalId]?
+  return {
+    state with
+    savedState := {
+      state.savedState with
+      tactic := { goals := [goal] },
+    },
+    calcPrevRhs? := .none,
+  }
+
+/-- Immediately bring all parent goals back into scope. Used in automatic mode -/
+@[export pantograph_goal_state_immediate_resume_parent]
+protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
+  -- Prune parents solved goals
+  let mctx := state.mctx
+  let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
+  {
+    state with
+    savedState := {
+      state.savedState with
+      tactic := { goals := state.goals ++ parentGoals },
+    },
+  }
+
+/--
+Brings into scope a list of goals
+-/
+@[export pantograph_goal_state_resume]
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
+  if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
+    let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
+    .error s!"Goals {invalid_goals} are not in scope"
+  else
+    -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
+    let unassigned := goals.filter (λ goal =>
+      let mctx := state.mctx
+      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
+    .ok {
+      state with
+      savedState := {
+        term := state.savedState.term,
+        tactic := { goals := unassigned },
+      },
+    }
+/--
+Brings into scope all goals from `branch`
+-/
+@[export pantograph_goal_state_continue]
+protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
+  if !target.goals.isEmpty then
+    .error s!"Target state has unresolved goals"
+  else if target.root != branch.root then
+    .error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}"
+  else
+    target.resume (goals := branch.goals)
+
+@[export pantograph_goal_state_root_expr]
+protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
+  if goalState.root.name == .anonymous then
+    .none
+  let expr ← goalState.mctx.eAssignment.find? goalState.root
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  if expr.hasExprMVar then
+    -- Must not assert that the goal state is empty here. We could be in a branch goal.
+    --assert! ¬goalState.goals.isEmpty
+    .none
+  else
+    assert! goalState.goals.isEmpty
+    return expr
+@[export pantograph_goal_state_parent_expr]
+protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
+  let parent ← goalState.parentMVar?
+  let expr := goalState.mctx.eAssignment.find! parent
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  return expr
+@[export pantograph_goal_state_get_mvar_e_assignment]
+protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarId): Option Expr := do
+  let expr ← goalState.mctx.eAssignment.find? mvarId
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  return expr
+
+--- Tactic execution functions ---
+
+-- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
+private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
+  -- These descendants serve as "seed" mvars. If a MVarError's mvar is related
+  -- to one of these seed mvars, it means an error has occurred when a tactic
+  -- was executing on `src`. `evalTactic`, will not capture these mvars, so we
+  -- need to manually find them and save them into the goal list.
+
+  let descendants ←  Meta.getMVars (.mvar src)
+  --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
+  let mut alreadyVisited : MVarIdSet := {}
+  let mut result : MVarIdSet := {}
+  for { mvarId, .. } in (← get).mvarErrorInfos do
+    unless alreadyVisited.contains mvarId do
+      alreadyVisited := alreadyVisited.insert mvarId
+      /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
+         delayed assigned to another metavariable that is unassigned. -/
+      let mvarDeps ← Meta.getMVars (.mvar mvarId)
+      if mvarDeps.any descendants.contains then do
+        result := mvarDeps.foldl (·.insert ·) result
+  return result.toList
+
+private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
+  let li2' := li2.filter (¬ li1.contains ·)
+  li1 ++ li2'
+
+/--
+Set `guardMVarErrors` to true to capture mvar errors. Lean will not
+automatically collect mvars from text tactics (vide
+`test_tactic_failure_synthesize_placeholder`)
+-/
+protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
+  : Elab.TermElabM GoalState := do
+  unless (← getMCtx).decls.contains goal do
+    throwError s!"Goal is not in context: {goal.name}"
+  goal.checkNotAssigned `GoalState.step
+  let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
+  let nextElabState ← MonadBacktrack.saveState
+  --Elab.Term.synthesizeSyntheticMVarsNoPostponing
+
+  let goals ← if guardMVarErrors then
+      pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
+    else
+      pure goals
+  return {
+    state with
+    savedState := { term := nextElabState, tactic := { goals }, },
+    parentMVar? := .some goal,
+    calcPrevRhs? := .none,
+  }
+
+/-- Response for executing a tactic -/
+inductive TacticResult where
+  -- Goes to next state
+  | success (state: GoalState)
+  -- Tactic failed with messages
+  | failure (messages: Array String)
+  -- Could not parse tactic
+  | parseError (message: String)
+  -- The given action cannot be executed in the state
+  | invalidAction (message: String)
+
+private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Array String) := do
+  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
+    |>.filterMapM λ m => do
+      if m.severity == .error then
+        return .some $ ← m.toString
+      else
+        return .none
+  Core.resetMessageLog
+  return newMessages.toArray
+
+/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
+protected def GoalState.tryTacticM
+    (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
+    (guardMVarErrors : Bool := false)
+    : Elab.TermElabM TacticResult := do
+  let prevMessageLength := state.coreState.messages.toList.length
+  try
+    let nextState ← state.step goal tacticM guardMVarErrors
+
+    -- Check if error messages have been generated in the core.
+    let newMessages ← dumpMessageLog prevMessageLength
+    if ¬ newMessages.isEmpty then
+      return .failure newMessages
+    return .success nextState
+  catch exception =>
+    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
+  let tactic ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := if state.isConv then `conv else `tactic)
+    (input := tactic)
+    (fileName := ← getFileName) with
+    | .ok stx => pure $ stx
+    | .error error => return .parseError error
+  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
+  state.restoreElabM
+  let expr ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := expr)
+    (fileName := ← getFileName) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.tryTacticM goal $ Tactic.evalAssign expr
+
+-- Specialized Tactics
+
+protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let type ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := type)
+    (fileName := ← getFileName) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.tryTacticM goal $ Tactic.evalLet binderName.toName type
+
+/-- Enter conv tactic mode -/
+protected def GoalState.conv (state: GoalState) (goal: MVarId):
+      Elab.TermElabM TacticResult := do
+  if state.convMVar?.isSome then
+    return .invalidAction "Already in conv state"
+  goal.checkNotAssigned `GoalState.conv
+  let tacticM :  Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
+    state.restoreTacticM goal
+
+    -- See Lean.Elab.Tactic.Conv.convTarget
+    let convMVar ← Elab.Tactic.withMainContext do
+      let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
+      Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
+      pure rhs.mvarId!
+    return (← MonadBacktrack.saveState, convMVar)
+  try
+    let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+    -- Other goals are now dormant
+    let otherGoals := state.goals.filter $ λ g => g != goal
+    return .success {
+      root := state.root,
+      savedState := nextSavedState
+      parentMVar? := .some goal,
+      convMVar? := .some (convRhs, goal, otherGoals),
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
+@[export pantograph_goal_state_conv_exit_m]
+protected def GoalState.convExit (state: GoalState):
+      Elab.TermElabM TacticResult := do
+  let (convRhs, convGoal, _) ← match state.convMVar? with
+    | .some mvar => pure mvar
+    | .none => return .invalidAction "Not in conv state"
+  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
+    -- Vide `Lean.Elab.Tactic.Conv.convert`
+    state.savedState.restore
+
+    -- Close all existing goals with `refl`
+    for mvarId in (← Elab.Tactic.getGoals) do
+      liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
+    Elab.Tactic.pruneSolvedGoals
+    unless (← Elab.Tactic.getGoals).isEmpty do
+      throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}"
+
+    Elab.Tactic.setGoals [convGoal]
+
+    let targetNew ← instantiateMVars (.mvar convRhs)
+    let proof ← instantiateMVars (.mvar convGoal)
+
+    Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
+    MonadBacktrack.saveState
+  try
+    let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+    return .success {
+      root := state.root,
+      savedState := nextSavedState
+      parentMVar? := .some convGoal,
+      convMVar? := .none
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do
+  let (mvarId, rhs) ← state.calcPrevRhs?
+  if mvarId == goal then
+    .some rhs
+  else
+    .none
+@[export pantograph_goal_state_try_calc_m]
+protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  if state.convMVar?.isSome then
+    return .invalidAction "Cannot initiate `calc` while in `conv` state"
+  let `(term|$pred) ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := pred)
+    (fileName := ← getFileName) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  goal.checkNotAssigned `GoalState.tryCalc
+  let calcPrevRhs? := state.calcPrevRhsOf? goal
+  let decl ← goal.getDecl
+  let target ← instantiateMVars decl.type
+  let tag := decl.userName
+  try
+    goal.withContext do
+
+    let mut step ← Elab.Term.elabType <| ← do
+      if let some prevRhs := calcPrevRhs? then
+        Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs)
+      else
+        pure pred
+
+    let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step |
+      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}"}"
+
+    -- Creates a mvar to represent the proof that the calc tactic solves the
+    -- current branch
+    -- In the Lean `calc` tactic this is gobbled up by
+    -- `withCollectingNewGoalsFrom`
+    let mut proof ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) step
+      (userName := tag ++ `calc)
+    let mvarBranch := proof.mvarId!
+
+    let mut proofType ← Meta.inferType proof
+    let mut remainder? := Option.none
+
+    -- The calc tactic either solves the main goal or leaves another relation.
+    -- Replace the main goal, and save the new goal if necessary
+    unless ← Meta.isDefEq proofType target do
+      let rec throwFailed :=
+        throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}"
+      let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed
+      let some (r, _, rhs') ← Elab.Term.getCalcRelation? target | throwFailed
+      let lastStep := mkApp2 r rhs rhs'
+      let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag
+      (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep
+      unless ← Meta.isDefEq proofType target do throwFailed
+      remainder? := .some lastStepGoal.mvarId!
+    goal.assign proof
+
+    let goals := [ mvarBranch ] ++ remainder?.toList
+    let calcPrevRhs? := remainder?.map $ λ g => (g, rhs)
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals },
+      },
+      parentMVar? := .some goal,
+      calcPrevRhs?
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+end Pantograph

Pantograph/Library.lean

@@ -0,0 +1,183 @@
+import Pantograph.Environment
+import Pantograph.Goal
+import Pantograph.Protocol
+import Pantograph.Delate
+import Pantograph.Version
+
+import Lean
+
+namespace Lean
+
+/-- This is better than the default version since it handles `.` and doesn't
+ crash the program when it fails. -/
+def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do
+  let ps := (entry.splitOn "=").map String.trim
+  let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
+  let key := key.toName
+  let defValue ← getOptionDefaultValue key
+  match defValue with
+  | DataValue.ofString _ => pure $ opts.setString key val
+  | DataValue.ofBool _   =>
+    match val with
+    | "true" => pure $ opts.setBool key true
+    | "false" => pure $ opts.setBool key false
+    | _ => throw  s!"invalid Bool option value '{val}'"
+  | DataValue.ofName _   => pure $ opts.setName key val.toName
+  | DataValue.ofNat _    =>
+    match val.toNat? with
+    | none   => throw s!"invalid Nat option value '{val}'"
+    | some v => pure $ opts.setNat key v
+  | DataValue.ofInt _    =>
+    match val.toInt? with
+    | none   => throw s!"invalid Int option value '{val}'"
+    | some v => pure $ opts.setInt key v
+  | DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
+
+end Lean
+
+open Lean
+
+namespace Pantograph
+
+def runMetaM { α } (metaM: MetaM α): CoreM α :=
+  metaM.run'
+
+def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
+
+/-- Adds the given paths to Lean package search path -/
+@[export pantograph_init_search]
+unsafe def initSearch (sp: String): IO Unit := do
+  Lean.enableInitializersExecution
+  Lean.initSearchPath (← Lean.findSysroot) (sp := System.SearchPath.parse sp)
+
+/-- Creates a Core.Context object needed to run all monads -/
+@[export pantograph_create_core_context]
+def createCoreContext (options: Array String): IO Core.Context := do
+  let options? ← options.foldlM setOptionFromString' Options.empty |>.run
+  let options ← match options? with
+    | .ok options => pure options
+    | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
+  return {
+    currNamespace := Name.str .anonymous "Aniva"
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph>",
+    fileMap := { source := "", positions := #[0] },
+    options := options
+  }
+
+/-- Creates a Core.State object needed to run all monads -/
+@[export pantograph_create_core_state]
+def createCoreState (imports: Array String): IO Core.State := do
+  let env ← Lean.importModules
+    (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+  return { env := env }
+
+@[export pantograph_parse_elab_type_m]
+def parseElabType (type: String): Protocol.FallibleT Elab.TermElabM Expr := do
+  let env ← MonadEnv.getEnv
+  let syn ← match parseTerm env type with
+    | .error str => Protocol.throw $ errorI "parsing" str
+    | .ok syn => pure syn
+  match ← elabType syn with
+  | .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): Protocol.FallibleT Elab.TermElabM Expr := do
+  let env ← MonadEnv.getEnv
+  let expectedType? ← expectedType?.mapM parseElabType
+  let syn ← match parseTerm env expr with
+    | .error str => Protocol.throw $ errorI "parsing" str
+    | .ok syn => pure syn
+  match ← elabTerm syn expectedType? with
+  | .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) (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) : 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) (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_have_m]
+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
+  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): Elab.TermElabM TacticResult := do
+  let expr ← match (← parseTermM expr) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.restoreElabM
+  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.restoreElabM
+  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

@@ -0,0 +1,398 @@
+/-
+All the command input/output structures are stored here
+
+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
+
+
+/-- Main Option structure, placed here to avoid name collision -/
+structure Options where
+  -- When false, suppress newlines in Json objects. Useful for machine-to-machine interaction.
+  -- This should be  false` by default to avoid any surprises with parsing.
+  printJsonPretty: Bool    := false
+  -- When enabled, pretty print every expression
+  printExprPretty: Bool    := true
+  -- When enabled, print the raw AST of expressions
+  printExprAST: Bool       := false
+  printDependentMVars: Bool := false
+  -- When enabled, the types and values of persistent variables in a goal
+  -- are not shown unless they are new to the proof step. Reduces overhead.
+  -- NOTE: that this assumes the type and assignment of variables can never change.
+  noRepeat: Bool := false
+  -- See `pp.auxDecls`
+  printAuxDecls: Bool      := false
+  -- See `pp.implementationDetailHyps`
+  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
+
+--- Expression Objects ---
+
+structure BoundExpression where
+  binders: Array (String × String)
+  target: String
+  deriving Lean.ToJson
+structure Expression where
+  -- Pretty printed expression
+  pp?: Option String             := .none
+  -- AST structure
+  sexp?: Option String           := .none
+  dependentMVars?: Option (Array String) := .none
+  deriving Lean.ToJson
+
+structure Variable where
+  /-- The internal name used in raw expressions -/
+  name: String := ""
+  /-- The name displayed to the user -/
+  userName: String
+  /-- Does the name contain a dagger -/
+  isInaccessible: Bool := false
+  type?: Option Expression  := .none
+  value?: Option Expression := .none
+  deriving Lean.ToJson
+structure Goal where
+  name: String := ""
+  /-- Name of the metavariable -/
+  userName?: Option String  := .none
+  /-- Is the goal in conversion mode -/
+  isConversion: Bool        := false
+  /-- target expression type -/
+  target: Expression
+  /-- Variables -/
+  vars: Array Variable      := #[]
+  deriving Lean.ToJson
+
+
+
+--- Individual Commands and return types ---
+
+structure Command where
+  cmd: String
+  payload: Lean.Json
+  deriving Lean.FromJson
+
+structure InteractionError where
+  error: String
+  desc: String
+  deriving Lean.ToJson
+
+def errorIndex (desc: String): InteractionError := { error := "index", desc }
+def errorExpr (desc: String): InteractionError := { error := "expr", desc }
+
+
+--- Individual command and return types ---
+
+
+structure Reset where
+  deriving Lean.FromJson
+structure Stat where
+  deriving Lean.FromJson
+structure StatResult where
+  -- Number of goals states
+  nGoals: Nat
+  deriving Lean.ToJson
+
+-- Return the type of an expression
+structure ExprEcho where
+  expr: String
+  type?: Option String := .none
+  -- universe levels
+  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
+structure EnvCatalogResult where
+  symbols: Array String
+  deriving Lean.ToJson
+
+-- Print the type of a symbol
+structure EnvInspect where
+  name: String
+  -- Show the value expressions; By default definitions values are shown and
+  -- theorem values are hidden.
+  value?: Option Bool := .some false
+  -- 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
+  numParams: Nat
+  numIndices: Nat
+  all: Array String
+  ctors: Array String
+  isRec:       Bool := false
+  isReflexive: Bool := false
+  isNested:    Bool := false
+  deriving Lean.ToJson
+-- See `ConstructorVal`
+structure ConstructorInfo where
+  induct: String
+  cidx: Nat
+  numParams: Nat
+  numFields: Nat
+  deriving Lean.ToJson
+
+/-- See `Lean/Declaration.lean` -/
+structure RecursorRule where
+  ctor: String
+  nFields: Nat
+  rhs: Expression
+  deriving Lean.ToJson
+structure RecursorInfo where
+  all: Array String
+  numParams: Nat
+  numIndices: Nat
+  numMotives: Nat
+  numMinors: Nat
+  rules: Array RecursorRule
+  k: Bool
+  deriving Lean.ToJson
+structure EnvInspectResult where
+  type: Expression
+  isUnsafe: Bool            := false
+  value?: Option Expression := .none
+  module?: Option String    := .none
+  -- If the name is private, displays the public facing name
+  publicName?: Option String := .none
+  typeDependency?: Option (Array String) := .none
+  valueDependency?: Option (Array String) := .none
+  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
+  levels?: Option (Array String) := .none
+  type?: Option String := .none
+  value: String
+  isTheorem: Bool := false
+  deriving Lean.FromJson
+structure EnvAddResult where
+  deriving Lean.ToJson
+
+structure EnvSaveLoad where
+  path: System.FilePath
+  deriving Lean.FromJson
+structure EnvSaveLoadResult where
+  deriving Lean.ToJson
+
+/-- Set options; See `Options` struct above for meanings -/
+structure OptionsSet where
+  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
+structure OptionsPrint where
+  deriving Lean.FromJson
+
+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 := .none -- Copy the type from a theorem in the environment
+  deriving Lean.FromJson
+structure GoalStartResult where
+  stateId: Nat := 0
+  -- Name of the root metavariable
+  root: String
+  deriving Lean.ToJson
+structure GoalTactic where
+  -- Identifiers for tree, state, and goal
+  stateId: Nat
+  goalId: Nat := 0
+  -- One of the fields here must be filled
+  tactic?: Option String := .none
+  expr?: Option String := .none
+  have?: Option String := .none
+  let?: Option String := .none
+  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
+
+  deriving Lean.FromJson
+structure GoalTacticResult where
+  -- The next goal state id. Existence of this field shows success
+  nextStateId?: Option Nat          := .none
+  -- If the array is empty, it shows the goals have been fully resolved.
+  goals?: Option (Array Goal)          := .none
+
+  -- Existence of this field shows tactic execution failure
+  tacticErrors?: Option (Array String) := .none
+
+  -- Existence of this field shows the tactic parsing has failed
+  parseError?: Option String := .none
+  deriving Lean.ToJson
+structure GoalContinue where
+  -- State from which the continuation acquires the context
+  target: Nat
+
+  -- One of the following must be supplied
+  -- The state which is an ancestor of `target` where goals will be extracted from
+  branch?: Option Nat := .none
+  -- Or, the particular goals that should be brought back into scope
+  goals?: Option (Array String) := .none
+  deriving Lean.FromJson
+structure GoalContinueResult where
+  nextStateId: Nat
+  goals: (Array Goal)
+  deriving Lean.ToJson
+
+-- Remove goal states
+structure GoalDelete where
+  -- This is ok being a List because it doesn't show up in the ABI
+  stateIds: List Nat
+  deriving Lean.FromJson
+structure GoalDeleteResult where
+  deriving Lean.ToJson
+
+structure GoalPrint where
+  stateId: Nat
+
+  -- Print root?
+  rootExpr?: Option Bool := .some False
+  -- Print the parent expr?
+  parentExpr?: Option Bool := .some False
+  -- Print goals?
+  goals?: Option Bool := .some False
+  -- Print values of extra mvars?
+  extraMVars?: Option (Array String) := .none
+  deriving Lean.FromJson
+structure GoalPrintResult where
+  -- The root expression
+  root?: Option Expression := .none
+  -- The filling expression of the parent goal
+  parent?: Option Expression := .none
+  goals: Array Goal := #[]
+  extraMVars: Array Expression := #[]
+  deriving Lean.ToJson
+
+-- Diagnostic Options, not available in REPL
+structure GoalDiag where
+  printContext: Bool := true
+  printValue: Bool := true
+  printNewMVars: Bool := false
+  -- Print all mvars
+  printAll: Bool := false
+  instantiate: Bool := true
+  printSexp: Bool := false
+
+structure GoalSave where
+  id: Nat
+  path: System.FilePath
+  deriving Lean.FromJson
+structure GoalSaveResult where
+  deriving Lean.ToJson
+structure GoalLoad where
+  path: System.FilePath
+  deriving Lean.FromJson
+structure GoalLoadResult where
+  id: Nat
+  deriving Lean.ToJson
+
+
+/-- Executes the Lean compiler on a single file -/
+structure FrontendProcess where
+  -- One of these two must be supplied: Either supply the file name or the content.
+  fileName?: Option String := .none
+  file?: Option String := .none
+  -- 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
+  -- 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
+  goalAfter: String
+  tactic: String
+
+  -- List of used constants
+  usedConstants: Array String
+  deriving Lean.ToJson
+
+structure CompilationUnit where
+  -- String boundaries of compilation units
+  boundary: (Nat × Nat)
+  messages: Array String := #[]
+  -- Tactic invocations
+  invocations?: Option (List InvokedTactic) := .none
+  goalStateId?: Option Nat := .none
+  goals?: Option (Array Goal) := .none
+  -- Code segments which generated the goals
+  goalSrcBoundaries?: Option (Array (Nat × Nat)) := .none
+
+  -- New constants defined in compilation unit
+  newConstants?: Option (Array String) := .none
+  deriving Lean.ToJson
+structure FrontendProcessResult where
+  units: List CompilationUnit
+  deriving Lean.ToJson
+
+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

@@ -0,0 +1,175 @@
+import Lean.Environment
+import Lean.Replay
+import Init.System.IOError
+import Std.Data.HashMap
+import Pantograph.Goal
+
+/-!
+Input/Output functions
+
+# Pickling and unpickling objects
+
+By abusing `saveModuleData` and `readModuleData` we can pickle and unpickle objects to disk.
+-/
+
+open Lean
+
+namespace Pantograph
+
+/--
+Save an object to disk.
+If you need to write multiple objects from within a single declaration,
+you will need to provide a unique `key` for each.
+-/
+def pickle {α : Type} (path : System.FilePath) (x : α) (key : Name := by exact decl_name%) : IO Unit :=
+  saveModuleData path key (unsafe unsafeCast x)
+
+/--
+Load an object from disk.
+Note: The returned `CompactedRegion` can be used to free the memory behind the value
+of type `α`, using `CompactedRegion.free` (which is only safe once all references to the `α` are
+released). Ignoring the `CompactedRegion` results in the data being leaked.
+Use `withUnpickle` to call `CompactedRegion.free` automatically.
+
+This function is unsafe because the data being loaded may not actually have type `α`, and this
+may cause crashes or other bad behavior.
+-/
+unsafe def unpickle (α : Type) (path : System.FilePath) : IO (α × CompactedRegion) := do
+  let (x, region) ← readModuleData path
+  pure (unsafeCast x, region)
+
+/-- Load an object from disk and run some continuation on it, freeing memory afterwards. -/
+unsafe def withUnpickle [Monad m] [MonadLiftT IO m] {α β : Type}
+    (path : System.FilePath) (f : α → m β) : m β := do
+  let (x, region) ← unpickle α path
+  let r ← f x
+  region.free
+  pure r
+
+/--
+Pickle an `Environment` to disk.
+
+We only store:
+* the list of imports
+* the new constants from `Environment.constants`
+and when unpickling, we build a fresh `Environment` from the imports,
+and then add the new constants.
+-/
+@[export pantograph_env_pickle_m]
+def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit :=
+  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.
+
+We construct a fresh `Environment` with the relevant imports,
+and then replace the new constants.
+-/
+@[export pantograph_env_unpickle_m]
+def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
+  let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
+  return (← resurrectEnvironment imports map₂, region)
+
+
+open Lean.Core in
+structure CompactCoreState where
+  -- env             : Environment
+  nextMacroScope  : MacroScope     := firstFrontendMacroScope + 1
+  ngen            : NameGenerator  := {}
+  -- traceState      : TraceState     := {}
+  -- cache           : Cache     := {}
+  -- messages        : MessageLog     := {}
+  -- infoState       : Elab.InfoState := {}
+
+@[export pantograph_goal_state_pickle_m]
+def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :=
+  let {
+    savedState := {
+      term := {
+        meta := {
+          core := {
+            env, nextMacroScope, ngen, ..
+          },
+          meta,
+        }
+        «elab»,
+      },
+      tactic
+    }
+    root,
+    parentMVar?,
+    convMVar?,
+    calcPrevRhs?,
+  } := goalState
+  Pantograph.pickle path (
+    env.constants.map₂,
+
+    ({ nextMacroScope, ngen } : CompactCoreState),
+    meta,
+    «elab»,
+    tactic,
+
+    root,
+    parentMVar?,
+    convMVar?,
+    calcPrevRhs?,
+  )
+
+@[export pantograph_goal_state_unpickle_m]
+def goalStateUnpickle (path : System.FilePath) (env : Environment)
+    : IO (GoalState × CompactedRegion) := unsafe do
+  let ((
+    map₂,
+
+    compactCore,
+    meta,
+    «elab»,
+    tactic,
+
+    root,
+    parentMVar?,
+    convMVar?,
+    calcPrevRhs?,
+  ), region) ← Pantograph.unpickle (
+    PHashMap Name ConstantInfo ×
+
+    CompactCoreState ×
+    Meta.State ×
+    Elab.Term.State ×
+    Elab.Tactic.State ×
+
+    MVarId ×
+    Option MVarId ×
+    Option (MVarId × MVarId × List MVarId) ×
+    Option (MVarId × Expr)
+  ) path
+  let env ← env.replay (Std.HashMap.ofList map₂.toList)
+  let goalState := {
+    savedState := {
+      term := {
+        meta := {
+          core := {
+            compactCore with
+            passedHeartbeats := 0,
+            env,
+          },
+          meta,
+        },
+        «elab»,
+      },
+      tactic,
+    },
+    root,
+    parentMVar?,
+    convMVar?,
+    calcPrevRhs?,
+  }
+  return (goalState, region)
+
+end Pantograph

Pantograph/Tactic.lean

@@ -0,0 +1,2 @@
+import Pantograph.Tactic.Assign
+import Pantograph.Tactic.Prograde

Pantograph/Tactic/Assign.lean

@@ -0,0 +1,65 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+/-- WARNING: This should be used with a function like `elabTermWithHoles` that properly collects the mvar information from `expr`. -/
+def assign (goal: MVarId) (expr: Expr) (nextGoals: List MVarId): MetaM (List MVarId) := do
+  goal.checkNotAssigned `Pantograph.Tactic.assign
+
+  -- This run of the unifier is critical in resolving mvars in passing
+  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}"
+  goal.assign expr
+  nextGoals.filterM (not <$> ·.isAssigned)
+
+def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
+  let target ← Elab.Tactic.getMainTarget
+  let goal ← Elab.Tactic.getMainGoal
+  goal.checkNotAssigned `Pantograph.Tactic.evalAssign
+  let (expr, nextGoals) ← Elab.Tactic.elabTermWithHoles stx
+    (expectedType? := .some target)
+    (tagSuffix := .anonymous )
+    (allowNaturalHoles := true)
+  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/Prograde.lean

@@ -0,0 +1,88 @@
+/- Prograde (forward) reasoning tactics -/
+
+import Lean
+open Lean
+
+namespace Pantograph.Tactic
+
+private def mkUpstreamMVar (goal: MVarId) : MetaM Expr := do
+  Meta.mkFreshExprSyntheticOpaqueMVar (← goal.getType) (tag := ← goal.getTag)
+
+
+/-- Introduces a fvar to the current mvar -/
+def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.define
+  let type ← Meta.inferType expr
+
+  Meta.withLetDecl binderName type expr λ fvar => do
+    let mvarUpstream ← mkUpstreamMVar mvarId
+    mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
+    pure (fvar.fvarId!, mvarUpstream.mvarId!)
+
+def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
+  let (_, mvarId) ← define goal binderName expr
+  Elab.Tactic.replaceMainGoal [mvarId]
+
+structure BranchResult where
+  fvarId?: Option FVarId := .none
+  branch: MVarId
+  main: MVarId
+
+def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.have
+  let lctx ← MonadLCtx.getLCtx
+  -- The branch goal inherits the same context, but with a different type
+  let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
+
+  -- Create the context for the `upstream` goal
+  let fvarId ← mkFreshFVarId
+  let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
+  let mvarUpstream ←
+    Meta.withLCtx lctxUpstream #[] do
+      Meta.withNewLocalInstances #[.fvar fvarId] 0 do
+        let mvarUpstream ← mkUpstreamMVar mvarId
+        --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
+        mvarId.assign $ ← Meta.mkLambdaFVars #[.fvar fvarId] mvarUpstream
+        pure mvarUpstream
+
+  return {
+    fvarId? := .some fvarId,
+    branch := mvarBranch.mvarId!,
+    main := mvarUpstream.mvarId!,
+  }
+
+def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let nextGoals: List MVarId ← goal.withContext do
+    let type ← Elab.Term.elabType (stx := type)
+    let result ← «have» goal binderName type
+    pure [result.branch, result.main]
+  Elab.Tactic.replaceMainGoal nextGoals
+
+def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.let
+  let lctx ← MonadLCtx.getLCtx
+
+  -- The branch goal inherits the same context, but with a different type
+  let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type (userName := binderName)
+
+  assert! ¬ type.hasLooseBVars
+  let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do
+    let mvarUpstream ← mkUpstreamMVar mvarId
+    mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
+    pure mvarUpstream
+
+  return {
+    branch := mvarBranch.mvarId!,
+    main := mvarUpstream.mvarId!,
+  }
+
+def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let type ← goal.withContext $ Elab.Term.elabType (stx := type)
+  let result ← «let» goal binderName type
+  Elab.Tactic.replaceMainGoal [result.branch, result.main]
+
+end Pantograph.Tactic

Pantograph/Version.lean

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

README.md

@@ -0,0 +1,130 @@
+# Pantograph
+
+A Machine-to-Machine interaction system for Lean 4.
+
+![Pantograph](doc/icon.svg)
+
+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
+``` sh
+nix build .#{sharedLib,executable}
+```
+to build either the shared library or executable.
+
+Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and
+run
+
+``` sh
+lake build
+```
+This builds the executable in `.lake/build/bin/pantograph-repl`.
+
+## Executable Usage
+
+``` sh
+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
+```
+command { ... }
+{ "cmd": command, "payload": ... }
+```
+The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
+empty command aborts the REPL.
+
+
+Example: (~5k symbols)
+```
+$ pantograph Init
+env.catalog
+env.inspect {"name": "Nat.le_add_left"}
+```
+Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
+```
+$ pantograph Mathlib.Analysis.Seminorm
+env.catalog
+```
+Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
+```
+$ pantograph Init
+goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
+goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"}
+goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"}
+goal.delete {"stateIds": [0]}
+stat {}
+goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
+stat
+```
+where the application of `assumption` should lead to a failure.
+
+For a list of commands, see [REPL Documentation](doc/repl.md).
+
+### Project Environment
+
+To use Pantograph in a project environment, setup the `LEAN_PATH` environment
+variable so it contains the library path of lean libraries. The libraries must
+be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
+the environment might be setup like this:
+
+``` sh
+LIB="../lib"
+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 $@
+```
+The `$LEAN_PATH` executable of any project can be extracted by
+``` sh
+lake env printenv LEAN_PATH
+```
+
+### Troubleshooting
+
+If lean encounters stack overflow problems when printing catalog, execute this before running lean:
+```sh
+ulimit -s unlimited
+```
+
+## Library Usage
+
+`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
+with `Pantograph` which mirrors the REPL commands above. It is recommended to
+call Pantograph via this FFI since it provides a tremendous speed up.
+
+The executable can be used as-is, but linking against the shared library
+requires the presence of `lean-all`. Note that there isn't a 1-1 correspondence
+between executable (REPL) commands and library functions.
+
+Inject any project path via the `pantograph_init_search` function.
+
+## Developing
+
+A Lean development shell is provided in the Nix flake.
+
+### Testing
+
+The tests are based on `LSpec`. To run tests, use either
+``` sh
+nix flake check
+```
+or
+``` sh
+lake test
+```
+You can run an individual test by specifying a prefix
+
+``` sh
+lake test -- "Tactic/No Confuse"
+```

Repl.lean

@@ -0,0 +1,399 @@
+import Std.Data.HashMap
+import Pantograph
+
+namespace Pantograph.Repl
+
+open Lean
+
+structure Context where
+  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
+
+  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
+  let stateId := state.nextId
+  set { state with
+    goalStates := state.goalStates.insert stateId goalState,
+    nextId := state.nextId + 1
+  }
+  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
+
+def runCoreM' { α } (coreM : Protocol.FallibleT CoreM α) : EMainM α := do
+  liftExcept $ ← runCoreM coreM.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 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): EMainM Protocol.StatResult := do
+    let state ← getMainState
+    let nGoals := state.goalStates.size
+    set { state with nextId := 0, goalStates := .empty }
+    return { nGoals }
+  stat (_: Protocol.Stat): EMainM Protocol.StatResult := do
+    let state ← getMainState
+    let nGoals := state.goalStates.size
+    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 {}
+  env_load (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
+    let (env, _) ← environmentUnpickle args.path
+    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 := {
+        -- FIXME: This should be replaced with something more elegant
+        printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
+        printExprPretty := args.printExprPretty?.getD options.printExprPretty,
+        printExprAST := args.printExprAST?.getD options.printExprAST,
+        printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars,
+        noRepeat := args.noRepeat?.getD options.noRepeat,
+        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 {  }
+  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"
+    match expr? with
+    | .error error => Protocol.throw error
+    | .ok goalState =>
+      let stateId ← newGoalState goalState
+      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]? |
+      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, .none => do
+        pure <| Except.ok <| ← goalState.tryAssign goal expr
+      | .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, .none => do
+        let binderName := args.binderName?.getD ""
+        pure <| Except.ok <| ← goalState.tryLet goal binderName type
+      | .none, .none, .none, .none, .some pred, .none, .none => do
+        pure <| Except.ok <| ← goalState.tryCalc goal pred
+      | .none, .none, .none, .none, .none, .some true, .none => do
+        pure <| Except.ok <| ← goalState.conv goal
+      | .none, .none, .none, .none, .none, .some false, .none => do
+        pure <| Except.ok <| ← goalState.convExit
+      | .none, .none, .none, .none, .none, .none, .some draft => do
+        pure <| Except.ok <| ← goalState.tryDraft goal draft
+      | _, _, _, _, _, _, _ =>
+        let error := errorI "arguments" "Exactly one of {tactic, expr, have, let, calc, conv, draft} must be supplied"
+        pure $ .error error
+    match nextGoalState? with
+    | .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) |
+            Protocol.throw $ errorIO "Resuming known goals"
+          pure result
+        | true, .some true => pure nextGoalState
+        | true, .some false => do
+          let .some (_, _, dormantGoals) := goalState.convMVar? |
+            Protocol.throw $ errorIO "If conv exit succeeded this should not fail"
+          let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
+            Protocol.throw $ errorIO "Resuming known goals"
+          pure result
+        | false, _ => pure nextGoalState
+      let nextStateId ← newGoalState nextGoalState
+      let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
+      return {
+        nextStateId? := .some nextStateId,
+        goals? := .some goals,
+      }
+    | .ok (.parseError message) =>
+      return { parseError? := .some message }
+    | .ok (.invalidAction message) =>
+      Protocol.throw $ errorI "invalid" message
+    | .ok (.failure messages) =>
+      return { tacticErrors? := .some messages }
+  goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
+    let state ← getMainState
+    let .some target := state.goalStates[args.target]? |
+      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 => Protocol.throw $ errorIndex s!"Invalid state index {branchId}"
+        | .some branch => pure $ target.continue branch
+      | .none, .some goals =>
+        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 ← liftMetaM $ goalSerialize nextGoalState (options := state.options)
+      return {
+        nextStateId,
+        goals,
+      }
+  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 {}
+  goal_print (args: Protocol.GoalPrint): EMainM Protocol.GoalPrintResult := do
+    let state ← getMainState
+    let .some goalState := state.goalStates[args.stateId]? |
+      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]? |
+      Protocol.throw $ errorIndex s!"Invalid state index {args.id}"
+    goalStatePickle goalState args.path
+    return {}
+  goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do
+    let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
+    let id ← newGoalState goalState
+    return { id }
+  frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
+    frontend_process_inner args
+
+end Pantograph.Repl

Test/Common.lean

@@ -0,0 +1,177 @@
+import Pantograph.Goal
+import Pantograph.Library
+import Pantograph.Protocol
+import Lean
+import LSpec
+
+open Lean
+
+namespace Pantograph
+
+deriving instance Repr for Expr
+-- Use strict equality check for expressions
+instance : BEq Expr := ⟨Expr.equal⟩
+
+def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
+
+-- Auxiliary functions
+namespace Protocol
+def Goal.devolatilizeVars (goal: Goal): Goal :=
+  {
+    goal with
+    vars := goal.vars.map removeInternalAux,
+
+  }
+  where removeInternalAux (v: Variable): Variable :=
+    {
+      v with
+      name := ""
+    }
+/-- Set internal names to "" -/
+def Goal.devolatilize (goal: Goal): Goal :=
+  {
+    goal.devolatilizeVars with
+    name := "",
+  }
+
+deriving instance DecidableEq, Repr for Name
+deriving instance DecidableEq, Repr for Expression
+deriving instance DecidableEq, Repr for Variable
+deriving instance DecidableEq, Repr for Goal
+deriving instance DecidableEq, Repr for ExprEchoResult
+deriving instance DecidableEq, Repr for InteractionError
+deriving instance DecidableEq, Repr for Option
+end Protocol
+
+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 }
+  }
+protected def Goal.devolatilize (goal: Goal): Goal :=
+  {
+    goal with
+    mvarId := { name := .anonymous },
+    context := goal.context.map LocalDecl.devolatilize
+  }
+
+end Condensed
+
+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)"
+  | .failure messages =>
+    let messages := "\n".intercalate messages.toList
+    s!".failure {messages}"
+  | .parseError error => s!".parseError {error}"
+  | .invalidAction error => s!".invalidAction {error}"
+
+namespace Test
+
+def expectationFailure (desc: String) (error: String): LSpec.TestSeq := LSpec.test desc (LSpec.ExpectationFailure "ok _" error)
+def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
+
+def parseFailure (error: String) := expectationFailure "parse" error
+def elabFailure (error: String) := expectationFailure "elab" error
+
+def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array String := #[]): IO LSpec.TestSeq := do
+  let coreContext: Core.Context ← createCoreContext options
+  match ← (coreM.run' coreContext { env := env }).toBaseIO with
+  | .error exception =>
+    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
+  | .ok a            => return a
+def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
+  runCoreMSeq env metaM.run'
+def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
+  termElabM.run' (ctx := defaultElabContext)
+def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
+  runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
+
+def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
+
+def strToTermSyntax (s: String): CoreM Syntax := do
+  let .ok stx := Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := s)
+    (fileName := ← getFileName) | panic! s!"Failed to parse {s}"
+  return stx
+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 := ← getFileName) with
+    | .ok syn => pure syn
+    | .error error => throwError "Failed to parse: {error}"
+  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] }
+    return newGoals.goals
+def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
+  let name := (← mvarId.getDecl).userName
+  let t ← exprToStr (← mvarId.getType)
+  return (name, t)
+
+
+-- Monadic testing
+
+abbrev TestT := StateRefT' IO.RealWorld LSpec.TestSeq
+
+section Monadic
+
+variable [Monad m] [MonadLiftT (ST IO.RealWorld) m]
+
+def addTest (test: LSpec.TestSeq) : TestT m Unit := do
+  set $ (← get) ++ test
+
+def checkEq [DecidableEq α] [Repr α] (desc : String) (lhs rhs : α) : TestT m Unit := do
+  addTest $ LSpec.check desc (lhs = rhs)
+def checkTrue (desc : String) (flag : Bool) : TestT m Unit := do
+  addTest $ LSpec.check desc flag
+def fail (desc : String) : TestT m Unit := do
+  addTest $ LSpec.check desc false
+
+def runTest (t: TestT m Unit): m LSpec.TestSeq :=
+  Prod.snd <$> t.run LSpec.TestSeq.done
+def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) :=
+  t.run LSpec.TestSeq.done
+def runTestCoreM (env: Environment) (coreM: TestT CoreM Unit) (options: Array String := #[]): IO LSpec.TestSeq := do
+  runCoreMSeq env (runTest coreM) options
+
+end Monadic
+
+def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
+  IO LSpec.TestSeq :=
+  runTermElabMSeq env $ runTest t
+
+def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl :=
+  { userName, type }
+
+def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
+    Protocol.Goal :=
+  {
+    userName?,
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      userName := x.fst,
+      type? := .some { pp? := .some x.snd },
+    })).toArray
+  }
+
+end Test
+
+end Pantograph

Test/Delate.lean

@@ -0,0 +1,135 @@
+import LSpec
+import Pantograph.Delate
+import Test.Common
+import Lean
+
+open Lean Pantograph
+
+namespace Pantograph.Test.Delate
+
+deriving instance Repr, DecidableEq for Protocol.BoundExpression
+
+def test_serializeName: LSpec.TestSeq :=
+  let quote := "\""
+  let escape := "\\"
+  LSpec.test "a.b.1" (serializeName (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
+  LSpec.test "seg.«a.b»" (serializeName (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++
+  -- Pathological test case
+  LSpec.test s!"«̈{escape}{quote}»" (serializeName (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}")
+
+def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
+  let entries: List (Name × Protocol.BoundExpression) := [
+    ("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
+    ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "n.succ ≤ m")], target := "n ≤ m" })
+  ]
+  runCoreMSeq env $ entries.foldlM (λ suites (symbol, target) => do
+    let env ← MonadEnv.getEnv
+    let expr := env.find? symbol |>.get! |>.type
+    let test := LSpec.check symbol.toString ((← typeExprToBound expr) = target)
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
+
+def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
+  let entries: List (String × String) := [
+    -- This one contains unhygienic variable names which must be suppressed
+    ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"),
+    -- These ones are normal and easy
+    ("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"),
+    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :i) :i)"),
+    -- Handling of higher order types
+    ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
+    ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
+  ]
+  runMetaMSeq env $ entries.foldlM (λ suites (symbol, target) => do
+    let env ← MonadEnv.getEnv
+    let expr := env.find? symbol.toName |>.get! |>.type
+    let test := LSpec.check symbol ((← serializeExpressionSexp expr) = target)
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
+
+def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
+  let entries: List (String × (List Name) × String) := [
+    ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
+    ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
+    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
+    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
+    ("(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) =>
+    let termElabM := do
+      let env ← MonadEnv.getEnv
+      let s ← match parseTerm env source with
+        | .ok s => pure s
+        | .error e => return parseFailure e
+      let expr ← match (← elabTerm s) with
+        | .ok expr => pure expr
+        | .error e => return elabFailure e
+      return LSpec.check source ((← serializeExpressionSexp expr) = target)
+    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultElabContext)
+    return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
+    LSpec.TestSeq.done
+
+def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
+  let entries: List (Expr × String) := [
+    (.lam `p (.sort .zero)
+        (.lam `q (.sort .zero)
+          (.lam `k (mkApp2 (.const `And []) (.bvar 1) (.bvar 0))
+            (.proj `And 1 (.bvar 0))
+            .default)
+        .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
+    let env ← MonadEnv.getEnv
+    let testCaseName := target.take 10
+    let test := LSpec.check   testCaseName ((← serializeExpressionSexp expr) = target)
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
+  runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
+
+-- Instance parsing
+def test_instance (env: Environment): IO LSpec.TestSeq :=
+  runMetaMSeq env do
+    let env ← MonadEnv.getEnv
+    let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
+    let s := parseTerm env source |>.toOption |>.get!
+    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),
+    ("Expression binder", test_expr_to_binder env),
+    ("Sexp from symbol", test_sexp_of_symbol env),
+    ("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

@@ -0,0 +1,133 @@
+import LSpec
+import Pantograph.Delate
+import Pantograph.Environment
+import Test.Common
+import Lean
+
+open Lean
+namespace Pantograph.Test.Environment
+
+open Pantograph
+
+deriving instance DecidableEq, Repr for Protocol.InductInfo
+deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
+deriving instance DecidableEq, Repr for Protocol.RecursorRule
+deriving instance DecidableEq, Repr for Protocol.RecursorInfo
+deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
+
+def test_catalog: IO LSpec.TestSeq := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
+  let inner: CoreM LSpec.TestSeq := do
+    let catalogResult ← Environment.catalog {}
+    let symbolsWithNum := env.constants.fold (init := #[]) (λ acc name info =>
+      match (Environment.toFilteredSymbol name info).isSome && (name matches .num _ _) with
+      | false => acc
+      | true => acc.push name
+      )
+    return LSpec.check "No num symbols" (symbolsWithNum.size == 0)
+  runCoreMSeq env inner
+
+def test_symbol_visibility: IO LSpec.TestSeq := do
+  let entries: List (Name × Bool) := [
+    ("Nat.add_comm".toName, false),
+    ("foo.bla.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4".toName, true),
+    ("Init.Data.Nat.Basic._auxLemma.4".toName, true),
+  ]
+  let suite := entries.foldl (λ suites (symbol, target) =>
+    let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
+    LSpec.TestSeq.append suites test) LSpec.TestSeq.done
+  return suite
+
+inductive ConstantCat where
+  | induct (info: Protocol.InductInfo)
+  | ctor (info: Protocol.ConstructorInfo)
+  | recursor (info: Protocol.RecursorInfo)
+
+def test_inspect: IO LSpec.TestSeq := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
+  let testCases: List (String × ConstantCat) := [
+    ("Or", ConstantCat.induct {
+      numParams := 2,
+      numIndices := 0,
+      all := #["Or"],
+      ctors := #["Or.inl", "Or.inr"],
+    }),
+    ("Except.ok", ConstantCat.ctor {
+      induct := "Except",
+      cidx := 1,
+      numParams := 2,
+      numFields := 1,
+    }),
+    ("Eq.rec", ConstantCat.recursor {
+      all := #["Eq"],
+      numParams := 2,
+      numIndices := 1,
+      numMotives := 1,
+      numMinors := 1,
+      rules := #[{ ctor := "Eq.refl", nFields := 0, rhs := { pp? := .some "fun {α} a motive refl => refl" } }]
+      k := true,
+    }),
+    ("ForM.rec", ConstantCat.recursor {
+      all := #["ForM"],
+      numParams := 3,
+      numIndices := 0,
+      numMotives := 1,
+      numMinors := 1,
+      rules := #[{ ctor := "ForM.mk", nFields := 1, rhs := { pp? := .some "fun m γ α motive mk forM => mk forM" } }]
+      k := false,
+    })
+  ]
+  let inner: CoreM LSpec.TestSeq := do
+    testCases.foldlM (λ acc (name, cat) => do
+      let args: Protocol.EnvInspect := { name := name }
+      let result ← match ← Environment.inspect args (options := {}) with
+        | .ok result => pure $ result
+        | .error e => panic! s!"Error: {e.desc}"
+      let p := match cat with
+        | .induct info => LSpec.test name (result.inductInfo? == .some info)
+        | .ctor info => LSpec.test name (result.constructorInfo? == .some info)
+        | .recursor info => LSpec.test name (result.recursorInfo? == .some info)
+      return LSpec.TestSeq.append acc p
+    ) 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

@@ -0,0 +1,266 @@
+import Pantograph
+import Repl
+import Test.Common
+
+import LSpec
+
+open Lean Pantograph
+namespace Pantograph.Test.Frontend
+
+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 options)
+  let li ← m.run context |>.run' state
+  let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
+    if sorrys.isEmpty then
+      return .none
+    let { state, .. } ← Frontend.sorrysToGoalState sorrys
+    return .some state
+  return goalStates
+
+def test_multiple_sorrys_in_proof : TestT MetaM Unit := do
+  let sketch := "
+theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := by
+   have h_nat_add_succ: ∀ n m : Nat, n = m := sorry
+   sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! "Incorrect number of states"
+  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+    {
+      target := { pp? := "∀ (n m : Nat), n = m" },
+      vars := #[
+      ]
+    },
+    {
+      target := { pp? := "∀ (n m : Nat), n + (m + 1) = n + m + 1" },
+      vars := #[{
+        userName := "h_nat_add_succ",
+        type? := .some { pp? := "∀ (n m : Nat), n = m" },
+      }],
+    }
+  ])
+
+def test_sorry_in_middle: TestT MetaM Unit := do
+  let sketch := "
+example : ∀ (n m: Nat), n + m = m + n := by
+  intros n m
+  sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+    {
+      target := { pp? := "n + m = m + n" },
+      vars := #[{
+           userName := "n",
+           type? := .some { pp? := "Nat" },
+        }, {
+           userName := "m",
+           type? := .some { pp? := "Nat" },
+        }
+      ],
+    }
+  ])
+
+def test_sorry_in_induction : TestT MetaM Unit := do
+  let sketch := "
+example : ∀ (n m: Nat), n + m = m + n := by
+  intros n m
+  induction n with
+  | zero =>
+    have h1 : 0 + m = m := sorry
+    sorry
+  | succ n ih =>
+    have h2 : n + m = m := sorry
+    sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+    {
+      target := { pp? := "0 + m = m" },
+      vars := #[{
+        userName := "m",
+        type? := .some { pp? := "Nat" },
+      }]
+    },
+    {
+      userName? := .some "zero",
+      target := { pp? := "0 + m = m + 0" },
+      vars := #[{
+        userName := "m",
+        type? := .some { pp? := "Nat" },
+      }, {
+        userName := "h1",
+        type? := .some { pp? := "0 + m = m" },
+      }]
+    },
+    {
+      target := { pp? := "n + m = m" },
+      vars := #[{
+        userName := "m",
+        type? := .some { pp? := "Nat" },
+      }, {
+        userName := "n",
+        type? := .some { pp? := "Nat" },
+      }, {
+        userName := "ih",
+        type? := .some { pp? := "n + m = m + n" },
+      }]
+    },
+    {
+      userName? := .some "succ",
+      target := { pp? := "n + 1 + m = m + (n + 1)" },
+      vars := #[{
+        userName := "m",
+        type? := .some { pp? := "Nat" },
+      }, {
+        userName := "n",
+        type? := .some { pp? := "Nat" },
+      }, {
+        userName := "ih",
+        type? := .some { pp? := "n + m = m + n" },
+      },  {
+        userName := "h2",
+        type? := .some { pp? := "n + m = m" },
+      }]
+    }
+  ])
+
+def test_sorry_in_coupled: TestT MetaM Unit := do
+  let sketch := "
+example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by
+  intro y
+  apply Exists.intro
+  case h => sorry
+  case w => sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+    {
+      target := { pp? := "y + 1 = ?w" },
+      vars := #[{
+           userName := "y",
+           type? := .some { pp? := "Nat" },
+        }
+      ],
+    },
+    {
+      userName? := .some "w",
+      target := { pp? := "Nat" },
+      vars := #[{
+           userName := "y",
+           type? := .some { pp? := "Nat" },
+        }
+      ],
+    }
+  ])
+
+def test_environment_capture: TestT MetaM Unit := do
+  let sketch := "
+def mystery (n: Nat) := n + 1
+
+example (n: Nat) : mystery n + 1 = n + 2 := sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+    {
+      target := { pp? := "mystery n + 1 = n + 2" },
+      vars := #[{
+         userName := "n",
+         type? := .some { pp? := "Nat" },
+      }],
+    }
+  ])
+
+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))
+
+end Pantograph.Test.Frontend

Test/Integration.lean

@@ -0,0 +1,329 @@
+/- Integration test for the REPL
+ -/
+import LSpec
+import Pantograph
+import Repl
+import Test.Common
+
+namespace Pantograph.Test.Integration
+open Pantograph.Repl
+
+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 (result.pretty = (Lean.toJson expected).pretty)
+
+abbrev Test := List (MainM LSpec.TestSeq)
+
+def test_expr_echo : Test :=
+  [
+    step "expr.echo"
+     ({ expr := "λ {α : Sort (u + 1)} => List α", levels? := .some #["u"]}: Protocol.ExprEcho)
+     ({
+       type := { pp? := .some "{α : Type u} → Type u" },
+       expr := { pp? := .some "fun {α} => List α" }
+     }: Protocol.ExprEchoResult),
+  ]
+
+def test_option_modify : Test :=
+  let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ"
+  let sexp? := Option.some "(: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)))"
+  let module? := Option.some "Init.Data.Nat.Basic"
+  let options: Protocol.Options := {}
+  [
+    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
+     ({ type := { pp? }, module? }: Protocol.EnvInspectResult),
+    step "options.set" ({ printExprAST? := .some true } : Protocol.OptionsSet)
+     ({ }: Protocol.OptionsSetResult),
+    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
+     ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
+    step "options.print" ({} : Protocol.OptionsPrint)
+     ({ options with printExprAST := true }: Protocol.Options),
+  ]
+def test_malformed_command : Test :=
+  let invalid := "invalid"
+  [
+    step invalid ({ name := "Nat.add_one" }: Protocol.EnvInspect)
+     ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
+     (name? := .some "Invalid Command"),
+    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 := #[varX],
+  }
+  let goal2: Protocol.Goal := {
+    name := "_uniq.14",
+    target := { pp? := .some "x ∨ y → y ∨ x" },
+    vars := #[
+      varX,
+      { name := "_uniq.13", userName := "y", type? := .some { pp? := .some "Prop" }}
+    ],
+  }
+  [
+    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p" }: Protocol.GoalStart)
+     ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
+    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" }},
+    { name := "_uniq.13", userName := "q", type? := .some { pp? := .some "Prop" }}
+  ]
+  let goal1: Protocol.Goal := {
+    name := "_uniq.17",
+    target := { pp? := .some "q ∨ p" },
+    vars := varsPQ ++ #[
+      { name := "_uniq.16", userName := "h", type? := .some { pp? := .some "p ∨ q" }}
+    ],
+  }
+  let goal2l: Protocol.Goal := {
+    name := "_uniq.61",
+    userName? := .some "inl",
+    target := { pp? := .some "q ∨ p" },
+    vars := varsPQ ++ #[
+      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+    ],
+  }
+  let goal2r: Protocol.Goal := {
+    name := "_uniq.74",
+    userName? := .some "inr",
+    target := { pp? := .some "q ∨ p" },
+    vars := varsPQ ++ #[
+      { name := "_uniq.62", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
+    ],
+  }
+  let goal3l: Protocol.Goal := {
+    name := "_uniq.80",
+    userName? := .some "inl.h",
+    target := { pp? := .some "p" },
+    vars := varsPQ ++ #[
+      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+    ],
+  }
+  [
+    step "options.set" ({automaticMode? := .some automatic}: Protocol.OptionsSet)
+     ({}: Protocol.OptionsSetResult),
+    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p"} : Protocol.GoalStart)
+     ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro p q h" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
+    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 := 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 := name1,
+        value := "λ (a b: Prop) => Or a b",
+        isTheorem := false
+      }: Protocol.EnvAdd)
+     ({}: Protocol.EnvAddResult),
+    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 := name2,
+        type? := "Nat → Int",
+        value := "λ (a: Nat) => a + 1",
+        isTheorem := false
+      }: Protocol.EnvAdd)
+     ({}: Protocol.EnvAddResult),
+    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),
+    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
+  intro p h
+  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"
+  [
+    step "frontend.process"
+      ({
+        file? := .some file,
+        invocations := true,
+      }: Protocol.FrontendProcess)
+     ({
+       units := [{
+         boundary := (0, file.utf8ByteSize),
+         invocations? := .some [
+           {
+             goalBefore := "⊢ ∀ (p q : Prop), p → p ∨ q",
+             goalAfter := goal1,
+             tactic := "intro p q h",
+             usedConstants := #[],
+           },
+           {
+             goalBefore := goal1 ,
+             goalAfter := "",
+             tactic := "exact Or.inl h",
+             usedConstants := #["Or.inl"],
+           },
+         ]
+       }],
+    }: Protocol.FrontendProcessResult),
+  ]
+
+example : 1 + 2 = 3 := rfl
+example (p: Prop): p → p := by simp
+
+def test_frontend_process_sorry : Test :=
+  let solved := "example : 1 + 2 = 3 := rfl\n"
+  let withSorry := "example (p: Prop): p → p := sorry"
+  [
+    let file := s!"{solved}{withSorry}"
+    let goal1: Protocol.Goal := {
+      name := "_uniq.6",
+      target := { pp? := .some "p → p" },
+      vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
+    }
+    step "frontend.process"
+      ({
+        file? := .some file,
+        sorrys := true,
+      }: Protocol.FrontendProcess)
+     ({
+       units := [{
+         boundary := (0, solved.utf8ByteSize),
+       }, {
+         boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
+         goalStateId? := .some 0,
+         goals? := .some #[goal1],
+         goalSrcBoundaries? := .some #[(57, 62)],
+         messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
+       }],
+     }: 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 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_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))
+
+
+end Pantograph.Test.Integration

Test/Library.lean

@@ -0,0 +1,41 @@
+import LSpec
+import Lean
+import Pantograph.Library
+import Test.Common
+
+open Lean
+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 ← 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 ← 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",
+        sexp? := "((:c PSigma) (:sort 0) (:lambda p (:sort 0) 0))",
+      },
+      expr := {
+        pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩",
+        sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall a 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))",
+      }
+    }))
+    return tests
+  runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("expr_echo", test_expr_echo env),
+  ]
+
+end Pantograph.Test.Library

Test/Main.lean

@@ -0,0 +1,60 @@
+import LSpec
+import Test.Delate
+import Test.Environment
+import Test.Frontend
+import Test.Integration
+import Test.Library
+import Test.Metavar
+import Test.Proofs
+import Test.Serial
+import Test.Tactic
+
+-- Test running infrastructure
+
+namespace Pantograph.Test
+
+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 (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))
+  let all := tasks.foldl (λ acc (name, task) =>
+    let v: Except IO.Error LSpec.TestSeq := Task.get task
+    match v with
+    | .ok case => acc ++ (LSpec.group name case)
+    | .error e => acc ++ (expectationFailure name e.toString)
+    ) LSpec.TestSeq.done
+  return all
+
+end Pantograph.Test
+
+open Pantograph.Test
+
+/-- Main entry of tests; Provide an argument to filter tests by prefix -/
+def main (args: List String) := do
+  let nameFilter? := args.head?
+  Lean.initSearchPath (← Lean.findSysroot)
+  let env_default: Lean.Environment ← Lean.importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
+
+  let suites: List (String × List (String × IO LSpec.TestSeq)) := [
+    ("Environment", Environment.suite),
+    ("Frontend", Frontend.suite env_default),
+    ("Integration", Integration.suite env_default),
+    ("Library", Library.suite env_default),
+    ("Metavar", Metavar.suite env_default),
+    ("Proofs", Proofs.suite env_default),
+    ("Delate", Delate.suite env_default),
+    ("Serial", Serial.suite env_default),
+    ("Tactic/Assign", Tactic.Assign.suite env_default),
+    ("Tactic/Prograde", Tactic.Prograde.suite env_default),
+  ]
+  let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
+  LSpec.lspecEachIO [()] (λ () => runTestGroup nameFilter? tests)

Test/Metavar.lean

@@ -0,0 +1,280 @@
+import LSpec
+import Pantograph.Goal
+import Pantograph.Delate
+import Test.Common
+import Lean
+
+namespace Pantograph.Test.Metavar
+open Pantograph
+open Lean
+
+abbrev TestM := TestT $ ReaderT Protocol.Options Elab.TermElabM
+
+-- Tests that all delay assigned mvars are instantiated
+def test_instantiate_mvar: TestM Unit := do
+  let env ← Lean.MonadEnv.getEnv
+  let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
+  let syn ← match parseTerm env value with
+    | .ok s => pure $ s
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let expr ← match ← elabTerm syn with
+    | .ok expr => pure $ expr
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let t ← Lean.Meta.inferType expr
+  addTest $ LSpec.check "typing" ((toString (← serializeExpressionSexp t)) =
+    "((: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
+  addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
+  match syn? with
+  | .error error =>
+    IO.println error
+    return Option.none
+  | .ok syn =>
+    let expr? ← elabType syn
+    addTest $ LSpec.check s!"Elaborating" expr?.isOk
+    match expr? with
+    | .error error =>
+      IO.println error
+      return Option.none
+    | .ok expr =>
+      let goal ← GoalState.create (expr := expr)
+      return Option.some goal
+
+def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
+  {
+    userName?,
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      userName := x.fst,
+      type? := .some { pp? := .some x.snd },
+    })).toArray
+  }
+def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
+  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
+
+  let coreContext: Lean.Core.Context ← createCoreContext #[]
+  let metaM := termElabM.run' (ctx := defaultElabContext)
+  let coreM := metaM.run'
+  match ← (coreM.run' coreContext { env := env }).toBaseIO with
+  | .error exception =>
+    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
+  | .ok (_, a) =>
+    return a
+
+/-- M-coupled goals -/
+def test_m_couple: TestM Unit := do
+  let state? ← startProof "(2: Nat) ≤ 5"
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+  -- Set m to 3
+  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
+  let state1b ← match state2.continue state1 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ 3", .some "3 ≤ 5"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+
+def test_m_couple_simp: TestM Unit := do
+  let state? ← startProof "(2: Nat) ≤ 5"
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true })
+  addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) =
+    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
+  addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
+    #[#["_uniq.38"], #["_uniq.38"], #[]])
+
+  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
+  let state1b ← match state2.continue state1 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ 2", .some "2 ≤ 5"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state4 ← match state3.continue state1b with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  state5.restoreMetaM
+  let root ← match state5.rootExpr? with
+    | .some e => pure e
+    | .none =>
+      addTest $ assertUnreachable "(5 root)"
+      return ()
+  let rootStr: String := toString (← Lean.Meta.ppExpr root)
+  addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
+  let unfoldedRoot ←  unfoldAuxLemmas root
+  addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) =
+    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
+  return ()
+
+def test_proposition_generation: TestM Unit := do
+  let state? ← startProof "Σ' p:Prop, p"
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      buildGoal [] "?fst" (userName? := .some "snd"),
+      buildGoal [] "Prop" (userName? := .some "fst")
+      ])
+  if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then
+    addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+
+  let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "?m.30 x"])
+  addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
+
+  let assign := "Eq.refl x"
+  let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[])
+
+  addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
+  return ()
+
+def test_partial_continuation: TestM Unit := do
+  let state? ← startProof "(2: Nat) ≤ 5"
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
+
+  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "apply Nat.succ" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "Nat"])
+
+  -- Execute a partial continuation
+  let coupled_goals := state1.goals ++ state2.goals
+  let state1b ← match state2.resume (goals := coupled_goals) with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+
+  -- Roundtrip
+  --let coupled_goals := coupled_goals.map (λ g =>
+  --  { name := str_to_name $ serializeName g.name (sanitize := false)})
+  let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false))
+  let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
+  let state1b ← match state2.resume (goals := coupled_goals) with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+
+  -- Continuation should fail if the state does not exist:
+  match state0.resume coupled_goals with
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
+  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
+  -- Continuation should fail if some goals have not been solved
+  match state2.continue state1 with
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Target state has unresolved goals")
+  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
+  return ()
+
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  let tests := [
+    ("Instantiate", test_instantiate_mvar),
+    ("2 < 5", test_m_couple),
+    ("2 < 5", test_m_couple_simp),
+    ("Proposition Generation", test_proposition_generation),
+    ("Partial Continuation", test_partial_continuation)
+  ]
+  tests.map (fun (name, test) => (name, proofRunner env test))
+
+end Pantograph.Test.Metavar

Test/Proofs.lean

@@ -0,0 +1,635 @@
+/-
+Tests pertaining to goals with no interdependencies
+-/
+import LSpec
+import Pantograph.Goal
+import Pantograph.Delate
+import Test.Common
+
+namespace Pantograph.Test.Proofs
+open Pantograph
+open Lean
+
+inductive Start where
+  | copy (name: String) -- Start from some name in the environment
+  | expr (expr: String) -- Start from some expression
+
+abbrev TestM := TestT $ ReaderT Protocol.Options $ Elab.TermElabM
+
+def startProof (start: Start): TestM (Option GoalState) := do
+  let env ← Lean.MonadEnv.getEnv
+  match start with
+  | .copy name =>
+    let cInfo? := name.toName |> env.find?
+    addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
+    match cInfo? with
+    | .some cInfo =>
+      let goal ← GoalState.create (expr := cInfo.type)
+      return Option.some goal
+    | .none =>
+      return Option.none
+  | .expr expr =>
+    let syn? := parseTerm env expr
+    addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
+    match syn? with
+    | .error error =>
+      IO.println error
+      return Option.none
+    | .ok syn =>
+      let expr? ← elabType syn
+      addTest $ LSpec.check s!"Elaborating" expr?.isOk
+      match expr? with
+      | .error error =>
+        IO.println error
+        return Option.none
+      | .ok expr =>
+        let goal ← GoalState.create (expr := expr)
+        return Option.some goal
+
+def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
+    (userName?: Option String := .none): Protocol.Goal :=
+  {
+    name,
+    userName?,
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      userName := x.fst,
+      type? := .some { pp? := .some x.snd },
+    })).toArray
+  }
+def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
+    Protocol.Goal :=
+  {
+    userName?,
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      userName := x.fst,
+      type? := .some { pp? := .some x.snd },
+    })).toArray
+  }
+def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
+  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
+
+  let coreContext: Lean.Core.Context ← createCoreContext #[]
+  let metaM := termElabM.run' (ctx := defaultElabContext)
+  let coreM := metaM.run'
+  match ← (coreM.run' coreContext { env := env }).toBaseIO with
+  | .error exception =>
+    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
+  | .ok (_, a) =>
+    return a
+
+def test_identity: TestM Unit := do
+  let state? ← startProof (.expr "∀ (p: Prop), p → p")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro p h"
+  let state1 ← match ← state0.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let inner := "_uniq.12"
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
+    #[inner])
+  let state1parent ← state1.withParentContext do
+    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
+example: ∀ (a b: Nat), a + b = b + a := by
+  intro n m
+  rw [Nat.add_comm]
+def test_nat_add_comm (manual: Bool): TestM Unit := do
+  let state? ← startProof <| match manual with
+    | false => .copy "Nat.add_comm"
+    | true => .expr "∀ (a b: Nat), a + b = b + a"
+  addTest $ LSpec.check "Start goal" state?.isSome
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let state1 ← match ← state0.tacticOn 0 "intro n m" with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])
+
+  match ← state1.tacticOn 0 "assumption" with
+  | .failure #[message] =>
+    addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
+  | other => do
+    addTest $ assertUnreachable $ other.toString
+
+  let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
+
+  return ()
+def test_delta_variable: TestM Unit := do
+  let options: Protocol.Options := { noRepeat := true }
+  let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
+  addTest $ LSpec.check "Start goal" state?.isSome
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
+    #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
+  let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) =
+    #[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"])
+  return ()
+  where
+-- Like `buildGoal` but allow certain variables to be elided.
+  buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
+    {
+      target := { pp? := .some target},
+      vars := (nameType.map fun x => ({
+        userName := x.fst,
+        type? := x.snd.map (λ type => { pp? := type }),
+      })).toArray
+    }
+
+example (w x y z : Nat) (p : Nat → Prop)
+        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
+  simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
+  assumption
+def test_arith: TestM Unit := do
+  let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intros"
+  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.goals.length = 1)
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+  let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
+  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
+  let tactic := "assumption"
+  let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test tactic state3.goals.isEmpty
+  addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
+  return ()
+
+-- Two ways to write the same theorem
+example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
+  intro p q h
+  cases h
+  apply Or.inr
+  assumption
+  apply Or.inl
+  assumption
+example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
+  intro p q h
+  cases h
+  . apply Or.inr
+    assumption
+  . apply Or.inl
+    assumption
+def test_or_comm: TestM Unit := do
+  let state? ← startProof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
+  addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
+
+  let tactic := "intro p q h"
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let [state1g0] := state1.goals | fail "Should have 1 goal"
+  let (fvP, fvQ, fvH) ← state1.withContext state1g0 do
+    let lctx ← getLCtx
+    let #[fvP, fvQ, fvH] := lctx.getFVarIds.map (toString ·.name) |
+      panic! "Incorrect number of decls"
+    pure (fvP, fvQ, fvH)
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
+    #[{
+      name := state1g0.name.toString,
+      target := { pp? := .some "q ∨ p" },
+      vars := #[
+        { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
+        { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" } },
+        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
+      ]
+    }])
+  addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
+  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
+
+  let state1parent ← state1.withParentContext do
+    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
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[branchGoal "inl" "p", branchGoal "inr" "q"])
+  let [state2g0, state2g1] := state2.goals |
+    fail s!"Should have 2 goals, but it has {state2.goals.length}"
+  let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
+  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!)
+  let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
+  let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
+  let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
+  let caseL := s!"(:lambda h (:fv {fvP}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))"
+  let caseR := s!"(:lambda h (:fv {fvQ}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))"
+  let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))"
+  addTest $ LSpec.test "(2 parent)" (state2parent ==
+    s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
+
+  let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state3_1parent ← state3_1.withParentContext do
+    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
+  let [state3_1goal0] := state3_1.goals | fail "Should have 1 goal"
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
+  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
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
+  let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
+  addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
+  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
+  let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
+  let state4_2 ← match ← state3_2.tacticOn (goalId := 0) (tactic := "assumption") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "  assumption" state4_2.goals.isEmpty
+  addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
+  -- Ensure the proof can continue from `state4_2`.
+  let state2b ← match state4_2.continue state2 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  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
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  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
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
+  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome
+
+  return ()
+  where
+    typeProp: Protocol.Expression := { pp? := .some "Prop" }
+    branchGoal (caseName varName: String): Protocol.Goal := {
+      userName? := .some caseName,
+      target := { pp? := .some "q ∨ p" },
+      vars := #[
+        { userName := "p", type? := .some typeProp },
+        { userName := "q", type? := .some typeProp },
+        { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible := true }
+      ]
+    }
+
+example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
+  intro a b c1 c2 h
+  conv =>
+    lhs
+    congr
+    . rw [Nat.add_comm]
+    . rfl
+  exact h
+
+def test_conv: TestM Unit := do
+  let state? ← startProof (.expr "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro a b c1 c2 h"
+  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) =
+    #[interiorGoal [] "a + b + c1 = b + a + c2"])
+
+  let state2 ← match ← state1.conv (state1.get! 0) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
+
+  let convTactic := "rhs"
+  let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
+
+  let convTactic := "lhs"
+  let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
+
+  let convTactic := "congr"
+  let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" },
+      { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" }
+    ])
+
+  let convTactic := "rw [Nat.add_comm]"
+  let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
+
+  let convTactic := "rfl"
+  let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  let state4_1 ← match state6_1.continue state4 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ expectationFailure "continue" e
+      return ()
+
+  let convTactic := "rfl"
+  let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  let state1_1 ← match ← state6.convExit with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  let tactic := "exact h"
+  let stateF ← match ← state1_1.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)).map (·.devolatilize) =
+    #[])
+
+  where
+    h := "b + a + c1 = b + a + c2"
+    interiorGoal (free: List (String × String)) (target: String) :=
+      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
+      buildGoal free target
+
+example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
+  intro a b c d h1 h2
+  calc a + b = b + c := by apply h1
+    _ = c + d := by apply h2
+
+def test_calc: TestM Unit := do
+  let state? ← startProof (.expr "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro a b c d h1 h2"
+  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) =
+    #[interiorGoal [] "a + b = c + d"])
+  let pred := "a + b = b + c"
+  let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      interiorGoal [] "a + b = b + c" (.some "calc"),
+      interiorGoal [] "b + c = c + d"
+    ])
+  addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
+  addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
+
+  let tactic := "apply h1"
+  let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state3 ← match state2m.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ expectationFailure "continue" e
+      return ()
+  let pred := "_ = c + d"
+  let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      interiorGoal [] "b + c = c + d" (.some "calc")
+    ])
+  addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
+  let tactic := "apply h2"
+  let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
+  where
+    interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
+      let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
+        ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
+      buildGoal free target userName?
+
+def test_tactic_failure_unresolved_goals : TestM Unit := do
+  let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro p"
+  let state1 ← match ← state0.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  let tactic := "exact ⟨0, by simp⟩"
+  let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
+  checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"]
+
+def test_tactic_failure_synthesize_placeholder : TestM Unit := do
+  let state? ← startProof (.expr "∀ (p q r : Prop) (h : p → q), q ∧ r")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro p q r h"
+  let state1 ← match ← state0.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  let 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))
+    #[
+      buildGoal [("p", "Prop"), ("q", "Prop"), ("hp", "p"), ("hq", "q")] "q ∧ p"
+    ]
+
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  let tests := [
+    ("identity", test_identity),
+    ("Nat.add_comm", test_nat_add_comm false),
+    ("Nat.add_comm manual", test_nat_add_comm true),
+    ("Nat.add_comm delta", test_delta_variable),
+    ("arithmetic", test_arith),
+    ("Or.comm", test_or_comm),
+    ("conv", test_conv),
+    ("calc", test_calc),
+    ("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))
+
+
+
+end Pantograph.Test.Proofs

Test/Serial.lean

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

Test/Tactic.lean

@@ -0,0 +1,2 @@
+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/Prograde.lean

@@ -0,0 +1,300 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.Prograde
+
+def test_define : TestT Elab.TermElabM Unit := do
+  let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
+  let expr ← parseSentence expr
+  Meta.forallTelescope expr $ λ _ body => do
+    let e ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := "Or.inl h")
+      (fileName := ← getFileName) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let target: Expr := mkAnd
+      (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
+      (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
+    let h := .fvar ⟨uniq 8⟩
+    addTest $ LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == {
+      context := #[
+        cdeclOf `p (.sort 0),
+        cdeclOf `q (.sort 0),
+        cdeclOf `h h
+      ],
+      target,
+    })
+    let tactic := Tactic.evalDefine `h2 e
+    let m := .mvar ⟨uniq 13⟩
+    let [newGoal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number"
+    addTest $ LSpec.test "goals after" ((← toCondensedGoal newGoal).devolatilize == {
+      context := #[
+        cdeclOf `p (.sort 0),
+        cdeclOf `q (.sort 0),
+        cdeclOf `h h,
+        {
+          userName := `h2,
+          type := mkOr h m,
+          value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩)
+        }
+      ],
+      target,
+    })
+    let .some e ← getExprMVarAssignment? goal.mvarId! | panic! "Tactic must assign"
+    addTest $ LSpec.test "assign" e.isLet
+
+def test_define_proof : TestT Elab.TermElabM Unit := do
+  let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "intro p q h"
+  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).map (·.devolatilize) =
+    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
+
+  let expr := "Or.inl (Or.inl h)"
+  let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let evalBind := "y"
+  let evalExpr := "Or.inl h"
+  let state2 ← match ← state1.tryDefine (state1.get! 0) (binderName := evalBind) (expr := evalExpr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"eval {evalBind} := {evalExpr}" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[{
+      target := { pp? := .some  "(p ∨ q) ∨ p ∨ q"},
+      vars := #[
+        { userName := "p", type? := .some { pp? := .some "Prop" } },
+        { userName := "q", type? := .some { pp? := .some "Prop" } },
+        { userName := "h", type? := .some { pp? := .some "p" } },
+        { userName := "y",
+          type? := .some { pp? := .some "p ∨ ?m.19" },
+          value? := .some { pp? := .some "Or.inl h" },
+        }
+      ]
+  }])
+
+  let expr := "Or.inl y"
+  let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
+
+def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
+  intro p x
+  apply x.fst
+  exact 5
+
+def test_define_root_expr : TestT Elab.TermElabM Unit := do
+  --let rootExpr ← parseSentence "Nat"
+  --let state0 ← GoalState.create rootExpr
+  --let .success state1 ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
+  --let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
+  --addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
+  let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "intro p x"
+  let .success state1 ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let binderName := `binder
+  let value := "x.fst"
+  let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
+  let tacticM := Tactic.evalDefine binderName expr
+  let .success state2 ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
+  let tactic := s!"apply {binderName}"
+  let .success state3 ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let tactic := s!"exact 5"
+  let .success state4 ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
+  addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n  let binder := x.fst;\n  binder 5")
+
+--set_option pp.all true
+--#check @PSigma (α := Prop) (β := λ (p: Prop) => p)
+--def test_define_root_expr : TestT Elab.TermElabM Unit := do
+
+def test_have_proof : TestT Elab.TermElabM Unit := do
+  let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "intro p q h"
+  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).map (·.devolatilize) =
+    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
+
+  let expr := "Or.inl (Or.inl h)"
+  let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let haveBind := "y"
+  let haveType := "p ∨ q"
+  let state2 ← match ← state1.tryHave (state1.get! 0) (binderName := haveBind) (type := haveType) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[
+      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q",
+      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q"
+    ])
+
+  let expr := "Or.inl h"
+  let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let state2b ← match state3.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let expr := "Or.inl y"
+  let state4 ← match ← state2b.tryAssign (state2b.get! 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
+  addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p q h y => Or.inl y")
+
+def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
+  let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "intro a p h"
+  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).map (·.devolatilize) =
+    #[{
+      target := { pp? := .some mainTarget },
+      vars := interiorVars,
+    }])
+
+  let letType := "Nat"
+  let expr := s!"let b: {letType} := _; _"
+  let result2 ← match specialized with
+    | true => state1.tryLet (state1.get! 0) (binderName := "b") (type := letType)
+    | false => state1.tryAssign (state1.get! 0) (expr := expr)
+  let state2 ← match result2 with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let serializedState2 ← state2.serializeGoals
+  let letBindName := if specialized then "b" else "_1"
+  addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
+    #[{
+      target := { pp? := .some letType },
+      vars := interiorVars,
+      userName? := .some letBindName
+    },
+    {
+      target := { pp? := .some mainTarget },
+      vars := interiorVars ++ #[{
+        userName := "b",
+        type? := .some { pp? := .some letType },
+        value? := .some { pp? := .some s!"?{letBindName}" },
+      }],
+      userName? := if specialized then .none else .some "_2",
+    }
+    ])
+
+  let tactic := "exact 1"
+  let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3.serializeGoals).map (·.devolatilize) = #[])
+
+  let state3r ← match state3.continue state2 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals).map (·.devolatilize) =
+    #[
+    {
+      target := { pp? := .some mainTarget },
+      vars := interiorVars ++ #[{
+        userName := "b",
+        type? := .some { pp? := .some "Nat" },
+        value? := .some { pp? := .some "1" },
+      }],
+      userName? := if specialized then .none else .some "_2",
+    }
+    ])
+
+  let tactic := "exact h"
+  match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
+  | .failure #[message] =>
+    addTest $ LSpec.check tactic  (message = s!"type mismatch\n  h\nhas type\n  a : Prop\nbut is expected to have type\n  {mainTarget} : Prop")
+  | other => do
+    addTest $ assertUnreachable $ other.toString
+
+  let tactic := "exact Or.inl (Or.inl h)"
+  let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(4 root)" state4.rootExpr?.isSome
+  where
+    mainTarget := "(a ∨ p) ∨ a ∨ p"
+    interiorVars: Array Protocol.Variable := #[
+        { userName := "a", type? := .some { pp? := .some "Prop" }, },
+        { userName := "p", type? := .some { pp? := .some "Prop" }, },
+        { userName := "h", type? := .some { pp? := .some "a" }, }
+      ]
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("define", test_define),
+    ("define proof", test_define_proof),
+    ("define root expr", test_define_root_expr),
+    ("have proof", test_have_proof),
+    ("let via assign", test_let false),
+    ("let via tryLet", test_let true),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.Prograde

doc/icon.svg

@@ -0,0 +1,157 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+
+<svg
+   width="256"
+   height="256"
+   viewBox="0 0 67.733332 67.733333"
+   version="1.1"
+   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="namedview1"
+     pagecolor="#ffffff"
+     bordercolor="#111111"
+     borderopacity="1"
+     inkscape:showpageshadow="0"
+     inkscape:pageopacity="0"
+     inkscape:pagecheckerboard="1"
+     inkscape:deskcolor="#d1d1d1"
+     inkscape:document-units="px"
+     showguides="true"
+     inkscape:zoom="5.1882633"
+     inkscape:cx="81.819286"
+     inkscape:cy="132.22151"
+     inkscape:window-width="3774"
+     inkscape:window-height="2126"
+     inkscape:window-x="0"
+     inkscape:window-y="0"
+     inkscape:window-maximized="1"
+     inkscape:current-layer="layer2">
+    <sodipodi:guide
+       position="33.866666,69.8437"
+       orientation="-1,0"
+       id="guide1"
+       inkscape:locked="false"
+       inkscape:label=""
+       inkscape:color="rgb(0,134,229)" />
+    <sodipodi:guide
+       position="-27.673679,33.866666"
+       orientation="0,1"
+       id="guide2"
+       inkscape:locked="false"
+       inkscape:label=""
+       inkscape:color="rgb(0,134,229)" />
+    <sodipodi:guide
+       position="16.933333,29.94582"
+       orientation="-1,0"
+       id="guide3"
+       inkscape:locked="false"
+       inkscape:label=""
+       inkscape:color="rgb(0,134,229)" />
+    <sodipodi:guide
+       position="50.799999,37.44627"
+       orientation="-1,0"
+       id="guide4"
+       inkscape:locked="false"
+       inkscape:label=""
+       inkscape:color="rgb(0,134,229)" />
+    <sodipodi:guide
+       position="31.336956,16.933333"
+       orientation="0,1"
+       id="guide5"
+       inkscape:locked="false"
+       inkscape:label=""
+       inkscape:color="rgb(0,134,229)" />
+    <sodipodi:guide
+       position="24.528038,25.4"
+       orientation="0,1"
+       id="guide6"
+       inkscape:locked="false"
+       inkscape:label=""
+       inkscape:color="rgb(0,134,229)" />
+    <sodipodi:guide
+       position="33.866666,50.799999"
+       orientation="0,1"
+       id="guide7"
+       inkscape:locked="false"
+       inkscape:label=""
+       inkscape:color="rgb(0,134,229)" />
+    <sodipodi:guide
+       position="32.770414,55.033333"
+       orientation="0,1"
+       id="guide8"
+       inkscape:locked="false"
+       inkscape:label=""
+       inkscape:color="rgb(0,134,229)" />
+    <sodipodi:guide
+       position="25.347689,33.866666"
+       orientation="1,0"
+       id="guide9"
+       inkscape:locked="false" />
+    <sodipodi:guide
+       position="25.347689,42.333333"
+       orientation="0,1"
+       id="guide10"
+       inkscape:locked="false"
+       inkscape:label=""
+       inkscape:color="rgb(0,134,229)" />
+  </sodipodi:namedview>
+  <defs
+     id="defs1" />
+  <g
+     inkscape:groupmode="layer"
+     id="layer4"
+     inkscape:label="bg" />
+  <g
+     inkscape:groupmode="layer"
+     id="layer1"
+     inkscape:label="Circle">
+    <path
+       id="path1"
+       style="fill:#666b98;fill-rule:evenodd;stroke:#ffffff;stroke-width:0.0191989;stroke-miterlimit:3.4;fill-opacity:1"
+       d="M 33.866666 0.009818522 A 33.857067 33.857067 0 0 0 0.009818522 33.866666 A 33.857067 33.857067 0 0 0 33.866666 67.723514 A 33.857067 33.857067 0 0 0 67.723514 33.866666 A 33.857067 33.857067 0 0 0 33.866666 0.009818522 z M 33.866666 4.2416015 A 29.624933 29.624933 0 0 1 63.491731 33.866666 A 29.624933 29.624933 0 0 1 33.866666 63.491731 A 29.624933 29.624933 0 0 1 4.2416015 33.866666 A 29.624933 29.624933 0 0 1 33.866666 4.2416015 z " />
+  </g>
+  <g
+     inkscape:groupmode="layer"
+     id="layer2"
+     inkscape:label="Pantograph-Core">
+    <rect
+       style="fill:#666b98;fill-opacity:1;fill-rule:evenodd;stroke:#ffffff;stroke-width:0.01905;stroke-miterlimit:3.4"
+       id="rect8"
+       width="16.942858"
+       height="4.2257233"
+       x="33.866665"
+       y="12.7"
+       rx="0.58070719"
+       ry="0.34097314" />
+    <rect
+       style="fill:#666b98;fill-opacity:1;fill-rule:evenodd;stroke:#ffffff;stroke-width:0.01905;stroke-miterlimit:3.4"
+       id="rect1"
+       width="33.885715"
+       height="8.4211359"
+       x="16.933332"
+       y="42.333332"
+       rx="0.58070719"
+       ry="0.34097314" />
+    <path
+       style="fill:#666b98;fill-opacity:1;stroke:none;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+       d="m 42.338095,16.925724 -16.990406,8.474275 13.121218,16.923808 -4.602241,0.0095 -4.254289,0.0015 -8.564029,-16.934789 17.310554,-8.464751 z"
+       id="path10"
+       sodipodi:nodetypes="cccccccc" />
+    <path
+       style="fill:none;stroke:#666b98;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+       d="M 46.53445,16.925724 26.018901,26.73418"
+       id="path11" />
+    <path
+       style="fill:none;stroke:#666b98;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+       d="m 21.048348,25.399999 4.352167,16.934808"
+       id="path12"
+       sodipodi:nodetypes="cc" />
+  </g>
+</svg>

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

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

flake.lock

@@ -0,0 +1,113 @@
+{
+  "nodes": {
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib"
+      },
+      "locked": {
+        "lastModified": 1743550720,
+        "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "c621e8422220273271f52058f618c94e405bb0f5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "flake-parts_2": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib_2"
+      },
+      "locked": {
+        "lastModified": 1727826117,
+        "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "lean4-nix": {
+      "inputs": {
+        "flake-parts": "flake-parts_2",
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1743534244,
+        "narHash": "sha256-WnoYs2iyrfgh35eXErCOyos8E2YbW3LT1xm/EtT88/k=",
+        "owner": "lenianiva",
+        "repo": "lean4-nix",
+        "rev": "5eb7f03be257e327fdb3cca9465392e68dc28a4d",
+        "type": "github"
+      },
+      "original": {
+        "owner": "lenianiva",
+        "repo": "lean4-nix",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1743975612,
+        "narHash": "sha256-o4FjFOUmjSRMK7dn0TFdAT0RRWUWD+WsspPHa+qEQT8=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "a880f49904d68b5e53338d1e8c7bf80f59903928",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-24.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-lib": {
+      "locked": {
+        "lastModified": 1743296961,
+        "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=",
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "type": "github"
+      }
+    },
+    "nixpkgs-lib_2": {
+      "locked": {
+        "lastModified": 1727825735,
+        "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
+      },
+      "original": {
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "lean4-nix": "lean4-nix",
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,125 @@
+{
+  description = "Pantograph";
+
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11";
+    flake-parts.url = "github:hercules-ci/flake-parts";
+    lean4-nix = {
+      url = "github:lenianiva/lean4-nix";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
+  };
+
+  outputs = inputs @ {
+    self,
+    nixpkgs,
+    flake-parts,
+    lean4-nix,
+    ...
+  }:
+    flake-parts.lib.mkFlake {inherit inputs;} {
+      flake = {
+      };
+      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

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

lakefile.lean

@@ -1,19 +1,29 @@
 import Lake
 open Lake DSL
 
-
-package pantograph {
-  -- add package configuration options here
-}
-
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @  "8e5a00a8afc8913c0584cb85f37951995275fd87"
+package pantograph
 
 lean_lib Pantograph {
-  -- add library configuration options here
+  roots := #[`Pantograph]
+  defaultFacets := #[LeanLib.sharedFacet]
 }
 
-@[default_target]
-lean_exe pantograph {
-  root := `Main
+lean_lib Repl {
+}
+@[default_target]
+lean_exe repl {
+  root := `Main
+  -- Solves the native symbol not found problem
+  supportInterpreter := true
+}
+
+require LSpec from git
+  "https://github.com/argumentcomputer/LSpec.git" @ "a6652a48b5c67b0d8dd3930fad6390a97d127e8d"
+lean_lib Test {
+}
+@[test_driver]
+lean_exe test {
+  root := `Test.Main
+  -- Solves the native symbol not found problem
+  supportInterpreter := true
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-05-06
+leanprover/lean4:v4.18.0