Pantograph.lean

@@ -30,14 +30,14 @@ def execute (command: Commands.Command): MainM Lean.Json := do
     | .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
-  | "proof.start"     => run proof_start
-  | "proof.tactic"    => run proof_tactic
-  | "proof.printTree" => run proof_print_tree
+  | "goal.start"     => run goal_start
+  | "goal.tactic"    => run goal_tactic
   | cmd =>
     let error: Commands.InteractionError :=
       errorCommand s!"Unknown command {cmd}"
@@ -47,11 +47,15 @@ def execute (command: Commands.Command): MainM Lean.Json := do
   errorCommand := errorI "command"
   errorIndex := errorI "index"
   -- Command Functions
-  reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do
+  reset (_: Commands.Reset): MainM (CR Commands.StatResult) := do
     let state ← get
-    let nStates := state.goalStates.size
+    let nGoals := state.goalStates.size
     set { state with goalStates := SemihashMap.empty }
-    return .ok { nStates := nStates }
+    return .ok { nGoals }
+  stat (_: Commands.Stat): MainM (CR Commands.StatResult) := do
+    let state ← get
+    let nGoals := state.goalStates.size
+    return .ok { nGoals }
   lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := do
     let env ← Lean.MonadEnv.getEnv
     let names := env.constants.fold (init := #[]) (λ acc name info =>
@@ -113,7 +117,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
     return .ok {  }
   options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
     return .ok (← get).options
-  proof_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do
+  goal_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with
@@ -138,7 +142,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
       let (goalStates, goalId) := state.goalStates.insert goalState
       set { state with goalStates }
       return .ok { goalId }
-  proof_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do
+  goal_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do
     let state ← get
     match state.goalStates.get? args.goalId with
     | .none => return .error $ errorIndex "Invalid goal index {args.goalId}"
@@ -160,8 +164,5 @@ def execute (command: Commands.Command): MainM Lean.Json := do
           return .ok { goals? := .some sGoals.reverse.toArray, goalIds? := .some goalIds.reverse.toArray }
       | .failure messages =>
         return .ok { tacticErrors? := .some messages }
-  proof_print_tree (_: Commands.ProofPrintTree): MainM (CR Commands.ProofPrintTreeResult) := do
-    let state ← get
-    return .ok { nGoals := state.goalStates.size }
 
 end Pantograph

Pantograph/Commands.lean

@@ -80,8 +80,11 @@ structure InteractionError where
 
 structure Reset where
   deriving Lean.FromJson
-structure ResetResult where
-  nStates: Nat
+structure Stat where
+  deriving Lean.FromJson
+structure StatResult where
+  -- Number of goals states
+  nGoals: Nat
   deriving Lean.ToJson
 
 -- Return the type of an expression
@@ -149,11 +152,5 @@ structure ProofTacticResult where
   tacticErrors?: Option (Array String) := .none
   deriving Lean.ToJson
 
-structure ProofPrintTree where
-  deriving Lean.FromJson
-structure ProofPrintTreeResult where
-  -- Total number of goals
-  nGoals: Nat
-  deriving Lean.ToJson
 
 end Pantograph.Commands

README.md

@@ -50,15 +50,15 @@ Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
 $ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm
 lib.catalog
 ```
-Example proving a theorem: (alternatively use `proof.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
+Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
 ```
 $ env build/bin/Pantograph Init
-proof.start {"expr": "∀ (n m : Nat), n + m = m + n"}
-proof.tactic {"goalId": 0, "tactic": "intro n m"}
-proof.tactic {"goalId": 1, "tactic": "assumption"}
-proof.printTree {}
-proof.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"}
-proof.printTree
+goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
+goal.tactic {"goalId": 0, "tactic": "intro n m"}
+goal.tactic {"goalId": 1, "tactic": "assumption"}
+stat {}
+goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"}
+stat
 ```
 where the application of `assumption` should lead to a failure.
 
@@ -74,9 +74,9 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va
 - `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/Commands.lean`
 - `options.print`: Display the current set of options
-- `proof.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new proof state from a given expression or symbol
-- `proof.tactic {"goalId": <id>, "tactic": <tactic>}`: Execute a tactic string on a given proof state
-- `proof.printTree`: Print the number of goals
+- `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
+- `goal.tactic {"goalId": <id>, "tactic": <tactic>}`: Execute a tactic string on a given goal
+- `stat`: Display resource usage
 
 ## Errors