Pantograph.lean

@@ -134,7 +134,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
     match expr? with
     | .error error => return .error error
     | .ok expr =>
-      let tree ← ProofTree.create expr
+      let tree ← ProofTree.create (str_to_name <| args.name.getD "Untitled") expr
       -- Put the new tree in the environment
       let nextTreeId := state.proofTrees.size
       set { state with proofTrees := state.proofTrees.push tree }

Pantograph/Commands.lean

@@ -128,6 +128,7 @@ structure OptionsPrint where
 abbrev OptionsPrintResult := Options
 
 structure ProofStart where
+  name: Option String     -- Identifier of the proof
   -- Only one of the fields below may be populated.
   expr: Option String     -- Proof expression
   copyFrom: Option String -- Theorem name
@@ -139,7 +140,7 @@ structure ProofTactic where
   -- Identifiers for tree, state, and goal
   treeId: Nat
   stateId: Nat
-  goalId: Option Nat -- Defaults to 0
+  goalId: Option Nat
   tactic: String
   deriving Lean.FromJson
 structure ProofTacticResult where

Pantograph/Tactic.lean

@@ -30,17 +30,21 @@ structure ProofState where
   parent : Option Nat := none
   parentGoalId : Nat  := 0
 structure ProofTree where
+  -- All parameters needed to run a `TermElabM` monad
+  name: Name
+
   -- Set of proof states
   states : Array ProofState := #[]
 
 abbrev M := Elab.TermElabM
 
-def ProofTree.create (expr: Expr): M ProofTree := do
+def ProofTree.create (name: Name) (expr: Expr): M ProofTree := do
   let expr ← instantiateMVars expr
   let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic))
   let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
   let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
   return {
+    name := name,
     states := #[{
       savedState := savedState,
       goals := [goal.mvarId!]

Test/Proofs.lean

@@ -22,6 +22,7 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
     match cInfo? with
     | .some cInfo =>
       let state ← ProofTree.create
+        (name := str_to_name "TestExample")
         (expr := cInfo.type)
       return (testSeq, Option.some state)
     | .none =>
@@ -42,6 +43,7 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
         return (testSeq, Option.none)
       | .ok expr =>
         let state ← ProofTree.create
+          (name := str_to_name "TestExample")
           (expr := expr)
         return (testSeq, Option.some state)