From a7aeb03b43cad5b4c30610c83ad510cca59f383f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 6 Nov 2023 11:04:28 -0800 Subject: [PATCH] chore: Update documentation --- README.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 0c19a3a..2b8425c 100644 --- a/README.md +++ b/README.md @@ -33,7 +33,7 @@ result of a command execution. The command can be passed in one of two formats command { ... } { "cmd": command, "payload": ... } ``` -The list of available commands can be found in `Pantograph/Commands.lean` and below. An +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 @@ -54,18 +54,18 @@ Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_ ``` $ pantograph Init goal.start {"expr": "∀ (n m : Nat), n + m = m + n"} -goal.tactic {"goalId": 0, "tactic": "intro n m"} -goal.tactic {"goalId": 1, "tactic": "assumption"} -goal.delete {"goalIds": [0]} +goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"} +goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"} +goal.delete {"stateIds": [0]} stat {} -goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"} +goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"} stat ``` where the application of `assumption` should lead to a failure. ## Commands -See `Pantograph/Commands.lean` for a description of the parameters and return values in JSON. +See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. - `reset`: Delete all cached expressions and proof trees - `expr.echo {"expr": }`: Determine the type of an expression and round-trip it - `lib.catalog`: Display a list of all safe Lean symbols in the current context @@ -73,10 +73,11 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va 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/Commands.lean` + have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` - `options.print`: Display the current set of options - `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new goal from a given expression or symbol - `goal.tactic {"stateId": , "goalId": , ["tactic": ], ["expr": ]}`: Execute a tactic string on a given goal +- `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: Continue from a proof state - `goal.remove {"stateIds": []}"`: Remove a bunch of stored goals. - `goal.print {"stateId": }"`: Print a goal state - `stat`: Display resource usage