chore: Update flake

Reviewed-on: #81

.gitignore

@@ -1,2 +1,6 @@
+.*
+!.gitignore
+
+*.olean
 /build
 /lake-packages

Main.lean

@@ -1,4 +1,66 @@
+import Lean.Data.Json
+import Lean.Environment
+
+import Pantograph.Version
+import Pantograph.Library
 import Pantograph
 
-def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
+-- Main IO functions
+open Pantograph
+
+/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
+def parseCommand (s: String): Except String Protocol.Command := do
+  let s := s.trim
+  match s.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
+  let state ← get
+  let command ← (← IO.getStdin).getLine
+  if command.trim.length = 0 then return ()
+  match parseCommand command with
+  | .error error =>
+    let error  := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError)
+    -- Using `Lean.Json.compress` here to prevent newline
+    IO.println error.compress
+  | .ok command =>
+    let ret ← execute command
+    let str := match state.options.printJsonPretty with
+      | true => ret.pretty
+      | false => ret.compress
+    IO.println str
+  loop
+
+
+unsafe def main (args: List String): IO Unit := do
+  -- NOTE: A more sophisticated scheme of command line argument handling is needed.
+  -- Separate imports and options
+  if args == ["--version"] then do
+    println! s!"{version}"
+    return
+
+  initSearch ""
+
+  let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
+    |>.toArray |> createCoreContext
+  let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
+  let coreState ← createCoreState imports.toArray
+  let context: Context := {
+    imports
+  }
+  try
+    let coreM := loop.run context |>.run' {}
+    IO.println "ready."
+    discard <| coreM.toIO coreContext coreState
+  catch ex =>
+    IO.println "Uncaught IO exception"
+    IO.println ex.toString

Makefile

@@ -0,0 +1,20 @@
+LIB := ./.lake/build/lib/Pantograph.olean
+EXE := ./.lake/build/bin/pantograph
+SOURCE := $(wildcard *.lean Pantograph/*.lean Pantograph/**/*.lean) lean-toolchain
+
+TEST_EXE := ./.lake/build/bin/test
+TEST_SOURCE := $(wildcard Test/*.lean Test/**/*.lean)
+
+$(LIB) $(EXE): $(SOURCE)
+	lake build pantograph
+
+$(TEST_EXE): $(LIB) $(TEST_SOURCE)
+	lake build test
+
+test: $(TEST_EXE)
+	$(TEST_EXE)
+
+clean:
+	lake clean
+
+.PHONY: test clean

Pantograph.lean

@@ -1 +1,211 @@
-def hello := "world"
+import Lean.Data.HashMap
+import Pantograph.Compile
+import Pantograph.Environment
+import Pantograph.Goal
+import Pantograph.Library
+import Pantograph.Protocol
+import Pantograph.Serial
+
+namespace Pantograph
+
+structure Context where
+  imports: List String
+
+/-- Stores state of the REPL -/
+structure State where
+  options: Protocol.Options := {}
+  nextId: Nat := 0
+  goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
+
+/-- Main state monad for executing commands -/
+abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
+-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
+-- certain monadic features in `MainM`
+abbrev CR α := Except Protocol.InteractionError α
+
+def execute (command: Protocol.Command): MainM Lean.Json := do
+  let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
+    match Lean.fromJson? command.payload with
+    | .ok args => do
+      match (← comm args) with
+      | .ok result =>  return Lean.toJson result
+      | .error ierror => return Lean.toJson ierror
+    | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
+  match command.cmd with
+  | "reset"         => run reset
+  | "stat"          => run stat
+  | "expr.echo"     => run expr_echo
+  | "env.catalog"   => run env_catalog
+  | "env.inspect"   => run env_inspect
+  | "env.add"       => run env_add
+  | "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
+  | "compile.unit"  => run compile_unit
+  | cmd =>
+    let error: Protocol.InteractionError :=
+      errorCommand s!"Unknown command {cmd}"
+    return Lean.toJson error
+  where
+  errorCommand := errorI "command"
+  errorIndex := errorI "index"
+  -- Command Functions
+  reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
+    let state ← get
+    let nGoals := state.goalStates.size
+    set { state with nextId := 0, goalStates := Lean.HashMap.empty }
+    return .ok { nGoals }
+  stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
+    let state ← get
+    let nGoals := state.goalStates.size
+    return .ok { nGoals }
+  env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
+    let result ← Environment.catalog args
+    return .ok result
+  env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
+    let state ← get
+    Environment.inspect args state.options
+  env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
+    Environment.addDecl args
+  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
+    let state ← get
+    exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
+  options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
+    let state ← get
+    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
+      }
+    }
+    return .ok {  }
+  options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
+    return .ok (← get).options
+  goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
+    let state ← get
+    let env ← Lean.MonadEnv.getEnv
+    let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
+      | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
+      | .none, .some copyFrom =>
+        (match env.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 => return .error error
+    | .ok goalState =>
+      let stateId := state.nextId
+      set { state with
+        goalStates := state.goalStates.insert stateId goalState,
+        nextId := state.nextId + 1
+      }
+      return .ok { stateId, root := goalState.root.name.toString }
+  goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
+    let state ← get
+    match state.goalStates.find? args.stateId with
+    | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
+    | .some goalState => do
+      let nextGoalState?: Except _ GoalState ←
+        match args.tactic?, args.expr?, args.have?, args.calc?, args.conv?  with
+        | .some tactic, .none, .none, .none, .none => do
+          pure ( Except.ok (← goalTactic goalState args.goalId tactic))
+        | .none, .some expr, .none, .none, .none => do
+          pure ( Except.ok (← goalAssign goalState args.goalId expr))
+        | .none, .none, .some type, .none, .none => do
+          let binderName := args.binderName?.getD ""
+          pure ( Except.ok (← goalHave goalState args.goalId binderName type))
+        | .none, .none, .none, .some pred, .none => do
+          pure ( Except.ok (← goalCalc goalState args.goalId pred))
+        | .none, .none, .none, .none, .some true => do
+          pure ( Except.ok (← goalConv goalState args.goalId))
+        | .none, .none, .none, .none, .some false => do
+          pure ( Except.ok (← goalConvExit goalState))
+        | _, _, _, _, _ => pure (Except.error <|
+          errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied")
+      match nextGoalState? with
+      | .error error => return .error error
+      | .ok (.success nextGoalState) =>
+        let nextStateId := state.nextId
+        set { state with
+          goalStates := state.goalStates.insert state.nextId nextGoalState,
+          nextId := state.nextId + 1,
+        }
+        let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
+        return .ok {
+          nextStateId? := .some nextStateId,
+          goals? := .some goals,
+        }
+      | .ok (.parseError message) =>
+        return .ok { parseError? := .some message }
+      | .ok (.indexError goalId) =>
+        return .error $ errorIndex s!"Invalid goal id index {goalId}"
+      | .ok (.invalidAction message) =>
+        return .error $ errorI "invalid" message
+      | .ok (.failure messages) =>
+        return .ok { tacticErrors? := .some messages }
+  goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
+    let state ← get
+    match state.goalStates.find? args.target with
+    | .none => return .error $ errorIndex s!"Invalid state index {args.target}"
+    | .some target => do
+      let nextState? ← match args.branch?, args.goals? with
+        | .some branchId, .none => do
+          match state.goalStates.find? branchId with
+          | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
+          | .some branch => pure $ goalContinue target branch
+        | .none, .some goals =>
+          pure $ goalResume target goals
+        | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
+      match nextState? with
+      | .error error => return .error <| errorI "structure" error
+      | .ok nextGoalState =>
+        let nextStateId := state.nextId
+        set { state with
+          goalStates := state.goalStates.insert nextStateId nextGoalState,
+          nextId := state.nextId + 1
+        }
+        let goals ← goalSerialize nextGoalState (options := state.options)
+        return .ok {
+          nextStateId,
+          goals,
+        }
+  goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
+    let state ← get
+    let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
+    set { state with goalStates }
+    return .ok {}
+  goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
+    let state ← get
+    match state.goalStates.find? args.stateId with
+    | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
+    | .some goalState => runMetaM <| do
+      return .ok (← goalPrint goalState state.options)
+  compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do
+    let module := args.module.toName
+    try
+      let steps ← Compile.processSource module
+      let units? := if args.compilationUnits then
+          .some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
+        else
+          .none
+      let invocations? ← if args.invocations then
+          pure $ .some (← Compile.collectTacticsFromCompilation steps)
+        else
+          pure .none
+      return .ok { units?, invocations? }
+    catch e =>
+      return .error $ errorI "compile" (← e.toMessageData.toString)
+
+end Pantograph

Pantograph/Compile.lean

@@ -0,0 +1,25 @@
+/- Adapted from lean-training-data by semorrison -/
+import Pantograph.Protocol
+import Pantograph.Compile.Frontend
+import Pantograph.Compile.Elab
+
+
+open Lean
+
+namespace Pantograph.Compile
+
+def collectTacticsFromCompilation (steps : List CompilationStep) : IO (List Protocol.InvokedTactic) := do
+  let infoTrees := steps.bind (·.trees)
+  let tacticInfoTrees := infoTrees.bind λ tree => tree.filter λ
+    | info@(.ofTacticInfo _) => info.isOriginal
+    | _ => false
+  let tactics := tacticInfoTrees.bind collectTactics
+  tactics.mapM λ invocation => do
+    let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
+    let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
+    let tactic ← invocation.ctx.runMetaM {} do
+      let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
+      return t.pretty
+    return { goalBefore, goalAfter, tactic }
+
+end Pantograph.Compile

Pantograph/Compile/Elab.lean

@@ -0,0 +1,146 @@
+
+import Lean.Elab.Import
+import Lean.Elab.Command
+import Lean.Elab.InfoTree
+
+import Pantograph.Compile.Frontend
+
+open Lean
+
+namespace Lean.Elab.Info
+/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
+protected def stx? : Info → Option Syntax
+  | .ofTacticInfo         info => info.stx
+  | .ofTermInfo           info => info.stx
+  | .ofCommandInfo        info => info.stx
+  | .ofMacroExpansionInfo info => info.stx
+  | .ofOptionInfo         info => info.stx
+  | .ofFieldInfo          info => info.stx
+  | .ofCompletionInfo     info => info.stx
+  | .ofUserWidgetInfo     info => info.stx
+  | .ofCustomInfo         info => info.stx
+  | .ofFVarAliasInfo      _    => none
+  | .ofFieldRedeclInfo    info => info.stx
+  | .ofOmissionInfo       info => info.stx
+/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
+protected def isOriginal (i : Info) : Bool :=
+  match i.stx? with
+  | none => true   -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
+  | some stx => match stx.getHeadInfo with
+    | .original .. => true
+    | _ => false
+end Lean.Elab.Info
+
+namespace Lean.Elab.TacticInfo
+
+/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
+def name? (t : TacticInfo) : Option Name :=
+  match t.stx with
+  | Syntax.node _ n _ => some n
+  | _ => none
+/-- Decide whether a tactic is "substantive",
+or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
+def isSubstantive (t : TacticInfo) : Bool :=
+  match t.name? with
+  | none => false
+  | some `null => false
+  | some ``cdot => false
+  | some ``cdotTk => false
+  | some ``Lean.Parser.Term.byTactic => false
+  | some ``Lean.Parser.Tactic.tacticSeq => false
+  | some ``Lean.Parser.Tactic.tacticSeq1Indented => false
+  | some ``Lean.Parser.Tactic.«tactic_<;>_» => false
+  | some ``Lean.Parser.Tactic.paren => false
+  | _ => true
+
+end Lean.Elab.TacticInfo
+
+namespace Lean.Elab.InfoTree
+
+/--
+Keep `.node` nodes and `.hole` nodes satisfying predicates.
+
+Returns a `List InfoTree`, although in most situations this will be a singleton.
+-/
+partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
+    InfoTree → List InfoTree
+  | .context ctx tree => tree.filter p m |>.map (.context ctx)
+  | .node info children =>
+    if p info then
+      [.node info (children.toList.map (filter p m)).join.toPArray']
+    else
+      (children.toList.map (filter p m)).join
+  | .hole mvar => if m mvar then [.hole mvar] else []
+
+end Lean.Elab.InfoTree
+
+
+namespace Pantograph.Compile
+
+-- Info tree filtering functions
+
+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. -/
+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))
+
+end TacticInvocation
+
+/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
+partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
+    List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
+  match t with
+  | .context inner t => findAllInfo t (inner.mergeIntoOuter? ctx) pred
+  | .node i children  =>
+      (if pred i then [(i, ctx, children)] else []) ++ children.toList.bind (fun t => findAllInfo t ctx pred)
+  | _ => []
+
+/-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
+each equipped with its relevant `ContextInfo`, and any children info trees. -/
+def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
+  let infos := findAllInfo t none 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
+
+
+end Pantograph.Compile

Pantograph/Compile/Frontend.lean

@@ -0,0 +1,86 @@
+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`.
+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.Compile
+
+structure CompilationStep where
+  fileName : String
+  fileMap : FileMap
+  src : Substring
+  stx : Syntax
+  before : Environment
+  after : Environment
+  msgs : List Message
+  trees : List Elab.InfoTree
+
+
+/--
+Process one command, returning a `CompilationStep` and
+`done : Bool`, indicating whether this was the last command.
+-/
+def processOneCommand: Elab.Frontend.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 ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
+
+partial def processFile : Elab.Frontend.FrontendM (List CompilationStep) := do
+  let (cmd, done) ← processOneCommand
+  if done then
+    return [cmd]
+  else
+    return cmd :: (← processFile)
+
+
+def findSourcePath (module : Name) : IO System.FilePath := do
+  return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean"
+
+def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) := unsafe do
+  let file ← IO.FS.readFile (← findSourcePath module)
+  let inputCtx := Parser.mkInputContext file module.toString
+
+  let (header, parserState, messages) ← Parser.parseHeader inputCtx
+  let (env, messages) ← Elab.processHeader header opts messages inputCtx
+  let commandState := Elab.Command.mkState env messages opts
+  processFile.run { inputCtx }
+    |>.run' {
+    commandState := { commandState with infoState.enabled := true },
+    parserState,
+    cmdPos := parserState.pos
+  }
+
+
+end Pantograph.Compile

Pantograph/Environment.lean

@@ -0,0 +1,144 @@
+import Pantograph.Protocol
+import Pantograph.Serial
+import Lean
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Environment
+
+def isNameInternal (n: Lean.Name): Bool :=
+  -- Returns true if the name is an implementation detail which should not be shown to the user.
+  isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes
+  where
+  isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
+    | .str _ name => name == "Lean"
+    | _ => true
+
+def toCompactSymbolName (n: Lean.Name) (info: Lean.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 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): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
+  let env ← Lean.MonadEnv.getEnv
+  let name :=  args.name.toName
+  let info? := env.find? name
+  let info ← match info? with
+    | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
+    | some info => pure info
+  let module? := env.getModuleIdxFor? name >>=
+    (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
+  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),
+    -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
+    typeDependency? := if args.dependency?.getD false
+      then .some <| type.getUsedConstants.map (λ n => serializeName n)
+      else .none,
+    valueDependency? := if args.dependency?.getD false
+      then value?.map (λ e =>
+        e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
+      else .none,
+    module? := module?
+  }
+  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
+  return .ok result
+def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
+  let env ← Lean.MonadEnv.getEnv
+  let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
+    let type ← match parseTerm env args.type with
+      | .ok syn => do
+        match ← elabTerm syn with
+        | .error e => return .error e
+        | .ok expr => pure expr
+      | .error e => return .error e
+    let value ← match parseTerm env args.value with
+      | .ok syn => do
+        try
+          let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
+          Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
+          let expr ← instantiateMVars expr
+          pure $ expr
+        catch ex => return .error (← ex.toMessageData.toString)
+      | .error e => return .error e
+    pure $ .ok (type, value)
+  let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
+    | .ok t => pure t
+    | .error e => return .error $ Protocol.errorExpr e
+  let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
+    (name := args.name.toName)
+    (levelParams := [])
+    (type := type)
+    (value := value)
+    (hints := Lean.mkReducibilityHintsRegularEx 1)
+    (safety := Lean.DefinitionSafety.safe)
+    (all := [])
+  let env' ← match env.addDecl (← getOptions) constant with
+    | .error e => do
+      let options ← Lean.MonadOptions.getOptions
+      let desc ← (e.toMessageData options).toString
+      return .error $ { error := "kernel", desc }
+    | .ok env' => pure env'
+  Lean.MonadEnv.modifyEnv (λ _ => env')
+  return .ok {}
+
+end Pantograph.Environment

Pantograph/Expr.lean

@@ -0,0 +1,140 @@
+import Lean
+
+open Lean
+
+namespace Pantograph
+
+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. -/
+def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
+  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
+
+/--
+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 (eOrig: Expr) : MetaM Expr := do
+  --let padding := String.join $ List.replicate level "│ "
+  --IO.println s!"{padding}Starting {toString eOrig}"
+  let mut result ← Meta.transform (← instantiateMVars eOrig)
+    (pre := fun e => e.withApp fun f args => do
+      let .mvar mvarId := f | return .continue
+      --IO.println s!"{padding}├V {e}"
+      let mvarDecl ← mvarId.getDecl
+
+      -- 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
+
+      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!"Local context variable violation: {violations}"
+
+      if let .some assign ← getExprMVarAssignment? mvarId then
+        --IO.println s!"{padding}├A ?{mvarId.name}"
+        assert! !(← mvarId.isDelayedAssigned)
+        return .visit (mkAppN assign args)
+      else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
+        --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
+        --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
+
+        if args.size < fvars.size then
+          throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
+        --if !args.isEmpty then
+          --IO.println s!"{padding}├── Arguments Begin"
+        let args ← args.mapM self
+        --if !args.isEmpty then
+          --IO.println s!"{padding}├── Arguments End"
+        if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
+          --IO.println s!"{padding}├T1"
+          let result := mkAppN f args
+          return .done result
+
+        let pending ← mvarIdPending.withContext do
+          let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
+          --IO.println s!"{padding}├Pre: {inner}"
+          pure <| (← inner.abstractM fvars).instantiateRev args
+
+        -- Tail arguments
+        let result := mkAppRange pending fvars.size args.size args
+        --IO.println s!"{padding}├MD {result}"
+        return .done result
+      else
+        assert! !(← mvarId.isAssigned)
+        assert! !(← mvarId.isDelayedAssigned)
+        --if !args.isEmpty then
+        --  IO.println s!"{padding}├── Arguments Begin"
+        let args ← args.mapM self
+        --if !args.isEmpty then
+        --  IO.println s!"{padding}├── Arguments End"
+
+        --IO.println s!"{padding}├M ?{mvarId.name}"
+        return .done (mkAppN f args))
+  --IO.println s!"{padding}└Result {result}"
+  return result
+  where
+  self e := instantiateDelayedMVars e --(level := level + 1)
+
+/--
+Convert an expression to an equiavlent form with
+1. No nested delayed assigned mvars
+2. No aux lemmas
+3. No assigned mvars
+ -/
+@[export pantograph_instantiate_all_meta_m]
+def instantiateAll (e: Expr): MetaM Expr := do
+  let e ← instantiateDelayedMVars e
+  let e ← unfoldAuxLemmas 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_meta_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: HashMap FVarId Expr := 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.find? 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,
+  }
+
+end Pantograph

Pantograph/Goal.lean

@@ -0,0 +1,536 @@
+/-
+Functions for handling metavariables
+
+All the functions starting with `try` resume their inner monadic state.
+-/
+import Pantograph.Protocol
+import Pantograph.Tactic
+import Lean
+
+
+namespace Pantograph
+open Lean
+
+def filename: String := "<pantograph>"
+
+/--
+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
+  -- New metavariables acquired in this state
+  newMVars: SSet MVarId
+
+  -- Parent state metavariable source
+  parentMVar?: Option MVarId
+
+  -- Existence of this field shows that we are currently in `conv` mode.
+  convMVar?: Option (MVarId × 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 Expr := .none
+
+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 goal ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)
+  let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
+  let root := goal.mvarId!
+  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
+  return {
+    root,
+    savedState,
+    newMVars := SSet.insert .empty root,
+    parentMVar? := .none,
+  }
+protected def GoalState.isConv (state: GoalState): Bool :=
+  state.convMVar?.isSome
+protected def GoalState.goals (state: GoalState): List MVarId :=
+  state.savedState.tactic.goals
+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
+
+protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
+  let metaM := mvarId.withContext m
+  metaM.run' (← read) state.savedState.term.meta.meta
+
+protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do
+  state.withContext state.parentMVar?.get! m
+protected def GoalState.withRootContext (state: GoalState) (m: MetaM α): MetaM α := do
+  state.withContext state.root m
+
+private def GoalState.mvars (state: GoalState): SSet MVarId :=
+  state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
+protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
+  state.savedState.term.meta.restore
+protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
+  state.savedState.term.restore
+private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
+  state.savedState.restore
+  Elab.Tactic.setGoals [goal]
+
+private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
+  mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
+    if let .some prevMVarDecl := mctxOld.decls.find? mvarId then
+      assert! prevMVarDecl.type == mvarDecl.type
+      acc
+    else
+      acc.insert mvarId
+    ) SSet.empty
+
+protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
+  let goal ← state.savedState.tactic.goals.get? goalId
+  return {
+    state with
+    savedState := {
+      state.savedState with
+      tactic := { goals := [goal] },
+    },
+    calcPrevRhs? := .none,
+  }
+
+/--
+Brings into scope a list of goals
+-/
+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 },
+      },
+      calcPrevRhs? := .none,
+    }
+/--
+Brings into scope all goals from `branch`
+-/
+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)
+
+protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
+  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
+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
+protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
+  let expr ← goalState.mctx.eAssignment.find? mvar
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  return expr
+
+--- Tactic execution functions ---
+
+/-- 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 goal index is out of bounds
+  | indexError (goalId: Nat)
+  -- The given action cannot be executed in the state
+  | invalidAction (message: String)
+
+protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
+          Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure $ goal
+    | .none => return .indexError goalId
+  goal.checkNotAssigned `GoalState.execute
+  try
+    let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
+    if (← getThe Core.State).messages.hasErrors then
+      let messages := (← getThe Core.State).messages.toArray
+      let errors ← (messages.map (·.data)).mapM fun md => md.toString
+      return .failure errors
+    let nextElabState ← MonadBacktrack.saveState
+    let nextMCtx := nextElabState.meta.meta.mctx
+    let prevMCtx := state.mctx
+    return .success {
+      state with
+      savedState := { term := nextElabState, tactic := newGoals },
+      newMVars := newMVarSet prevMCtx nextMCtx,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none,
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+/-- Execute tactic on given state -/
+protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
+    Elab.TermElabM TacticResult := do
+  let tactic ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := if state.isConv then `conv else `tactic)
+    (input := tactic)
+    (fileName := filename) with
+    | .ok stx => pure $ stx
+    | .error error => return .parseError error
+  state.execute goalId $ Elab.Tactic.evalTactic tactic
+
+/-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
+protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
+      Elab.TermElabM TacticResult := do
+  let goalType ← goal.getType
+  try
+    -- For some reason this is needed. One of the unit tests will fail if this isn't here
+    let error?: Option String ← goal.withContext do
+      let exprType ← Meta.inferType expr
+      if ← Meta.isDefEq goalType exprType then
+        pure .none
+      else do
+        return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}"
+    if let .some error := error? then
+      return .parseError error
+    goal.checkNotAssigned `GoalState.assign
+    goal.assign expr
+    if (← getThe Core.State).messages.hasErrors then
+      let messages := (← getThe Core.State).messages.toArray
+      let errors ← (messages.map (·.data)).mapM fun md => md.toString
+      return .failure errors
+    let prevMCtx := state.savedState.term.meta.meta.mctx
+    let nextMCtx ← getMCtx
+    -- Generate a list of mvarIds that exist in the parent state; Also test the
+    -- assertion that the types have not changed on any mvars.
+    let newMVars := newMVarSet prevMCtx nextMCtx
+    let nextGoals ← newMVars.toList.filterM (not <$> ·.isAssigned)
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals := nextGoals }
+      },
+      newMVars,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  goal.checkNotAssigned `GoalState.tryAssign
+  let expr ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := expr)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let goalType ← goal.getType
+  try
+    let expr ← goal.withContext $
+      Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType)
+    state.assign goal expr
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+-- Specialized Tactics
+
+protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  goal.checkNotAssigned `GoalState.tryHave
+  let type ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := type)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let binderName := binderName.toName
+  try
+    -- Implemented similarly to the intro tactic
+    let nextGoals: List MVarId ← goal.withContext do
+      let type ← Elab.Term.elabType (stx := type)
+      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 fvar   := mkFVar fvarId
+      let mvarUpstream ←
+        withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
+          Meta.withNewLocalInstances #[fvar] 0 do
+            let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+              (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
+            let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
+            goal.assign expr
+            pure mvarUpstream
+
+      pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals := nextGoals }
+      },
+      newMVars := nextGoals.toSSet,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  goal.checkNotAssigned `GoalState.tryLet
+  let type ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := type)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let binderName := binderName.toName
+  try
+    -- Implemented similarly to the intro tactic
+    let nextGoals: List MVarId ← goal.withContext do
+      let type ← Elab.Term.elabType (stx := type)
+      let lctx ← MonadLCtx.getLCtx
+
+      -- The branch goal inherits the same context, but with a different type
+      let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
+
+      let upstreamType := .letE binderName type mvarBranch (← goal.getType) false
+      let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+        upstreamType (kind := MetavarKind.synthetic) (userName := (← goal.getTag))
+
+      goal.assign mvarUpstream
+
+      pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals := nextGoals }
+      },
+      newMVars := nextGoals.toSSet,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+/-- Enter conv tactic mode -/
+protected def GoalState.conv (state: GoalState) (goalId: Nat):
+      Elab.TermElabM TacticResult := do
+  if state.convMVar?.isSome then
+    return .invalidAction "Already in conv state"
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  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.setGoals [newGoal.mvarId!]
+      pure rhs.mvarId!
+    return (← MonadBacktrack.saveState, convMVar)
+  try
+    let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+    let prevMCtx := state.mctx
+    let nextMCtx := nextSavedState.term.meta.meta.mctx
+    return .success {
+      root := state.root,
+      savedState := nextSavedState
+      newMVars := newMVarSet prevMCtx nextMCtx,
+      parentMVar? := .some goal,
+      convMVar? := .some (convRhs, goal),
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
+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
+    let nextMCtx := nextSavedState.term.meta.meta.mctx
+    let prevMCtx := state.savedState.term.meta.meta.mctx
+    return .success {
+      root := state.root,
+      savedState := nextSavedState
+      newMVars := newMVarSet prevMCtx nextMCtx,
+      parentMVar? := .some convGoal,
+      convMVar? := .none
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+protected def GoalState.calcPrevRhsOf? (state: GoalState) (goalId: Nat) :=
+  if goalId == 1 then
+    state.calcPrevRhs?
+  else
+    .none
+protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  if state.convMVar?.isSome then
+    return .invalidAction "Cannot initiate `calc` while in `conv` state"
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let `(term|$pred) ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := pred)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  goal.checkNotAssigned `GoalState.tryCalc
+  let calcPrevRhs? := state.calcPrevRhsOf? goalId
+  let target ← instantiateMVars (← goal.getDecl).type
+  let tag := (← goal.getDecl).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 calcPrevRhs? := Option.some rhs
+    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
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals },
+      },
+      newMVars := goals.toSSet,
+      parentMVar? := .some goal,
+      calcPrevRhs?
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+
+protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let recursor ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := recursor)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.execute goalId (tacticM := Tactic.motivatedApply recursor)
+protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let recursor ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := eq)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.execute goalId (tacticM := Tactic.noConfuse recursor)
+
+end Pantograph

Pantograph/Library.lean

@@ -0,0 +1,223 @@
+import Pantograph.Environment
+import Pantograph.Goal
+import Pantograph.Protocol
+import Pantograph.Serial
+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 defaultTermElabMContext: Elab.Term.Context := {
+    errToSorry := false
+  }
+def runMetaM { α } (metaM: MetaM α): CoreM α :=
+  metaM.run'
+def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
+  termElabM.run' (ctx := defaultTermElabMContext) |>.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_create_meta_context]
+def createMetaContext: IO Lean.Meta.Context := do
+  return {}
+
+@[export pantograph_env_catalog_m]
+def envCatalog: CoreM Protocol.EnvCatalogResult :=
+  Environment.catalog ({}: Protocol.EnvCatalog)
+
+@[export pantograph_env_inspect_m]
+def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
+    CoreM (Protocol.CR Protocol.EnvInspectResult) :=
+  Environment.inspect ({
+    name, value? := .some value, dependency?:= .some dependency
+  }: Protocol.EnvInspect) options
+
+@[export pantograph_env_add_m]
+def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
+    CoreM (Protocol.CR Protocol.EnvAddResult) :=
+  Environment.addDecl { name, type, value, isTheorem }
+
+def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
+  let env ← MonadEnv.getEnv
+  let syn ← match parseTerm env type with
+    | .error str => return .error $ errorI "parsing" str
+    | .ok syn => pure syn
+  match ← elabType syn with
+  | .error str => return .error $ errorI "elab" str
+  | .ok expr => return .ok (← instantiateMVars expr)
+
+/-- This must be a TermElabM since the parsed expr contains extra information -/
+def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
+  let env ← MonadEnv.getEnv
+  let expectedType? ← match ← expectedType?.mapM parseElabType with
+    | .none => pure $ .none
+    | .some (.ok t) => pure $ .some t
+    | .some (.error e) => return .error e
+  let syn ← match parseTerm env expr with
+    | .error str => return .error $ errorI "parsing" str
+    | .ok syn => pure syn
+  match ← elabTerm syn expectedType? with
+  | .error str => return .error $ errorI "elab" str
+  | .ok expr => return .ok (← instantiateMVars expr)
+
+@[export pantograph_expr_echo_m]
+def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[])  (options: @&Protocol.Options := {}):
+    CoreM (Protocol.CR Protocol.ExprEchoResult) :=
+  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
+    let expr ← match ← parseElabExpr expr expectedType? with
+      | .error e => return .error e
+      | .ok expr => pure expr
+    try
+      let type ← unfoldAuxLemmas (← Meta.inferType expr)
+      return .ok {
+          type := (← serializeExpression options type),
+          expr := (← serializeExpression options expr)
+      }
+    catch exception =>
+      return .error $ errorI "typing" (← exception.toMessageData.toString)
+
+@[export pantograph_goal_start_expr_m]
+def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR GoalState) :=
+  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
+    let expr ← match ← parseElabType expr with
+      | .error e => return .error e
+      | .ok expr => pure $ expr
+    return .ok $ ← GoalState.create expr
+
+@[export pantograph_goal_resume]
+def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
+  target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
+
+@[export pantograph_goal_continue]
+def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
+  target.continue branch
+
+@[export pantograph_goal_serialize_m]
+def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
+  runMetaM <| state.serializeGoals (parent := .none) options
+
+@[export pantograph_goal_print_m]
+def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
+  runMetaM do
+    state.restoreMetaM
+    return {
+      root? := ← state.rootExpr?.mapM (λ expr =>
+        state.withRootContext do
+          serializeExpression options (← instantiateAll expr)),
+      parent? := ← state.parentExpr?.mapM (λ expr =>
+        state.withParentContext do
+          serializeExpression options (← instantiateAll expr)),
+    }
+@[export pantograph_goal_diag_m]
+def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : CoreM String :=
+  runMetaM $ state.diag diagOptions
+
+@[export pantograph_goal_tactic_m]
+def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult :=
+  runTermElabM <| state.tryTactic goalId tactic
+@[export pantograph_goal_assign_m]
+def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult :=
+  runTermElabM <| state.tryAssign goalId expr
+@[export pantograph_goal_have_m]
+def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
+  runTermElabM <| state.tryHave goalId binderName type
+@[export pantograph_goal_let_m]
+def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
+  runTermElabM <| state.tryLet goalId binderName type
+@[export pantograph_goal_conv_m]
+def goalConv (state: GoalState) (goalId: Nat): CoreM TacticResult :=
+  runTermElabM <| state.conv goalId
+@[export pantograph_goal_conv_exit_m]
+def goalConvExit (state: GoalState): CoreM TacticResult :=
+  runTermElabM <| state.convExit
+@[export pantograph_goal_calc_m]
+def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult :=
+  runTermElabM <| state.tryCalc goalId pred
+@[export pantograph_goal_focus]
+def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
+  state.focus goalId
+@[export pantograph_goal_motivated_apply_m]
+def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): CoreM TacticResult :=
+  runTermElabM <| state.tryMotivatedApply goalId recursor
+@[export pantograph_goal_no_confuse_m]
+def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult :=
+  runTermElabM <| state.tryNoConfuse goalId eq
+
+inductive SyntheticTactic where
+  | congruenceArg
+  | congruenceFun
+  | congruence
+/-- Executes a synthetic tactic which has no arguments -/
+@[export pantograph_goal_synthetic_tactic_m]
+def goalSyntheticTactic (state: GoalState) (goalId: Nat) (case: SyntheticTactic): CoreM TacticResult :=
+  runTermElabM do
+    state.restoreElabM
+    state.execute goalId $ match case with
+      | .congruenceArg => Tactic.congruenceArg
+      | .congruenceFun => Tactic.congruenceFun
+      | .congruence => Tactic.congruence
+
+
+
+end Pantograph

Pantograph/Protocol.lean

@@ -0,0 +1,303 @@
+/-
+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
+
+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
+  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?: Option Bool := .none
+  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
+  -- universe levels
+  levels: Option (Array String) := .none
+  deriving Lean.FromJson
+structure ExprEchoResult where
+  expr: Expression
+  type: Expression
+  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
+  -- If true/false, show/hide the value expressions; By default definitions
+  -- values are shown and theorem values are hidden.
+  value?: Option Bool := .some false
+  -- If true, show the type and value dependencies
+  dependency?: 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
+  deriving Lean.ToJson
+
+structure EnvAdd where
+  name: String
+  type: String
+  value: String
+  isTheorem: Bool
+  deriving Lean.FromJson
+structure EnvAddResult where
+  deriving Lean.ToJson
+
+/-- Set options; See `Options` struct above for meanings -/
+structure OptionsSet where
+  printJsonPretty?: Option Bool
+  printExprPretty?: Option Bool
+  printExprAST?: Option Bool
+  printDependentMVars?: Option Bool
+  noRepeat?: Option Bool
+  printAuxDecls?: Option Bool
+  printImplementationDetailHyps?: Option Bool
+  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 -- 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
+  calc?: Option String := .none
+  -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
+  conv?: Option Bool := .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
+  deriving Lean.FromJson
+structure GoalPrintResult where
+  -- The root expression
+  root?: Option Expression := .none
+  -- The filling expression of the parent goal
+  parent?: Option 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
+
+
+/-- Executes the Lean compiler on a single file -/
+structure CompileUnit where
+  module: String
+  -- If set to true, query the string boundaries of compilation units
+  compilationUnits: Bool := false
+  -- If set to true, collect tactic invocations
+  invocations: Bool := false
+  deriving Lean.FromJson
+structure InvokedTactic where
+  goalBefore: String
+  goalAfter: String
+  tactic: String
+  deriving Lean.ToJson
+structure CompileUnitResult where
+  units?: Option $ List (Nat × Nat)
+  invocations?: Option $ List InvokedTactic
+  deriving Lean.ToJson
+
+abbrev CR α := Except InteractionError α
+
+end Pantograph.Protocol

Pantograph/Serial.lean

@@ -0,0 +1,352 @@
+/-
+All serialisation functions;
+This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
+using `Scope`s.
+-/
+import Lean
+import Pantograph.Expr
+
+import Pantograph.Protocol
+import Pantograph.Goal
+
+open Lean
+
+-- Symbol processing functions --
+
+namespace Pantograph
+
+
+--- Input Functions ---
+
+/-- Read syntax object from string -/
+def parseTerm (env: Environment) (s: String): Except String Syntax :=
+  Parser.runParserCategory
+    (env := env)
+    (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)
+
+
+--- Output Functions ---
+
+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) (sanitize: Bool): String :=
+  let k := level.getOffset
+  let u := level.getLevelOffset
+  let u_str := match u with
+    | .zero => "0"
+    | .succ _ => panic! "getLevelOffset should not return .succ"
+    | .max v w =>
+      let v := serializeSortLevel v sanitize
+      let w := serializeSortLevel w sanitize
+      s!"(:max {v} {w})"
+    | .imax v w =>
+      let v := serializeSortLevel v sanitize
+      let w := serializeSortLevel w sanitize
+      s!"(:imax {v} {w})"
+    | .param name =>
+      let name := serializeName name sanitize
+      s!"{name}"
+    | .mvar id =>
+      let name := serializeName id.name sanitize
+      s!"(:mv {name})"
+  match k, u with
+  | 0, _ => u_str
+  | _, .zero => s!"{k}"
+  | _, _ => s!"(+ {u_str} {k})"
+
+
+/--
+ Completely serializes an expression tree. Json not used due to compactness
+
+A `_` symbol in the AST indicates automatic deductions not present in the original expression.
+-/
+partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
+  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 := ofName fvarId.name
+      pure s!"(:fv {name})"
+    | .mvar mvarId => do
+        let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
+        let name := ofName mvarId.name
+        pure s!"(:{pref} {name})"
+    | .sort level =>
+      let level := serializeSortLevel level sanitize
+      pure s!"(:sort {level})"
+    | .const declName _ =>
+      -- 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' := ofName binderName
+      let binderType' ← self binderType
+      let body' ← self body
+      let binderInfo' := binderInfoSexp binderInfo
+      pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
+    | .forallE binderName binderType body binderInfo => do
+      let binderName' := ofName binderName
+      let binderType' ← self binderType
+      let body' ← self body
+      let binderInfo' := binderInfoSexp binderInfo
+      pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
+    | .letE name type value body _ => do
+      -- Dependent boolean flag diacarded
+      let name' := serializeName name
+      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 => s!"\"{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
+      let ctor := getStructureCtor env typeName
+      let fieldName := getStructureFields env typeName |>.get! idx
+      let projectorName := getProjFnForField? env typeName fieldName |>.get!
+
+      let autos := String.intercalate " " (List.replicate ctor.numParams "_")
+      let inner ← self inner
+      pure s!"((:c {projectorName}) {autos} {inner})"
+  -- Elides all unhygenic names
+  binderInfoSexp : Lean.BinderInfo → String
+    | .default => ""
+    | .implicit => " :implicit"
+    | .strictImplicit => " :strictImplicit"
+    | .instImplicit => " :instImplicit"
+  ofName (name: Name) := serializeName name sanitize
+
+def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
+  let pp?: Option String ← match options.printExprPretty with
+    | 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)
+      : 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 _ _ _ =>
+        let userName := userName.simpMacroScopes
+        return {
+          name := ofName fvarId.name,
+          userName:= ofName userName.simpMacroScopes,
+        }
+      | .ldecl _ fvarId userName _ _ _ _ => do
+        return {
+          name := ofName fvarId.name,
+          userName := toString userName.simpMacroScopes,
+        }
+    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 := ofName fvarId.name,
+          userName:= ofName userName,
+          isInaccessible? := .some 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 := ofName fvarId.name,
+          userName:= ofName userName,
+          isInaccessible? := .some 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 := ofName goal.name,
+      userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
+      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
+      target := (← serializeExpression options (← instantiate mvarDecl.type)),
+      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 -/
+protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): 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 goalState.newMVars.contains mvarId then "~" else " "
+        printMVar pref mvarId decl
+      )
+  pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
+  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 (sanitize := false)
+          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}]"
+
+end Pantograph

Pantograph/Tactic.lean

@@ -0,0 +1,4 @@
+
+import Pantograph.Tactic.Congruence
+import Pantograph.Tactic.MotivatedApply
+import Pantograph.Tactic.NoConfuse

Pantograph/Tactic/Congruence.lean

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

Pantograph/Tactic/MotivatedApply.lean

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

Pantograph/Tactic/NoConfuse.lean

@@ -0,0 +1,18 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+def noConfuse: Elab.Tactic.Tactic := λ stx => do
+  let goal ← Elab.Tactic.getMainGoal
+  goal.withContext do
+    let absurd ← Elab.Term.elabTerm (stx := stx) .none
+    let noConfusion ← Meta.mkNoConfusion (target := ← goal.getType) (h := absurd)
+
+    unless ← Meta.isDefEq (← Meta.inferType noConfusion) (← goal.getType) do
+      throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr $ ← goal.getType}"
+    goal.assign noConfusion
+  Elab.Tactic.setGoals []
+
+end Pantograph.Tactic

Pantograph/Version.lean

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

README.md

@@ -0,0 +1,161 @@
+# 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.
+
+## Installation
+
+For Nix based workflow, see below.
+
+Install `elan` and `lake`. Execute
+``` sh
+make
+```
+This builds the executable in `.lake/build/bin/pantograph`.
+
+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-packages"
+export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+
+LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
+```
+The `$LEAN_PATH` executable of any project can be extracted by
+``` sh
+lake env printenv LEAN_PATH
+```
+
+## Executable Usage
+
+``` sh
+pantograph MODULES|LEAN_OPTIONS
+```
+
+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.
+
+The `pantograph` executable must be run with a list of modules to import. It can
+also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
+
+Example: (~5k symbols)
+```
+$ 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.
+
+### Commands
+
+See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
+* `reset`: Delete all cached expressions and proof trees
+* `stat`: Display resource usage
+* `expr.echo {"expr": <expr>, "type": <optional expected type>, ["levels": [<levels>]]}`: Determine the
+  type of an expression and format it.
+* `env.catalog`: Display a list of all safe Lean symbols in the current environment
+* `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
+  given symbol; If value flag is set, the value is printed or hidden. By default
+  only the values of definitions are printed.
+* `options.set { key: value, ... }`: Set one or more options (not Lean options; those
+  have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
+* `options.print`: Display the current set of options
+* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
+  Start a new proof from a given expression or symbol
+* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
+  given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
+  - `{ "tactic": <tactic> }`: Execute an ordinary tactic
+  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
+  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
+  - `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
+    be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
+    to the previous `rhs`.
+  - `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
+    exit, the goal id is ignored.
+* `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
+  Execute continuation/resumption
+  - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.
+  - `{ "goals": <names> }`: Resume the given goals
+* `goal.remove {"stateIds": [<id>]}"`: Drop the goal states specified in the list
+* `goal.print {"stateId": <id>}"`: Print a goal state
+
+### 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.
+
+### 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.
+
+## Developing
+
+A Lean development shell is provided in the Nix flake.
+
+### Testing
+
+The tests are based on `LSpec`. To run tests,
+``` sh
+make test
+```
+
+## Nix based workflow
+
+The included Nix flake provides build targets for `sharedLib` and `executable`.
+The executable can be used as-is, but linking against the shared library
+requires the presence of `lean-all`.
+
+To run tests:
+``` sh
+nix flake check
+```

Test/Common.lean

@@ -0,0 +1,89 @@
+import Pantograph.Goal
+import Pantograph.Library
+import Pantograph.Protocol
+import Lean
+import LSpec
+
+open Lean
+
+namespace Pantograph
+
+-- 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
+
+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}"
+  | .indexError index => s!".indexError {index}"
+  | .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 := Pantograph.defaultTermElabMContext)
+
+def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
+
+def parseSentence (s: String): MetaM Expr := do
+  let recursor ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := s)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => throwError "Failed to parse: {error}"
+  runTermElabMInMeta $ Elab.Term.elabTerm (stx := recursor) .none
+
+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)
+
+end Test
+
+end Pantograph

Test/Environment.lean

@@ -0,0 +1,107 @@
+import LSpec
+import Pantograph.Serial
+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),
+    ("Lean.Name".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 suite: List (String × IO LSpec.TestSeq) :=
+  [
+    ("Catalog", test_catalog),
+    ("Symbol Visibility", test_symbol_visibility),
+    ("Inspect", test_inspect),
+  ]
+
+end Pantograph.Test.Environment

Test/Integration.lean

@@ -0,0 +1,171 @@
+/- Integration test for the REPL
+ -/
+import LSpec
+import Pantograph
+namespace Pantograph.Test.Integration
+open Pantograph
+
+def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
+    (expected: Lean.Json): MainM LSpec.TestSeq := do
+  let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload }
+  return LSpec.test name (toString result = toString expected)
+def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
+    (expected: Lean.Json): MainM LSpec.TestSeq := subroutine_named_step cmd cmd payload expected
+
+def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
+  -- Setup the environment for execution
+  let env ← Lean.importModules
+    (imports := #[{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
+    (opts := {})
+    (trustLevel := 1)
+  let context: Context := {
+    imports := ["Init"]
+  }
+  let coreContext: Lean.Core.Context ← createCoreContext #[]
+  let commands: MainM LSpec.TestSeq :=
+    steps.foldlM (λ suite step => do
+      let result ← step
+      return suite ++ result) LSpec.TestSeq.done
+  try
+    let coreM := commands.run context |>.run' {}
+    return Prod.fst $ (← coreM.toIO coreContext { env := env })
+  catch ex =>
+    return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
+
+def test_elab : IO LSpec.TestSeq :=
+  subroutine_runner [
+    subroutine_step "expr.echo"
+      [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
+     (Lean.toJson ({
+       type := { pp? := .some "{α : Type u} → Type u" },
+       expr := { pp? := .some "fun {α} => List α" }
+     }: Protocol.ExprEchoResult)),
+  ]
+
+def test_option_modify : IO LSpec.TestSeq :=
+  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 := {}
+  subroutine_runner [
+    subroutine_step "env.inspect"
+      [("name", .str "Nat.add_one")]
+     (Lean.toJson ({
+       type := { pp? }, module? }:
+      Protocol.EnvInspectResult)),
+    subroutine_step "options.set"
+      [("printExprAST", .bool true)]
+     (Lean.toJson ({ }:
+      Protocol.OptionsSetResult)),
+    subroutine_step "env.inspect"
+      [("name", .str "Nat.add_one")]
+     (Lean.toJson ({
+       type := { pp?, sexp? }, module? }:
+      Protocol.EnvInspectResult)),
+    subroutine_step "options.print"
+      []
+     (Lean.toJson ({ options with printExprAST := true }:
+      Protocol.Options))
+  ]
+def test_malformed_command : IO LSpec.TestSeq :=
+  let invalid := "invalid"
+  subroutine_runner [
+    subroutine_named_step "Invalid command" invalid
+      [("name", .str "Nat.add_one")]
+     (Lean.toJson ({
+       error := "command", desc := s!"Unknown command {invalid}"}:
+      Protocol.InteractionError)),
+    subroutine_named_step "JSON Deserialization" "expr.echo"
+      [(invalid, .str "Random garbage data")]
+     (Lean.toJson ({
+       error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
+      Protocol.InteractionError))
+  ]
+def test_tactic : IO LSpec.TestSeq :=
+  let goal1: Protocol.Goal := {
+    name := "_uniq.11",
+    target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
+    vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
+  }
+  let goal2: Protocol.Goal := {
+    name := "_uniq.17",
+    target := { pp? := .some "x ∨ y → y ∨ x" },
+    vars := #[
+      { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
+      { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
+    ],
+  }
+  subroutine_runner [
+    subroutine_step "goal.start"
+      [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+     (Lean.toJson ({stateId := 0, root := "_uniq.9"}:
+      Protocol.GoalStartResult)),
+    subroutine_step "goal.tactic"
+      [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
+     (Lean.toJson ({
+       nextStateId? := .some 1,
+       goals? := #[goal1],
+     }:
+      Protocol.GoalTacticResult)),
+    subroutine_step "goal.print"
+      [("stateId", .num 1)]
+     (Lean.toJson ({
+       parent? := .some { pp? := .some "fun x => ?m.12 x" },
+     }:
+      Protocol.GoalPrintResult)),
+    subroutine_step "goal.tactic"
+      [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
+     (Lean.toJson ({
+       nextStateId? := .some 2,
+       goals? := #[goal2],
+     }:
+      Protocol.GoalTacticResult))
+  ]
+
+def test_env_add_inspect : IO LSpec.TestSeq :=
+  let name1 := "Pantograph.mystery"
+  let name2 := "Pantograph.mystery2"
+  subroutine_runner [
+    subroutine_step "env.add"
+      [
+        ("name", .str name1),
+        ("type", .str "Prop → Prop → Prop"),
+        ("value", .str "λ (a b: Prop) => Or a b"),
+        ("isTheorem", .bool false)
+      ]
+     (Lean.toJson ({}: Protocol.EnvAddResult)),
+    subroutine_step "env.inspect"
+      [("name", .str name1)]
+     (Lean.toJson ({
+       value? := .some { pp? := .some "fun a b => a ∨ b" },
+       type := { pp? := .some "Prop → Prop → Prop" },
+     }:
+      Protocol.EnvInspectResult)),
+    subroutine_step "env.add"
+      [
+        ("name", .str name2),
+        ("type", .str "Nat → Int"),
+        ("value", .str "λ (a: Nat) => a + 1"),
+        ("isTheorem", .bool false)
+      ]
+     (Lean.toJson ({}: Protocol.EnvAddResult)),
+    subroutine_step "env.inspect"
+      [("name", .str name2)]
+     (Lean.toJson ({
+       value? := .some { pp? := .some "fun a => ↑a + 1" },
+       type := { pp? := .some "Nat → Int" },
+     }:
+      Protocol.EnvInspectResult))
+  ]
+
+def suite: List (String × IO LSpec.TestSeq) :=
+  [
+    ("Elab", test_elab),
+    ("Option modify", test_option_modify),
+    ("Malformed command", test_malformed_command),
+    ("Tactic", test_tactic),
+    ("env.add env.inspect", test_env_add_inspect),
+  ]
+
+
+end Pantograph.Test.Integration

Test/Library.lean

@@ -0,0 +1,38 @@
+import LSpec
+import Lean
+import Pantograph.Library
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Library
+
+def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
+  let inner: CoreM LSpec.TestSeq := do
+    let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
+    let tests := LSpec.TestSeq.done
+    let echoResult ← exprEcho prop_and_proof (options := {})
+    let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
+      type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
+    }))
+    let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
+    let 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 _ 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,57 @@
+import LSpec
+import Test.Environment
+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 (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
+  let tests: List (String × IO LSpec.TestSeq) := match filter with
+    | .some filter => tests.filter (λ (name, _) => filter.isPrefixOf name)
+    | .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 name_filter := 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),
+    ("Integration", Integration.suite),
+    ("Library", Library.suite env_default),
+    ("Metavar", Metavar.suite env_default),
+    ("Proofs", Proofs.suite env_default),
+    ("Serial", Serial.suite env_default),
+    ("Tactic/Congruence", Tactic.Congruence.suite env_default),
+    ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
+    ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
+  ]
+  let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
+  LSpec.lspecIO (← runTestGroup name_filter tests)

Test/Metavar.lean

@@ -0,0 +1,285 @@
+import LSpec
+import Pantograph.Goal
+import Pantograph.Serial
+import Test.Common
+import Lean
+
+namespace Pantograph.Test.Metavar
+open Pantograph
+open Lean
+
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
+
+def addTest (test: LSpec.TestSeq): TestM Unit := do
+  set $ (← get) ++ test
+
+-- 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 },
+      isInaccessible? := .some false
+    })).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 := defaultTermElabMContext)
+  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.tryTactic (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.tryTactic (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.tryTactic (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.tryTactic (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.tryTactic (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.tryTactic (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.tryTactic (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 (goalId := 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 "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
+  addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
+
+  let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check ":= Eq.refl" ((← 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.tryTactic (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.tryTactic (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 ≤ ?m.succ", .some "?m.succ ≤ 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 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+
+  -- Continuation should fail if the state does not exist:
+  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,871 @@
+/-
+Tests pertaining to goals with no interdependencies
+-/
+import LSpec
+import Pantograph.Goal
+import Pantograph.Serial
+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 := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
+
+def addTest (test: LSpec.TestSeq): TestM Unit := do
+  set $ (← get) ++ test
+
+def startProof (start: Start): TestM (Option GoalState) := do
+  let env ← Lean.MonadEnv.getEnv
+  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 },
+      isInaccessible? := .some false
+    })).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 },
+      isInaccessible? := .some false
+    })).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 := defaultTermElabMContext)
+  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.tryTactic (goalId := 0) (tactic := 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!) (sanitize := false)
+  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.tryTactic (goalId := 0) (tactic := "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.tryTactic (goalId := 0) (tactic := "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.tryTactic (goalId := 0) (tactic := "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.tryTactic (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.tryTactic (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 }),
+        isInaccessible? := x.snd.map (λ _ => false)
+      })).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.tryTactic (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.tryTactic (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.tryTactic (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.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let fvP := "_uniq.10"
+  let fvQ := "_uniq.13"
+  let fvH := "_uniq.16"
+  let state1g0 := "_uniq.17"
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
+    #[{
+      name := state1g0,
+      target := { pp? := .some "q ∨ p" },
+      vars := #[
+        { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
+        { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
+        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" }, isInaccessible? := .some false }
+      ]
+    }])
+  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!) (sanitize := false)
+  addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
+  let tactic := "cases h"
+  let state2 ← match ← state1.tryTactic (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 (caseL, caseR) := ("_uniq.64", "_uniq.77")
+  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
+    #[caseL, caseR])
+  addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
+  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
+
+  let state2parent ← state2.withParentContext do
+    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
+  let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
+  let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
+  let motive := s!"(:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
+  let caseL := s!"(:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))"
+  let caseR := s!"(:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))"
+  let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))"
+  addTest $ LSpec.test "(2 parent)" (state2parent ==
+    s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
+
+  let state3_1 ← match ← state2.tryTactic (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!) (sanitize := false)
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
+  addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
+  let state4_1 ← match ← state3_1.tryTactic (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.tryTactic (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.tryTactic (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.get! 0])
+  let state3_1 ← match ← state2b.tryTactic (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.tryTactic (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, isInaccessible? := .some false },
+        { userName := "q", type? := .some typeProp, isInaccessible? := .some false },
+        { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true }
+      ]
+    }
+
+def test_have: TestM Unit := do
+  let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro p q h"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
+
+  let expr := "Or.inl (Or.inl h)"
+  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  let haveBind := "y"
+  let haveType := "p ∨ q"
+  let state2 ← match ← state1.tryHave (goalId := 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 (options := ← read)).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 (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals (options := ← read)).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 (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
+
+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.tryTactic (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 (goalId := 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.tryTactic (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.tryTactic (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.tryTactic (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.tryTactic (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.tryTactic (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.tryTactic (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.tryTactic (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.tryTactic (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 (goalId := 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? 0 |>.isNone)
+  addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? 1 |>.isSome)
+
+  let tactic := "apply h1"
+  let state2m ← match ← state2.tryTactic (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 (goalId := 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? 0 |>.isNone)
+  let tactic := "apply h2"
+  let state4m ← match ← state4.tryTactic (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_let (specialized: Bool): TestM Unit := do
+  let state? ← startProof (.expr "∀ (a: Nat) (p: Prop), p → p ∨ ¬p")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro a p h"
+  let state1 ← match ← state0.tryTactic (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 [] "p ∨ ¬p"])
+
+
+  let letType := "Nat"
+  let expr := s!"let b: {letType} := _; _"
+  let result2 ← match specialized with
+    | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType)
+    | false => state1.tryAssign (goalId := 0) (expr := expr)
+  let state2 ← match result2 with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let serializedState2 ← state2.serializeGoals (options := ← read)
+  addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
+    #[
+      interiorGoal [] letType,
+      interiorGoal [] "let b := ?m.20;\np ∨ ¬p"
+    ])
+  -- Check that the goal mvar ids match up
+  addTest $ LSpec.check "(mvarId)" ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20")
+
+  let tactic := "exact a"
+  let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = #[])
+
+  let state3r ← match state3.continue state2 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[interiorGoal [] "let b := a;\np ∨ ¬p"])
+
+  let tactic := "exact h"
+  match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
+  | .failure #[message] =>
+    addTest $ LSpec.check tactic  (message = "type mismatch\n  h\nhas type\n  p : Prop\nbut is expected to have type\n  let b := a;\n  p ∨ ¬p : Prop")
+  | other => do
+    addTest $ assertUnreachable $ other.toString
+
+  let tactic := "intro b"
+  let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let tactic := "exact Or.inl h"
+  let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(5 root)" state5.rootExpr?.isSome
+  where
+    interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
+      let free := [("a", "Nat"), ("p", "Prop"), ("h", "p")] ++ free
+      buildGoal free target userName?
+
+def test_nat_zero_add: TestM Unit := do
+  let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro n"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat")] "n + 0 = n"])
+  let recursor := "@Nat.brecOn"
+  let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
+    #[
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
+    ])
+
+  let tactic := "exact n"
+  let state3b ← match ← state2.tryTactic (goalId := 1) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3b.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+  let state2b ← match state3b.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let tactic := "exact (λ x => x + 0 = x)"
+  let state3c ← match ← state2b.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3c.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+  let state2c ← match state3c.continue state2b with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let tactic := "intro t h"
+  let state3 ← match ← state2c.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
+
+  let tactic := "simp"
+  let state3d ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state2d ← match state3d.continue state2c with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let tactic := "rfl"
+  let stateF ← match ← state2d.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) =
+    #[])
+
+  let expr := stateF.mctx.eAssignment.find! stateF.root
+  let (expr, _) := instantiateMVarsCore (mctx := stateF.mctx) (e := expr)
+  addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome
+
+def test_nat_zero_add_alt: TestM Unit := do
+  let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro n"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat")] "n + 0 = n"])
+  let recursor := "@Nat.brecOn"
+  let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let major := "_uniq.68"
+  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
+    #[
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal major [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
+    ])
+
+  let tactic := "intro x"
+  let state3m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")])
+  let tactic := "apply Eq"
+  let state3m2 ← match ← state3m.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
+  addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
+  let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
+  let state2b ← match state3m2.resume [conduit] with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+
+  let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
+  let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
+  let fvN := "_uniq.63"
+  let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
+  let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
+  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
+    #[
+      {
+        name := "_uniq.70",
+        userName? := .some "conduit",
+        target := {
+          pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
+          sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
+        },
+        vars := #[{
+          name := fvN,
+          userName := "n",
+          type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
+          isInaccessible? := .some false
+        }],
+      }
+    ])
+
+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),
+    ("have", test_have),
+    ("conv", test_conv),
+    ("calc", test_calc),
+    ("let via assign", test_let false),
+    ("let via tryLet", test_let true),
+    ("Nat.zero_add", test_nat_zero_add),
+    ("Nat.zero_add alt", test_nat_zero_add_alt),
+  ]
+  tests.map (fun (name, test) => (name, proofRunner env test))
+
+
+
+end Pantograph.Test.Proofs

Test/Serial.lean

@@ -0,0 +1,109 @@
+import LSpec
+import Pantograph.Serial
+import Test.Common
+import Lean
+
+open Lean
+namespace Pantograph.Test.Serial
+
+open Pantograph
+
+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 _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"),
+    -- These ones are normal and easy
+    ("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"),
+    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"),
+    -- Handling of higher order types
+    ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
+    ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
+  ]
+  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) :implicit)"),
+    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
+    ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
+  ]
+  entries.foldlM (λ suites (source, levels, target) =>
+    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 := defaultTermElabMContext)
+    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)) :implicit) :implicit)"
+    ),
+  ]
+  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 := defaultTermElabMContext)
+
+-- 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 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),
+  ]
+
+end Pantograph.Test.Serial

Test/Tactic.lean

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

Test/Tactic/Congruence.lean

@@ -0,0 +1,109 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.Congruence
+
+def test_congr_arg_list (env: Environment): IO LSpec.TestSeq :=
+  let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
+  runMetaMSeq env do
+    let expr ← parseSentence expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let mut tests := LSpec.TestSeq.done
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let (newGoals, test) ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
+        let test := LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+          [
+            (`α, "Sort ?u.30"),
+            (`a₁, "?α"),
+            (`a₂, "?α"),
+            (`f, "?α → List α"),
+            (`h, "?a₁ = ?a₂"),
+            (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
+          ])
+        return (newGoals, test)
+      tests := tests ++ test
+      let f := newGoals.get! 3
+      let h := newGoals.get! 4
+      let c := newGoals.get! 5
+      let results ← f.apply (← parseSentence "List.reverse")
+      tests := tests ++ (LSpec.check "apply" (results.length = 0))
+      tests := tests ++ (LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂"))
+      tests := tests ++ (LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)"))
+      return tests
+def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
+  let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
+  runMetaMSeq env do
+    let expr ← parseSentence expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let mut tests := LSpec.TestSeq.done
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+          [
+            (`α, "Sort ?u.70"),
+            (`a₁, "?α"),
+            (`a₂, "?α"),
+            (`f, "?α → Nat"),
+            (`h, "?a₁ = ?a₂"),
+            (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
+          ])
+      tests := tests ++ test
+      return tests
+def test_congr_fun (env: Environment): IO LSpec.TestSeq :=
+  let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
+  runMetaMSeq env do
+    let expr ← parseSentence expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let mut tests := LSpec.TestSeq.done
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId!
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+          [
+            (`α, "Sort ?u.159"),
+            (`f₁, "?α → Nat"),
+            (`f₂, "?α → Nat"),
+            (`h, "?f₁ = ?f₂"),
+            (`a, "?α"),
+            (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
+          ])
+      tests := tests ++ test
+      return tests
+def test_congr (env: Environment): IO LSpec.TestSeq :=
+  let expr := "λ (a b: Nat) => a = b"
+  runMetaMSeq env do
+    let expr ← parseSentence expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let mut tests := LSpec.TestSeq.done
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId!
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+          [
+            (`α, "Sort ?u.10"),
+            (`f₁, "?α → Nat"),
+            (`f₂, "?α → Nat"),
+            (`a₁, "?α"),
+            (`a₂, "?α"),
+            (`h₁, "?f₁ = ?f₂"),
+            (`h₂, "?a₁ = ?a₂"),
+            (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
+          ])
+      tests := tests ++ test
+      return tests
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("congrArg List.reverse", test_congr_arg_list env),
+    ("congrArg", test_congr_arg env),
+    ("congrFun", test_congr_fun env),
+    ("congr", test_congr env),
+  ]
+
+end Pantograph.Test.Tactic.Congruence

Test/Tactic/MotivatedApply.lean

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

Test/Tactic/NoConfuse.lean

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

doc/icon.svg

@@ -0,0 +1,73 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+
+<svg
+   width="256"
+   height="256"
+   viewBox="0 0 55.900957 55.900957"
+   version="1.1"
+   id="svg21534"
+   xml:space="preserve"
+   inkscape:version="1.2.2 (b0a8486541, 2022-12-01)"
+   sodipodi:docname="icon.svg"
+   xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+   xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+   xmlns="http://www.w3.org/2000/svg"
+   xmlns:svg="http://www.w3.org/2000/svg"><sodipodi:namedview
+     id="namedview21536"
+     pagecolor="#ffffff"
+     bordercolor="#111111"
+     borderopacity="1"
+     inkscape:showpageshadow="0"
+     inkscape:pageopacity="0"
+     inkscape:pagecheckerboard="1"
+     inkscape:deskcolor="#d1d1d1"
+     inkscape:document-units="px"
+     showgrid="true"
+     inkscape:zoom="5.1754899"
+     inkscape:cx="158.82554"
+     inkscape:cy="91.682142"
+     inkscape:window-width="3777"
+     inkscape:window-height="2093"
+     inkscape:window-x="0"
+     inkscape:window-y="0"
+     inkscape:window-maximized="1"
+     inkscape:current-layer="layer1"><inkscape:grid
+       type="xygrid"
+       id="grid23833"
+       spacingx="3.4938098"
+       spacingy="3.4938098"
+       empspacing="4" /></sodipodi:namedview><defs
+     id="defs21531" /><g
+     inkscape:label="Layer 1"
+     inkscape:groupmode="layer"
+     id="layer1"><rect
+       style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:1.78013;stroke-miterlimit:3.4;stroke-dasharray:none"
+       id="rect26805"
+       width="11.502316"
+       height="2.2512667"
+       x="33.344425"
+       y="7.6690259"
+       ry="0.28140834"
+       rx="0.47926313" /><path
+       style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
+       d="m 35.764667,9.9513013 c 0,0 -26.8581417,13.7987337 -28.0863506,14.9501437 -1.250042,1.171878 3.2347846,3.945325 3.2347846,3.945325 l 21.34979,14.934062 6.624567,0.453105 -27.599216,-17.304358 c 0,0 -0.603209,-0.08927 -0.600411,-0.762283 0.0028,-0.673015 27.32022,-16.4227356 27.32022,-16.4227356 z"
+       id="path27381"
+       sodipodi:nodetypes="csccccscc" /><path
+       style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
+       d="M 10.97848,26.985751 40.537772,9.7943227 41.921795,9.7005084 11.210626,27.421377 Z"
+       id="path27479" /><path
+       style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
+       d="m 7.0509847,25.522367 c -0.8266141,1.386819 -2.4011783,4.48805 -2.4706357,4.90223 -0.069458,0.414182 0.4434324,0.513474 0.8491061,0.757041 C 5.835129,31.425204 19.33424,43.917182 19.33424,43.917182 l 0.324562,-0.539228 c 0,0 -14.2055729,-12.369493 -14.0644435,-12.868167 0.1411292,-0.498672 3.544896,-3.777392 3.544896,-3.777392 L 7.4596884,25.117508 Z"
+       id="path27481" /><rect
+       style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:2.11692;stroke-miterlimit:3.4;stroke-dasharray:none;stroke-opacity:1"
+       id="rect27483"
+       width="36.38942"
+       height="3.6217353"
+       x="13.953447"
+       y="43.009739"
+       rx="0.43672624"
+       ry="0.43672624" /><path
+       style="fill:none;stroke:#000000;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+       d="M -2.1119274,7.666599 H 64.179192"
+       id="path27487" /></g></svg>

flake.lock

@@ -0,0 +1,238 @@
+{
+  "nodes": {
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib"
+      },
+      "locked": {
+        "lastModified": 1709336216,
+        "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "locked": {
+        "lastModified": 1656928814,
+        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "lean": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "lean4-mode": "lean4-mode",
+        "nix": "nix",
+        "nixpkgs": "nixpkgs_2",
+        "nixpkgs-old": "nixpkgs-old"
+      },
+      "locked": {
+        "lastModified": 1719788866,
+        "narHash": "sha256-kB2cp1XJKODXiuiKp7J5OK+PFP+sOSBE5gdVNOKWCPI=",
+        "owner": "leanprover",
+        "repo": "lean4",
+        "rev": "3b58e0649156610ce3aeed4f7b5c652340c668d4",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover",
+        "ref": "v4.10.0-rc1",
+        "repo": "lean4",
+        "type": "github"
+      }
+    },
+    "lean4-mode": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1676498134,
+        "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
+        "owner": "leanprover",
+        "repo": "lean4-mode",
+        "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover",
+        "repo": "lean4-mode",
+        "type": "github"
+      }
+    },
+    "lowdown-src": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1633514407,
+        "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
+        "owner": "kristapsdz",
+        "repo": "lowdown",
+        "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
+        "type": "github"
+      },
+      "original": {
+        "owner": "kristapsdz",
+        "repo": "lowdown",
+        "type": "github"
+      }
+    },
+    "lspec": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1701971219,
+        "narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=",
+        "owner": "lurk-lab",
+        "repo": "LSpec",
+        "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+        "type": "github"
+      },
+      "original": {
+        "owner": "lurk-lab",
+        "ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+        "repo": "LSpec",
+        "type": "github"
+      }
+    },
+    "nix": {
+      "inputs": {
+        "lowdown-src": "lowdown-src",
+        "nixpkgs": "nixpkgs",
+        "nixpkgs-regression": "nixpkgs-regression"
+      },
+      "locked": {
+        "lastModified": 1657097207,
+        "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
+        "owner": "NixOS",
+        "repo": "nix",
+        "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "repo": "nix",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1653988320,
+        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-22.05-small",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-lib": {
+      "locked": {
+        "dir": "lib",
+        "lastModified": 1709237383,
+        "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
+        "type": "github"
+      },
+      "original": {
+        "dir": "lib",
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-old": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-regression": {
+      "locked": {
+        "lastModified": 1643052045,
+        "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1686089707,
+        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixpkgs-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs_3": {
+      "locked": {
+        "lastModified": 1711703276,
+        "narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "d8fe5e6c92d0d190646fb9f1056741a229980089",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "lean": "lean",
+        "lspec": "lspec",
+        "nixpkgs": "nixpkgs_3"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,81 @@
+{
+  description = "Pantograph";
+
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+    flake-parts.url = "github:hercules-ci/flake-parts";
+    lean = {
+      # Do not follow input's nixpkgs since it could cause build failures
+      url = "github:leanprover/lean4?ref=v4.10.0-rc1";
+    };
+    lspec = {
+      url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
+      flake = false;
+    };
+  };
+
+  outputs = inputs @ {
+    self,
+    nixpkgs,
+    flake-parts,
+    lean,
+    lspec,
+    ...
+  } : flake-parts.lib.mkFlake { inherit inputs; } {
+    flake = {
+    };
+    systems = [
+      "x86_64-linux"
+      "x86_64-darwin"
+    ];
+    perSystem = { system, pkgs, ... }: let
+      leanPkgs = lean.packages.${system};
+      lspecLib = leanPkgs.buildLeanPackage {
+        name = "LSpec";
+        roots = [ "Main" "LSpec" ];
+        src = "${lspec}";
+      };
+      project = leanPkgs.buildLeanPackage {
+        name = "Pantograph";
+        roots = [ "Main" "Pantograph" ];
+        src = pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "/Test/" path) &&
+            !(pkgs.lib.hasSuffix ".md" path) &&
+            !(pkgs.lib.hasSuffix "Makefile" path);
+        };
+      };
+      test = leanPkgs.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 project ];
+        src = pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "Pantograph" path);
+        };
+      };
+    in rec {
+      packages = {
+        inherit (leanPkgs) lean lean-all;
+        inherit (project) sharedLib executable;
+        default = project.executable;
+      };
+      checks = {
+        test = pkgs.runCommand "test" {
+          buildInputs = [ test.executable leanPkgs.lean-all ];
+        } ''
+          #export LEAN_SRC_PATH="${./.}"
+          ${test.executable}/bin/test > $out
+        '';
+      };
+      devShells.default = pkgs.mkShell {
+        buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
+      };
+    };
+  };
+}

lake-manifest.json

@@ -0,0 +1,14 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/lurk-lab/LSpec.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "pantograph",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -1,19 +1,25 @@
 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
+  defaultFacets := #[LeanLib.sharedFacet]
 }
 
 @[default_target]
 lean_exe pantograph {
   root := `Main
+  -- Somehow solves the native symbol not found problem
+  supportInterpreter := true
+}
+
+require LSpec from git
+  "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
+lean_lib Test {
+}
+lean_exe test {
+  root := `Test.Main
+  -- Somehow solves the native symbol not found problem
+  supportInterpreter := true
 }

lean-toolchain

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