Merge branch 'dev' into frontend/infotree

.gitignore

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

Pantograph/Delate.lean

@@ -327,11 +327,11 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       -- Lean these are handled using a `#` prefix.
       pure s!"{deBruijnIndex}"
     | .fvar fvarId =>
-      let name := ofName fvarId.name
+      let name := fvarId.name
       pure s!"(:fv {name})"
     | .mvar mvarId => do
         let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
-        let name := ofName mvarId.name
+        let name := mvarId.name
         pure s!"(:{pref} {name})"
     | .sort level =>
       let level := serializeSortLevel level sanitize
@@ -346,20 +346,20 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       let args := " ".intercalate args
       pure s!"({fn'} {args})"
     | .lam binderName binderType body binderInfo => do
-      let binderName' := ofName binderName
+      let binderName' := binderName.eraseMacroScopes
       let binderType' ← self binderType
       let body' ← self body
       let binderInfo' := binderInfoSexp binderInfo
       pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
     | .forallE binderName binderType body binderInfo => do
-      let binderName' := ofName binderName
+      let binderName' := binderName.eraseMacroScopes
       let binderType' ← self binderType
       let body' ← self body
       let binderInfo' := binderInfoSexp binderInfo
       pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
     | .letE name type value body _ => do
       -- Dependent boolean flag diacarded
-      let name' := serializeName name
+      let name' := name.eraseMacroScopes
       let type' ← self type
       let value' ← self value
       let body' ← self body
@@ -387,7 +387,6 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
     | .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
@@ -420,13 +419,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
       match localDecl with
       | .cdecl _ fvarId userName _ _ _ =>
         return {
-          name := ofName fvarId.name,
+          name := fvarId.name.toString,
           userName:= ofName userName.simpMacroScopes,
           isInaccessible := userName.isInaccessibleUserName
         }
       | .ldecl _ fvarId userName _ _ _ _ => do
         return {
-          name := ofName fvarId.name,
+          name := fvarId.name.toString,
           userName := toString userName.simpMacroScopes,
           isInaccessible := userName.isInaccessibleUserName
         }
@@ -436,7 +435,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         let userName := userName.simpMacroScopes
         let type ← instantiate type
         return {
-          name := ofName fvarId.name,
+          name := fvarId.name.toString,
           userName:= ofName userName,
           isInaccessible := userName.isInaccessibleUserName
           type? := .some (← serializeExpression options type)
@@ -450,7 +449,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         else
           pure $ .none
         return {
-          name := ofName fvarId.name,
+          name := fvarId.name.toString,
           userName:= ofName userName,
           isInaccessible := userName.isInaccessibleUserName
           type? := .some (← serializeExpression options type)
@@ -469,7 +468,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
           | false => ppVar localDecl
         return var::acc
     return {
-      name := ofName goal.name,
+      name := goal.name.toString,
       userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
       isConversion := isLHSGoal? mvarDecl.type |>.isSome,
       target := (← serializeExpression options (← instantiate mvarDecl.type)),

Pantograph/Goal.lean

@@ -10,8 +10,6 @@ import Lean
 namespace Pantograph
 open Lean
 
-def filename: String := "<pantograph>"
-
 /--
 Represents an interconnected set of metavariables, or a state in proof search
  -/
@@ -73,6 +71,8 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O
   return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
 protected def GoalState.metaState (state: GoalState): Meta.State :=
   state.savedState.term.meta.meta
+protected def GoalState.coreState (state: GoalState): Core.SavedState :=
+  state.savedState.term.meta.core
 
 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
   mvarId.withContext m |>.run' (← read) state.metaState
@@ -202,16 +202,27 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message: String)
 
-/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
+/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
 protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit):
       Elab.TermElabM TacticResult := do
   try
     let nextState ← state.step goal tacticM
+
+    -- Check if error messages have been generated in the core.
+    let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length
+      |>.filterMapM λ m => do
+        if m.severity == .error then
+          return .some $ ← m.toString
+        else
+          return .none
+    if ¬ newMessages.isEmpty then
+      return .failure newMessages.toArray
     return .success nextState
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
 /-- Execute a string tactic on given state. Restores TermElabM -/
+@[export pantograph_goal_state_try_tactic_m]
 protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
     Elab.TermElabM TacticResult := do
   state.restoreElabM
@@ -219,7 +230,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
     (env := ← MonadEnv.getEnv)
     (catName := if state.isConv then `conv else `tactic)
     (input := tactic)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
   state.tryTacticM goal $ Elab.Tactic.evalTactic tactic
@@ -231,7 +242,7 @@ protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: Strin
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := expr)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.tryTacticM goal $ Tactic.evalAssign expr
@@ -245,7 +256,7 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := type)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.tryTacticM goal $ Tactic.evalLet binderName.toName type
@@ -332,7 +343,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
     (env := state.env)
     (catName := `term)
     (input := pred)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   goal.checkNotAssigned `GoalState.tryCalc
@@ -353,7 +364,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
       throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
     if let some prevRhs := calcPrevRhs? then
       unless ← Meta.isDefEqGuarded lhs prevRhs do
-        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- "
+        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}"
 
     -- Creates a mvar to represent the proof that the calc tactic solves the
     -- current branch

Pantograph/Protocol.lean

@@ -289,6 +289,19 @@ structure GoalDiag where
   instantiate: Bool := true
   printSexp: Bool := false
 
+structure GoalSave where
+  id: Nat
+  path: System.FilePath
+  deriving Lean.FromJson
+structure GoalSaveResult where
+  deriving Lean.ToJson
+structure GoalLoad where
+  path: System.FilePath
+  deriving Lean.FromJson
+structure GoalLoadResult where
+  id: Nat
+  deriving Lean.ToJson
+
 
 /-- Executes the Lean compiler on a single file -/
 structure FrontendProcess where

Pantograph/Serial.lean

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

README.md

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

Repl.lean

@@ -15,6 +15,16 @@ structure State where
 /-- Main state monad for executing commands -/
 abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
 
+def newGoalState (goalState: GoalState) : MainM Nat := do
+  let state ← get
+  let stateId := state.nextId
+  set { state with
+    goalStates := state.goalStates.insert stateId goalState,
+    nextId := state.nextId + 1
+  }
+  return stateId
+
+
 -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
 -- certain monadic features in `MainM`
 abbrev CR α := Except Protocol.InteractionError α
@@ -50,6 +60,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     | "goal.continue" => run goal_continue
     | "goal.delete"   => run goal_delete
     | "goal.print"    => run goal_print
+    | "goal.save"     => run goal_save
+    | "goal.load"     => run goal_load
     | "frontend.process"  => run frontend_process
     | cmd =>
       let error: Protocol.InteractionError :=
@@ -62,14 +74,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   errorCommand := errorI "command"
   errorIndex := errorI "index"
   errorIO := errorI "io"
-  newGoalState (goalState: GoalState) : MainM Nat := do
-    let state ← get
-    let stateId := state.nextId
-    set { state with
-      goalStates := state.goalStates.insert stateId goalState,
-      nextId := state.nextId + 1
-    }
-    return stateId
   -- Command Functions
   reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
     let state ← get
@@ -90,10 +94,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     Environment.addDecl args
   env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
     let env ← Lean.MonadEnv.getEnv
-    env_pickle env args.path
+    environmentPickle env args.path
     return .ok {}
   env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
-    let (env, _) ← env_unpickle args.path
+    let (env, _) ← environmentUnpickle args.path
     Lean.setEnv env
     return .ok {}
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
@@ -203,11 +207,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     match nextState? with
     | .error error => return .error <| errorI "structure" error
     | .ok nextGoalState =>
-      let nextStateId := state.nextId
+      let nextStateId ← newGoalState nextGoalState
-      set { state with
-        goalStates := state.goalStates.insert nextStateId nextGoalState,
-        nextId := state.nextId + 1
-      }
       let goals ← goalSerialize nextGoalState (options := state.options)
       return .ok {
         nextStateId,
@@ -224,6 +224,16 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       return .error $ errorIndex s!"Invalid state index {args.stateId}"
     let result ← runMetaInMainM <| goalPrint goalState state.options
     return .ok result
+  goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
+    let state ← get
+    let .some goalState := state.goalStates[args.id]? |
+      return .error $ errorIndex s!"Invalid state index {args.id}"
+    goalStatePickle goalState args.path
+    return .ok {}
+  goal_load (args: Protocol.GoalLoad): MainM (CR Protocol.GoalLoadResult) := do
+    let (goalState, _) ← goalStateUnpickle args.path (← Lean.MonadEnv.getEnv)
+    let id ← newGoalState goalState
+    return .ok { id }
   frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
     let options := (← get).options
     try

Test/Common.lean

@@ -95,19 +95,19 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq)
 
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 
-def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do
+def strToTermSyntax (s: String): CoreM Syntax := do
   let .ok stx := Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := s)
-    (fileName := filename) | panic! s!"Failed to parse {s}"
+    (fileName := ← getFileName) | panic! s!"Failed to parse {s}"
   return stx
 def parseSentence (s: String): Elab.TermElabM Expr := do
   let stx ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := s)
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
   Elab.Term.elabTerm (stx := stx) .none
@@ -123,13 +123,28 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
 
 -- Monadic testing
 
-abbrev TestT := StateT LSpec.TestSeq
+abbrev TestT := StateRefT' IO.RealWorld LSpec.TestSeq
 
-def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do
+section Monadic
+
+variable [Monad m] [MonadLiftT (ST IO.RealWorld) m]
+
+def addTest (test: LSpec.TestSeq) : TestT m Unit := do
   set $ (← get) ++ test
 
-def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq :=
+def checkEq [DecidableEq α] [Repr α] (desc : String) (lhs rhs : α) : TestT m Unit := do
+  addTest $ LSpec.check desc (lhs = rhs)
+def checkTrue (desc : String) (flag : Bool) : TestT m Unit := do
+  addTest $ LSpec.check desc flag
+def fail (desc : String) : TestT m Unit := do
+  addTest $ LSpec.check desc false
+
+def runTest (t: TestT m Unit): m LSpec.TestSeq :=
   Prod.snd <$> t.run LSpec.TestSeq.done
+def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) :=
+  t.run LSpec.TestSeq.done
+
+end Monadic
 
 def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
   IO LSpec.TestSeq :=

Test/Delate.lean

@@ -32,7 +32,7 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
 def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × String) := [
     -- This one contains unhygienic variable names which must be suppressed
-    ("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"),
+    ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"),
     -- These ones are normal and easy
     ("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"),
     ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"),

Test/Library.lean

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

Test/Main.lean

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

Test/Metavar.lean

@@ -8,10 +8,7 @@ namespace Pantograph.Test.Metavar
 open Pantograph
 open Lean
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
+abbrev TestM := TestT $ 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
@@ -32,8 +29,6 @@ def test_instantiate_mvar: TestM Unit := do
     "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
   return ()
 
-
-
 def startProof (expr: String): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
   let syn? := parseTerm env expr

Test/Proofs.lean

@@ -14,10 +14,7 @@ inductive Start where
   | copy (name: String) -- Start from some name in the environment
   | expr (expr: String) -- Start from some expression
 
-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
+abbrev TestM := TestT $ 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
@@ -282,9 +279,9 @@ def test_or_comm: TestM Unit := 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 motive := s!"(:lambda t {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 caseL := s!"(:lambda h (:fv {fvP}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))"
-  let caseR := s!"(:lambda h._@._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 caseR := s!"(:lambda h (:fv {fvQ}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))"
   let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))"
   addTest $ LSpec.test "(2 parent)" (state2parent ==
     s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
@@ -704,6 +701,25 @@ def test_nat_zero_add_alt: TestM Unit := do
       }
     ])
 
+def test_composite_tactic_failure: TestM Unit := do
+  let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro p"
+  let state1 ← match ← state0.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  let tactic := "exact ⟨0, by simp⟩"
+  let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
+  checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"]
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("identity", test_identity),
@@ -716,6 +732,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("calc", test_calc),
     ("Nat.zero_add", test_nat_zero_add),
     ("Nat.zero_add alt", test_nat_zero_add_alt),
+    ("composite tactic failure", test_composite_tactic_failure),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))
 

Test/Serial.lean

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

Test/Tactic/MotivatedApply.lean

@@ -28,7 +28,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "@Nat.brecOn")
-      (fileName := filename) with
+      (fileName := ← getFileName) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -52,7 +52,7 @@ def test_list_brec_on : TestT Elab.TermElabM Unit := do
       (env := ← MonadEnv.getEnv)
       (catName := `term)
       (input := "@List.brecOn")
-      (fileName := filename) with
+      (fileName := ← getFileName) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
@@ -74,7 +74,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
     (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := "@Nat.brecOn")
-    (fileName := filename) with
+    (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
   let expr ← parseSentence expr

Test/Tactic/NoConfuse.lean

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

Test/Tactic/Prograde.lean

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

doc/icon.svg

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

doc/rationale.md

@@ -0,0 +1,30 @@
+# Design Rationale
+
+A great problem in machine learning is to use ML agents to automatically prove
+mathematical theorems. This sort of proof necessarily involves *search*.
+Compatibility for search is the main reason for creating Pantograph.  The Lean 4
+LSP interface is not conducive to search. Pantograph is designed with this in
+mind. It emphasizes the difference between 3 views of a proof:
+
+- **Presentation View**: The view of a written, polished proof. e.g. Mathlib and
+  math papers are almost always written in this form.
+- **Search View**: The view of a proof exploration trajectory. This is not
+  explicitly supported by Lean LSP.
+- **Kernel View**: The proof viewed as a set of metavariables.
+
+Pantograph enables proof agents to operate on the search view.
+
+## Name
+
+The name Pantograph is a pun. It means two things
+- A pantograph is an instrument for copying down writing. As an agent explores
+  the vast proof search space, Pantograph records the current state to ensure
+  the proof is sound.
+- A pantograph is also an equipment for an electric train. It supplies power to
+  a locomotive. In comparison the (relatively) simple Pantograph software powers
+  theorem proving projects.
+
+## References
+
+* [Pantograph Paper](https://arxiv.org/abs/2410.16429)
+

doc/repl.md

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