From 80ad7a2bd0647916d6f725f993ae1c2a1ea62e63 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 27 Aug 2023 19:58:52 -0700 Subject: [PATCH] Rename proof commands to goal commands --- Pantograph.lean | 35 ++++++++++++++++++----------------- Pantograph/Commands.lean | 13 +++++-------- README.md | 20 ++++++++++---------- 3 files changed, 33 insertions(+), 35 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 543c49e..bb2635e 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -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 diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 8c8b509..f9abf9d 100644 --- a/Pantograph/Commands.lean +++ b/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 diff --git a/README.md b/README.md index 8407d49..9a2ec5b 100644 --- a/README.md +++ b/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": ], ["expr": ], ["copyFrom": ]}`: Start a new proof state from a given expression or symbol -- `proof.tactic {"goalId": , "tactic": }`: Execute a tactic string on a given proof state -- `proof.printTree`: Print the number of goals +- `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new goal from a given expression or symbol +- `goal.tactic {"goalId": , "tactic": }`: Execute a tactic string on a given goal +- `stat`: Display resource usage ## Errors