Merge pull request 'feat: Allow selective continuation of goals' (#27) from goal/continuation into dev

Reviewed-on: #27

.gitignore

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

Main.lean

@@ -1,4 +1,115 @@
+import Lean.Data.Json
+import Lean.Environment
+
+import Pantograph.Version
 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
+
+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
+
+
+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
+
+  Lean.enableInitializersExecution
+  Lean.initSearchPath (← Lean.findSysroot)
+
+  let options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
+    |>.foldlM Lean.setOptionFromString' Lean.Options.empty
+    |>.run
+  let options ← match options? with
+    | .ok options => pure options
+    | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
+  let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
+
+  let env ← Lean.importModules
+    (imports := imports.toArray.map (λ str => { module := str.toName, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+  let context: Context := {
+    imports
+  }
+  let coreContext: Lean.Core.Context := {
+    currNamespace := Lean.Name.str .anonymous "Aniva"
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph>",
+    fileMap := { source := "", positions := #[0], lines := #[1] },
+    options := options
+  }
+  try
+    let termElabM := loop.run context |>.run' {}
+    let metaM := termElabM.run' (ctx := {
+      declName? := some "_pantograph",
+      errToSorry := false
+    })
+    let coreM := metaM.run'
+    IO.println "ready."
+    discard <| coreM.toIO coreContext { env := env }
+  catch ex =>
+    IO.println "Uncaught IO exception"
+    IO.println ex.toString

Makefile

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

Pantograph.lean

@@ -1 +1,223 @@
-def hello := "world"
+import Pantograph.Goal
+import Pantograph.Protocol
+import Pantograph.Serial
+import Pantograph.Symbol
+import Lean.Data.HashMap
+
+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.Elab.TermElabM)
+-- 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
+  | "lib.catalog"   => run lib_catalog
+  | "lib.inspect"   => run lib_inspect
+  | "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
+  | cmd =>
+    let error: Protocol.InteractionError :=
+      errorCommand s!"Unknown command {cmd}"
+    return Lean.toJson error
+  where
+  errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
+  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 }
+  lib_catalog (_: Protocol.LibCatalog): MainM (CR Protocol.LibCatalogResult) := do
+    let env ← Lean.MonadEnv.getEnv
+    let names := env.constants.fold (init := #[]) (λ acc name info =>
+      match to_filtered_symbol name info with
+      | .some x => acc.push x
+      | .none => acc)
+    return .ok { symbols := names }
+  lib_inspect (args: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do
+    let state ← get
+    let env ← Lean.MonadEnv.getEnv
+    let name :=  args.name.toName
+    let info? := env.find? name
+    match info? with
+    | none => return .error $ errorIndex s!"Symbol not found {args.name}"
+    | some 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
+      return .ok {
+        type := ← serialize_expression state.options info.type,
+        value? := ← value?.mapM (λ v => serialize_expression state.options v),
+        module? := module?
+      }
+  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
+    let state ← get
+    let env ← Lean.MonadEnv.getEnv
+    match syntax_from_str env args.expr with
+    | .error str => return .error $ errorI "parsing" str
+    | .ok syn => do
+      match (← syntax_to_expr syn) with
+      | .error str => return .error $ errorI "elab" str
+      | .ok expr => do
+        try
+          let type ← Lean.Meta.inferType expr
+          return .ok {
+              type := (← serialize_expression (options := state.options) type),
+              expr := (← serialize_expression (options := state.options) expr)
+          }
+        catch exception =>
+          return .error $ errorI "typing" (← exception.toMessageData.toString)
+  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,
+        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.OptionsPrintResult) := 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 _ Lean.Expr ← (match args.expr, args.copyFrom with
+      | .some expr, .none =>
+        (match syntax_from_str env expr with
+        | .error str => return .error <| errorI "parsing" str
+        | .ok syn => do
+          (match (← syntax_to_expr syn) with
+          | .error str => return .error <| errorI "elab" str
+          | .ok expr => return .ok expr))
+      | .none, .some copyFrom =>
+        (match env.find? <| copyFrom.toName with
+        | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
+        | .some cInfo => return .ok cInfo.type)
+      | _, _ =>
+        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
+    match expr? with
+    | .error error => return .error error
+    | .ok expr =>
+      let goalState ← GoalState.create expr
+      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? with
+        | .some tactic, .none => do
+          pure ( Except.ok (← GoalState.execute goalState args.goalId tactic))
+        | .none, .some expr => do
+          pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr))
+        | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} 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)
+        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 (.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 $ target.continue branch
+        | .none, .some goals =>
+          let goals := goals.map (λ name => { name := name.toName })
+          pure $ target.resume goals
+        | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
+      match nextState? with
+      | .error error => return .ok { error? := .some error }
+      | .ok nextGoalState =>
+        let nextStateId := state.nextId
+        set { state with
+          goalStates := state.goalStates.insert nextStateId nextGoalState,
+          nextId := state.nextId + 1
+        }
+        let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options)
+        return .ok {
+          nextStateId? := .some nextStateId,
+          goals? := .some 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 => do
+      let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
+      return .ok {
+        root?,
+      }
+
+end Pantograph

Pantograph/Goal.lean

@@ -0,0 +1,213 @@
+import Lean
+
+import Pantograph.Symbol
+
+def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
+  {
+    msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
+  }
+
+
+namespace Pantograph
+open Lean
+
+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
+
+  -- The id of the goal in the parent
+  parentGoalId: Nat := 0
+
+abbrev M := Elab.TermElabM
+
+protected def GoalState.create (expr: Expr): M 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 {
+    savedState,
+    root,
+    newMVars := SSet.insert .empty root,
+  }
+protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
+
+protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do
+  state.savedState.term.restore
+  m
+
+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
+private def GoalState.mvars (state: GoalState): SSet MVarId :=
+  state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
+
+/-- Inner function for executing tactic on goal state -/
+def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
+    M (Except (Array String) Elab.Tactic.SavedState):= do
+  let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do
+    state.restore
+    Elab.Tactic.setGoals [goal]
+    try
+      Elab.Tactic.evalTactic stx
+      if (← getThe Core.State).messages.hasErrors then
+        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+        let errors ← (messages.map Message.data).mapM fun md => md.toString
+        return .error errors
+      else
+        return .ok (← MonadBacktrack.saveState)
+    catch exception =>
+      return .error #[← exception.toMessageData.toString]
+  tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
+
+/-- 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)
+
+/-- Execute tactic on given state -/
+protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
+    M TacticResult := do
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure $ goal
+    | .none => return .indexError goalId
+  let tactic ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `tactic)
+    (input := tactic)
+    (fileName := "<stdin>") with
+    | .ok stx => pure $ stx
+    | .error error => return .parseError error
+  match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
+  | .error errors =>
+    return .failure errors
+  | .ok nextSavedState =>
+    -- Assert that the definition of metavariables are the same
+    let nextMCtx := nextSavedState.term.meta.meta.mctx
+    let prevMCtx := state.savedState.term.meta.meta.mctx
+    -- 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 ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
+      if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
+        assert! prevMVarDecl.type == mvarDecl.type
+        return acc
+      else
+        return acc.insert mvarId
+      ) SSet.empty
+    return .success {
+      state with
+      savedState := nextSavedState
+      newMVars,
+      parentGoalId := goalId,
+    }
+
+protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let expr ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := expr)
+    (fileName := "<stdin>") with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let tacticM:  Elab.Tactic.TacticM TacticResult := do
+    state.savedState.restore
+    Elab.Tactic.setGoals [goal]
+    try
+      let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
+      -- Attempt to unify the expression
+      let goalType ← goal.getType
+      let exprType ← Meta.inferType expr
+      if !(← Meta.isDefEq goalType exprType) then
+        return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)]
+      goal.checkNotAssigned `GoalState.tryAssign
+      goal.assign expr
+      if (← getThe Core.State).messages.hasErrors then
+        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+        let errors ← (messages.map Message.data).mapM fun md => md.toString
+        return .failure errors
+      else
+        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 ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
+          if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
+            assert! prevMVarDecl.type == mvarDecl.type
+            return acc
+          else
+            return mvarId :: acc
+          ) []
+        -- The new goals are the newMVars that lack an assignment
+        Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
+        let nextSavedState ← MonadBacktrack.saveState
+        return .success {
+          state with
+          savedState := nextSavedState,
+          newMVars := newMVars.toSSet,
+          parentGoalId := goalId,
+        }
+    catch exception =>
+      return .failure #[← exception.toMessageData.toString]
+  tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+
+/--
+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
+    .error s!"Goals not in scope"
+  else
+    -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
+    let unassigned := goals.filter (λ goal =>
+      let mctx := state.mctx
+      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
+    .ok {
+      state with
+      savedState := {
+        term := state.savedState.term,
+        tactic := { goals := unassigned },
+      },
+    }
+
+/--
+Brings into scope all goals from `branch`
+-/
+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 :=
+  let expr := goalState.mctx.eAssignment.find! goalState.root
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  if expr.hasMVar 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
+    .some expr
+
+end Pantograph

Pantograph/Protocol.lean

@@ -0,0 +1,208 @@
+/-
+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
+  -- 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
+  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
+
+
+--- 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
+  deriving Lean.FromJson
+structure ExprEchoResult where
+  expr: Expression
+  type: Expression
+  deriving Lean.ToJson
+
+-- Print all symbols in environment
+structure LibCatalog where
+  deriving Lean.FromJson
+structure LibCatalogResult where
+  symbols: Array String
+  deriving Lean.ToJson
+-- Print the type of a symbol
+structure LibInspect 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
+  deriving Lean.FromJson
+structure LibInspectResult where
+  type: Expression
+  value?: Option Expression := .none
+  module?: Option String
+  deriving Lean.ToJson
+
+/-- Set options; See `Options` struct above for meanings -/
+structure OptionsSet where
+  printJsonPretty?: Option Bool
+  printExprPretty?: Option Bool
+  printExprAST?: 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
+abbrev OptionsPrintResult := Options
+
+structure GoalStart where
+  -- Only one of the fields below may be populated.
+  expr: Option String     -- Directly parse in an expression
+  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
+  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 (List String) := .none
+  deriving Lean.FromJson
+structure GoalContinueResult where
+  error?: Option String := .none
+  nextStateId?: Option Nat := .none
+  goals?: Option (Array Goal) := .none
+  deriving Lean.ToJson
+
+-- Remove goal states
+structure GoalDelete where
+  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
+  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
+
+
+end Pantograph.Protocol

Pantograph/Serial.lean

@@ -0,0 +1,301 @@
+/-
+All serialisation functions
+-/
+import Lean
+
+import Pantograph.Protocol
+import Pantograph.Goal
+
+namespace Pantograph
+open Lean
+
+--- Input Functions ---
+
+
+/-- Read a theorem from the environment -/
+def expr_from_const (env: Environment) (name: Name): Except String Lean.Expr :=
+  match env.find? name with
+  | none       => throw s!"Symbol not found: {name}"
+  | some cInfo => return cInfo.type
+/-- Read syntax object from string -/
+def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
+  Parser.runParserCategory
+    (env := env)
+    (catName := `term)
+    (input := s)
+    (fileName := "<stdin>")
+
+
+def syntax_to_expr_type (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 syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
+  try
+    let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
+    return .ok expr
+  catch ex => return .error (← ex.toMessageData.toString)
+
+
+--- Output Functions ---
+
+def type_expr_to_bound (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 name_to_ast (name: Name) (sanitize: Bool := true): String :=
+  let internal := name.isInaccessibleUserName || name.hasMacroScopes
+  if sanitize && internal then "_"
+  else toString name |> enclose_if_escaped
+  where
+  enclose_if_escaped (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 serialize_sort_level_ast (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 := serialize_sort_level_ast v sanitize
+      let w := serialize_sort_level_ast w sanitize
+      s!"(:max {v} {w})"
+    | .imax v w =>
+      let v := serialize_sort_level_ast v sanitize
+      let w := serialize_sort_level_ast w sanitize
+      s!"(:imax {v} {w})"
+    | .param name =>
+      let name := name_to_ast name sanitize
+      s!"{name}"
+    | .mvar id =>
+      let name := name_to_ast 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
+-/
+partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
+  self expr
+  where
+  self (e: Expr): String :=
+    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.
+      s!"{deBruijnIndex}"
+    | .fvar fvarId =>
+      let name := of_name fvarId.name
+      s!"(:fv {name})"
+    | .mvar mvarId =>
+      let name := of_name mvarId.name
+      s!"(:mv {name})"
+    | .sort level =>
+      let level := serialize_sort_level_ast level sanitize
+      s!"(:sort {level})"
+    | .const declName _ =>
+      -- The universe level of the const expression is elided since it should be
+      -- inferrable from surrounding expression
+      s!"(:c {declName})"
+    | .app _ _ =>
+      let fn' := self e.getAppFn
+      let args := e.getAppArgs.map self |>.toList
+      let args := " ".intercalate args
+      s!"({fn'} {args})"
+    | .lam binderName binderType body binderInfo =>
+      let binderName' := of_name binderName
+      let binderType' := self binderType
+      let body' := self body
+      let binderInfo' := binder_info_to_ast binderInfo
+      s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
+    | .forallE binderName binderType body binderInfo =>
+      let binderName' := of_name binderName
+      let binderType' := self binderType
+      let body' := self body
+      let binderInfo' := binder_info_to_ast binderInfo
+      s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
+    | .letE name type value body _ =>
+      -- Dependent boolean flag diacarded
+      let name' := name_to_ast name
+      let type' := self type
+      let value' := self value
+      let body' := self body
+      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}\""
+      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 struct =>
+      let struct' := self struct
+      s!"(:proj {typeName} {idx} {struct'})"
+  -- Elides all unhygenic names
+  binder_info_to_ast : Lean.BinderInfo → String
+    | .default => ""
+    | .implicit => " :implicit"
+    | .strictImplicit => " :strictImplicit"
+    | .instImplicit => " :instImplicit"
+  of_name (name: Name) := name_to_ast name sanitize
+
+def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
+  let pp := toString (← Meta.ppExpr e)
+  let pp?: Option String := match options.printExprPretty with
+    | true => .some pp
+    | false => .none
+  let sexp: String := serialize_expression_ast e
+  let sexp?: Option String := match options.printExprAST with
+    | true => .some sexp
+    | false => .none
+  return {
+    pp?,
+    sexp?
+  }
+
+/-- Adapted from ppGoal -/
+def serialize_goal (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 := of_name fvarId.name,
+          userName:= of_name userName.simpMacroScopes,
+        }
+      | .ldecl _ fvarId userName _ _ _ _ => do
+        return {
+          name := of_name 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 ← instantiateMVars type
+        return {
+          name := of_name fvarId.name,
+          userName:= of_name userName,
+          isInaccessible? := .some userName.isInaccessibleUserName
+          type? := .some (← serialize_expression options type)
+        }
+      | .ldecl _ fvarId userName type val _ _ => do
+        let userName := userName.simpMacroScopes
+        let type ← instantiateMVars type
+        let value? ← if showLetValues then
+          let val ← instantiateMVars val
+          pure $ .some (← serialize_expression options val)
+        else
+          pure $ .none
+        return {
+          name := of_name fvarId.name,
+          userName:= of_name userName,
+          isInaccessible? := .some userName.isInaccessibleUserName
+          type? := .some (← serialize_expression 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 := of_name goal.name,
+      userName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
+      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
+      target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
+      vars := vars.reverse.toArray
+    }
+  where
+  of_name (n: Name) := name_to_ast n (sanitize := false)
+
+protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do
+  let goals := state.goals.toArray
+  state.savedState.term.meta.restore
+  let parentDecl? := parent.bind (λ parentState =>
+    let parentGoal := parentState.goals.get! state.parentGoalId
+    parentState.mctx.findDecl? parentGoal)
+  goals.mapM fun goal => do
+    match state.mctx.findDecl? goal with
+    | .some mvarDecl =>
+      let serializedGoal ← serialize_goal 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.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
+  let savedState := goalState.savedState
+  savedState.term.meta.restore
+  let goals := savedState.tactic.goals
+  let mctx ← getMCtx
+  let root := goalState.root
+  -- Print the root
+  match mctx.decls.find? root with
+  | .some decl => printMVar ">" root decl
+  | .none => IO.println s!">{root.name}: ??"
+  goals.forM (fun mvarId => do
+    if mvarId != root then
+      match mctx.decls.find? mvarId with
+      | .some decl => printMVar "⊢" mvarId decl
+      | .none => IO.println s!"⊢{mvarId.name}: ??"
+  )
+  let goals := goals.toSSet
+  mctx.decls.forM (fun mvarId decl => do
+    if goals.contains mvarId || mvarId == root then
+      pure ()
+    -- Always print the root goal
+    else if mvarId == goalState.root then
+      printMVar (pref := ">") mvarId decl
+    -- Print the remainig ones that users don't see in Lean
+    else if options.printAll then
+      let pref := if goalState.newMVars.contains mvarId then "~" else " "
+      printMVar pref mvarId decl
+    else
+      pure ()
+      --IO.println s!" {mvarId.name}{userNameToString decl.userName}"
+  )
+  where
+    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
+      if options.printContext then
+        decl.lctx.fvarIdToDecl.forM printFVar
+      let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
+      IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
+      if options.printValue then
+        if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
+          IO.println s!"  = {← Meta.ppExpr value}"
+    printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
+      IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
+    userNameToString : Name → String
+      | .anonymous => ""
+      | other => s!"[{other}]"
+
+end Pantograph

Pantograph/Symbol.lean

@@ -0,0 +1,32 @@
+import Lean.Declaration
+
+namespace Pantograph
+
+def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
+  let nameDeduce: Bool := match n.getRoot with
+  | .str _ name => name.startsWith "_" ∨ name == "Lean"
+  | _ => true
+  let stemDeduce: Bool := match n with
+  | .anonymous => true
+  | .str _ name => name.startsWith "_"
+  | .num _ _ => true
+  nameDeduce ∨ stemDeduce ∨ info.isUnsafe
+
+def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+  let pref := match info with
+  | .axiomInfo  _ => "axiom"
+  | .defnInfo   _ => "defn"
+  | .thmInfo    _ => "thm"
+  | .opaqueInfo _ => "opaque"
+  | .quotInfo   _ => "quot"
+  | .inductInfo _ => "induct"
+  | .ctorInfo   _ => "ctor"
+  | .recInfo    _ => "rec"
+  s!"{pref}|{toString n}"
+
+def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
+  if is_symbol_unsafe_or_internal n info
+  then Option.none
+  else Option.some <| to_compact_symbol_name n info
+
+end Pantograph

Pantograph/Version.lean

@@ -0,0 +1,5 @@
+namespace Pantograph
+
+def version := "0.2.8"
+
+end Pantograph

README.md

@@ -0,0 +1,112 @@
+# Pantograph
+
+An interaction system for Lean 4.
+
+![Pantograph](doc/icon.svg)
+
+## Installation
+
+Install `elan` and `lake`. Execute
+``` sh
+make build/bin/pantograph
+```
+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`,
+``` 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 provided `flake.nix` has a develop environment with Lean already setup.
+
+## 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
+lib.catalog
+lib.inspect {"name": "Nat.le_add_left"}
+```
+Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
+```
+$ pantograph Mathlib.Analysis.Seminorm
+lib.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
+- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
+- `lib.catalog`: Display a list of all safe Lean symbols in the current context
+- `lib.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>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
+- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
+- `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: Continue from a proof state
+- `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
+- `goal.print {"stateId": <id>}"`: Print a goal state
+- `stat`: Display resource usage
+
+## 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
+```
+
+## Testing
+
+The tests are based on `LSpec`. To run tests,
+``` sh
+make test
+```

Test/Common.lean

@@ -0,0 +1,35 @@
+import Pantograph.Protocol
+import Pantograph.Goal
+import LSpec
+
+namespace Pantograph
+
+namespace Protocol
+/-- Set internal names to "" -/
+def Goal.devolatilize (goal: Goal): Goal :=
+  {
+    goal with
+    name := "",
+    vars := goal.vars.map removeInternalAux,
+  }
+  where removeInternalAux (v: Variable): Variable :=
+    {
+      v with
+      name := ""
+    }
+deriving instance DecidableEq, Repr for Expression
+deriving instance DecidableEq, Repr for Variable
+deriving instance DecidableEq, Repr for Goal
+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}"
+
+def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
+
+end Pantograph

Test/Holes.lean

@@ -0,0 +1,217 @@
+import LSpec
+import Pantograph.Goal
+import Pantograph.Serial
+import Test.Common
+
+namespace Pantograph.Test.Holes
+open Pantograph
+open Lean
+
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
+
+def addTest (test: LSpec.TestSeq): TestM Unit := do
+  set $ (← get) ++ test
+
+def startProof (expr: String): TestM (Option GoalState) := do
+  let env ← Lean.MonadEnv.getEnv
+  let syn? := syntax_from_str 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? ← syntax_to_expr_type 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 := {
+    currNamespace := Name.append .anonymous "Aniva",
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph>",
+    fileMap := { source := "", positions := #[0], lines := #[1] }
+  }
+  let metaM := termElabM.run' (ctx := {
+    declName? := some "_pantograph",
+    errToSorry := false
+  })
+  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.execute (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.execute (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
+  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.execute (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.execute (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.execute (goalId := 2) (tactic := "apply Nat.succ") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "apply Nat.succ" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "Nat"])
+
+  -- Execute a partial continuation
+  let coupled_goals := state1.goals ++ state2.goals
+  let state1b ← match state2.resume (goals := coupled_goals) with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+
+  -- Roundtrip
+  --let coupled_goals := coupled_goals.map (λ g =>
+  --  { name := str_to_name $ name_to_ast g.name (sanitize := false)})
+  let coupled_goals := coupled_goals.map (λ g => name_to_ast g.name (sanitize := false))
+  let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
+  let state1b ← match state2.resume (goals := coupled_goals) with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+
+  -- Continuation should fail if the state does not exist:
+  match state0.resume coupled_goals with
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals 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: IO LSpec.TestSeq := do
+  let env: Lean.Environment ← Lean.importModules
+    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+  let tests := [
+    ("2 < 5", test_m_couple),
+    ("Proposition Generation", test_proposition_generation),
+    ("Partial Continuation", test_partial_continuation)
+  ]
+  let tests ← tests.foldlM (fun acc tests => do
+    let (name, tests) := tests
+    let tests ← proofRunner env tests
+    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
+
+  return LSpec.group "Holes" tests
+
+end Pantograph.Test.Holes

Test/Integration.lean

@@ -0,0 +1,128 @@
+/- 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 := {
+    currNamespace := Lean.Name.str .anonymous "Aniva"
+    openDecls := [],
+    fileName := "<Test>",
+    fileMap := { source := "", positions := #[0], lines := #[1] },
+    options := Lean.Options.empty
+  }
+  let commands: MainM LSpec.TestSeq :=
+    steps.foldlM (λ suite step => do
+      let result ← step
+      return suite ++ result) LSpec.TestSeq.done
+  try
+    let termElabM := commands.run context |>.run' {}
+    let metaM := termElabM.run' (ctx := {
+      declName? := some "_pantograph",
+      errToSorry := false
+    })
+    let coreM := metaM.run'
+    return Prod.fst $ (← coreM.toIO coreContext { env := env })
+  catch ex =>
+    return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
+
+def test_option_modify : IO LSpec.TestSeq :=
+  let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
+  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 "lib.inspect"
+      [("name", .str "Nat.add_one")]
+     (Lean.toJson ({
+       type := { pp? }, module? }:
+      Protocol.LibInspectResult)),
+    subroutine_step "options.set"
+      [("printExprAST", .bool true)]
+     (Lean.toJson ({ }:
+      Protocol.OptionsSetResult)),
+    subroutine_step "lib.inspect"
+      [("name", .str "Nat.add_one")]
+     (Lean.toJson ({
+       type := { pp?, sexp? }, module? }:
+      Protocol.LibInspectResult)),
+    subroutine_step "options.print"
+      []
+     (Lean.toJson ({ options with printExprAST := true }:
+      Protocol.OptionsPrintResult))
+  ]
+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.10",
+    target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
+    vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
+  }
+  let goal2: Protocol.Goal := {
+    name := "_uniq.13",
+    target := { pp? := .some "x ∨ y → y ∨ x" },
+    vars := #[
+      { name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
+      { name := "_uniq.12", 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.8"}:
+      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.tactic"
+      [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
+     (Lean.toJson ({
+       nextStateId? := .some 2,
+       goals? := #[goal2],
+     }:
+      Protocol.GoalTacticResult))
+  ]
+
+def suite: IO LSpec.TestSeq := do
+
+  return LSpec.group "Integration" $
+    (LSpec.group "Option modify" (← test_option_modify)) ++
+    (LSpec.group "Malformed command" (← test_malformed_command)) ++
+    (LSpec.group "Tactic" (← test_tactic))
+
+
+end Pantograph.Test.Integration

Test/Main.lean

@@ -0,0 +1,19 @@
+import LSpec
+import Test.Holes
+import Test.Integration
+import Test.Proofs
+import Test.Serial
+
+open Pantograph.Test
+
+def main := do
+  Lean.initSearchPath (← Lean.findSysroot)
+
+  let suites := [
+    Holes.suite,
+    Integration.suite,
+    Proofs.suite,
+    Serial.suite
+  ]
+  let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
+  LSpec.lspecIO $ all

Test/Proofs.lean

@@ -0,0 +1,309 @@
+/-
+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 M)
+
+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? := syntax_from_str 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? ← syntax_to_expr_type 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 := {
+    currNamespace := Name.append .anonymous "Aniva",
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph>",
+    fileMap := { source := "", positions := #[0], lines := #[1] }
+  }
+  let metaM := termElabM.run' (ctx := {
+    declName? := some "_pantograph",
+    errToSorry := false
+  })
+  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
+
+-- Individual test cases
+example: ∀ (a b: Nat), a + b = b + a := by
+  intro n m
+  rw [Nat.add_comm]
+def proof_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.execute (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.execute (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.execute (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 proof_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.execute (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.execute (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 proof_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 state1 ← match ← state0.execute (goalId := 0) (tactic := "intros") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "intros" (state1.goals.length = 1)
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+  let state2 ← match ← state1.execute (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 state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "assumption" 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 proof_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 ()
+
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") 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 [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
+  let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[branchGoal "inl" "p", branchGoal "inr" "q"])
+
+  let state3_1 ← match ← state2.execute (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.execute (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?.isNone
+  let state3_2 ← match ← state2.execute (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.execute (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.execute (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.execute (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 suite: IO LSpec.TestSeq := do
+  let env: Lean.Environment ← Lean.importModules
+    (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
+    (opts := {})
+    (trustLevel := 1)
+  let tests := [
+    ("Nat.add_comm", proof_nat_add_comm false),
+    ("Nat.add_comm manual", proof_nat_add_comm true),
+    ("Nat.add_comm delta", proof_delta_variable),
+    ("arithmetic", proof_arith),
+    ("Or.comm", proof_or_comm)
+  ]
+  let tests ← tests.foldlM (fun acc tests => do
+    let (name, tests) := tests
+    let tests ← proofRunner env tests
+    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
+
+  return LSpec.group "Proofs" tests
+
+end Pantograph.Test.Proofs

Test/Serial.lean

@@ -0,0 +1,81 @@
+import LSpec
+import Pantograph.Serial
+import Pantograph.Symbol
+
+namespace Pantograph.Test.Serial
+
+open Pantograph
+open Lean
+
+deriving instance Repr, DecidableEq for Protocol.BoundExpression
+
+def test_name_to_ast: LSpec.TestSeq :=
+  let quote := "\""
+  let escape := "\\"
+  LSpec.test "a.b.1" (name_to_ast (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
+  LSpec.test "seg.«a.b»" (name_to_ast (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++
+  -- Pathological test case
+  LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (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", "Nat.succ n ≤ m")], target := "n ≤ m" })
+  ]
+  let coreM: CoreM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
+    let env ← MonadEnv.getEnv
+    let expr := env.find? symbol |>.get! |>.type
+    let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target)
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
+  let coreContext: Core.Context := {
+    currNamespace := Lean.Name.str .anonymous "Aniva"
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph/Test>",
+    fileMap := { source := "", positions := #[0], lines := #[1] }
+  }
+  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_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)))")
+  ]
+  let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
+    let env ← MonadEnv.getEnv
+    let expr := env.find? symbol.toName |>.get! |>.type
+    let test := LSpec.check symbol ((serialize_expression_ast expr) = target)
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
+  let coreM := metaM.run'
+  let coreContext: Core.Context := {
+    currNamespace := Lean.Name.str .anonymous "Aniva"
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph/Test>",
+    fileMap := { source := "", positions := #[0], lines := #[1] }
+  }
+  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 suite: IO LSpec.TestSeq := do
+  let env: Environment ← importModules
+    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+
+  return LSpec.group "Serialization" $
+    (LSpec.group "name_to_ast" test_name_to_ast) ++
+    (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
+    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))
+
+end Pantograph.Test.Serial

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,202 @@
+{
+  "nodes": {
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib"
+      },
+      "locked": {
+        "lastModified": 1696343447,
+        "narHash": "sha256-B2xAZKLkkeRFG5XcHHSXXcP7To9Xzr59KXeZiRf4vdQ=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "c9afaba3dfa4085dbd2ccb38dfade5141e33d9d4",
+        "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"
+      },
+      "locked": {
+        "lastModified": 1695693562,
+        "narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=",
+        "owner": "leanprover",
+        "repo": "lean4",
+        "rev": "a832f398b80a5ebb820d27b9e55ec949759043ff",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover",
+        "ref": "v4.1.0",
+        "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"
+      }
+    },
+    "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": 1696019113,
+        "narHash": "sha256-X3+DKYWJm93DRSdC5M6K5hLqzSya9BjibtBsuARoPco=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "f5892ddac112a1e9b3612c39af1b72987ee5783a",
+        "type": "github"
+      },
+      "original": {
+        "dir": "lib",
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "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": 1697456312,
+        "narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "ca012a02bf8327be9e488546faecae5e05d7d749",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "lean": "lean",
+        "nixpkgs": "nixpkgs_3"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,38 @@
+{
+  description = "Pantograph";
+
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+    flake-parts.url = "github:hercules-ci/flake-parts";
+    lean.url = "github:leanprover/lean4?ref=v4.1.0";
+  };
+
+  outputs = inputs @ {
+    self,
+    nixpkgs,
+    flake-parts,
+    lean,
+    ...
+  } : flake-parts.lib.mkFlake { inherit inputs; } {
+    flake = {
+    };
+    systems = [
+      "x86_64-linux"
+      "x86_64-darwin"
+    ];
+    perSystem = { system, pkgs, ... }: let
+      leanPkgs = lean.packages.${system};
+      project = leanPkgs.buildLeanPackage {
+        name = "Pantograph";
+        roots = [ "Main" "Pantograph" ];
+        src = ./.;
+      };
+    in rec {
+      packages = project // {
+        inherit (leanPkgs) lean;
+        default = packages.executable;
+      };
+      devShells.default = project.devShell;
+    };
+  };
+}

lake-manifest.json

@@ -0,0 +1,11 @@
+{"version": 5,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/lurk-lab/LSpec.git",
+    "subDir?": null,
+    "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
+    "opts": {},
+    "name": "LSpec",
+    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
+    "inherited": false}}]}

lakefile.lean

@@ -1,19 +1,24 @@
 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
 }
 
 @[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" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
+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:4.1.0