Rename proof commands to goal commands

This commit is contained in:
Leni Aniva 2023-08-27 19:58:52 -07:00
parent 0c5f439067
commit 80ad7a2bd0
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 33 additions and 35 deletions

View File

@ -29,15 +29,15 @@ def execute (command: Commands.Command): MainM Lean.Json := do
| .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
| "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
| "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
| 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

View File

@ -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

View File

@ -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