Classify JSON error as command error

Also add documentation for this
This commit is contained in:
Leni Aniva 2023-08-24 22:51:40 -07:00
parent 5978e5f4f3
commit 95d26a2f50
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 20 additions and 4 deletions

View File

@ -27,7 +27,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
match (← comm args) with match (← comm args) with
| .ok result => return Lean.toJson result | .ok result => return Lean.toJson result
| .error ierror => return Lean.toJson ierror | .error ierror => return Lean.toJson ierror
| .error error => pure $ error | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
match command.cmd with match command.cmd with
| "reset" => run reset | "reset" => run reset
| "expr.echo" => run expr_echo | "expr.echo" => run expr_echo
@ -40,10 +40,11 @@ def execute (command: Commands.Command): MainM Lean.Json := do
| "proof.printTree" => run proof_print_tree | "proof.printTree" => run proof_print_tree
| cmd => | cmd =>
let error: Commands.InteractionError := let error: Commands.InteractionError :=
{ error := "command", desc := s!"Unknown command {cmd}" } errorCommand s!"Unknown command {cmd}"
return Lean.toJson error return Lean.toJson error
where where
errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc } errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
errorCommand := errorI "command"
errorIndex := errorI "index" errorIndex := errorI "index"
-- Command Functions -- Command Functions
reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do

View File

@ -27,7 +27,7 @@ build/bin/pantograph MODULES|LEAN_OPTIONS
``` ```
The REPL loop accepts commands as single-line JSON inputs and outputs either an The REPL loop accepts commands as single-line JSON inputs and outputs either an
`Error:` (indicating malformed command) or a json return value indicating the `Error:` (indicating malformed command) or a JSON return value indicating the
result of a command execution. The command can be passed in one of two formats result of a command execution. The command can be passed in one of two formats
``` ```
command { ... } command { ... }
@ -64,7 +64,7 @@ where the application of `assumption` should lead to a failure.
## Commands ## Commands
See `Pantograph/Commands.lean` for a description of the parameters and return values in Json. See `Pantograph/Commands.lean` for a description of the parameters and return values in JSON.
- `reset`: Delete all cached expressions and proof trees - `reset`: Delete all cached expressions and proof trees
- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it - `expr.echo {"expr": <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 - `lib.catalog`: Display a list of all safe Lean symbols in the current context
@ -78,6 +78,21 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va
- `proof.tactic {"treeId": <id>, "stateId": <id>, "goalId": <id>, "tactic": string}`: Execute a tactic on a given proof state - `proof.tactic {"treeId": <id>, "stateId": <id>, "goalId": <id>, "tactic": string}`: Execute a tactic on a given proof state
- `proof.printTree {"treeId": <id>}`: Print the topological structure of a proof tree - `proof.printTree {"treeId": <id>}`: Print the topological structure of a proof tree
## Errors
When an error pertaining to the execution of a command happens, the returning JSON structure is
``` json
{ error: "type", desc: "description" }
```
Common error forms:
* `command`: Indicates malformed command structure which results from either
invalid command or a malformed JSON structure that cannot be fed to an
individual command.
* `index`: Indicates an invariant maintained by the output of one command and
input of another is broken. For example, attempting to query a symbol not
existing in the library or indexing into a non-existent proof state.
## Troubleshooting ## Troubleshooting
If lean encounters stack overflow problems when printing catalog, execute this before running lean: If lean encounters stack overflow problems when printing catalog, execute this before running lean: