Error category consolidation #7
|
@ -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
|
||||||
|
|
19
README.md
19
README.md
|
@ -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:
|
||||||
|
|
|
@ -5,10 +5,12 @@ import Pantograph
|
||||||
namespace Pantograph.Test
|
namespace Pantograph.Test
|
||||||
open Pantograph
|
open Pantograph
|
||||||
|
|
||||||
def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
|
def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
|
||||||
(expected: Lean.Json): MainM LSpec.TestSeq := do
|
(expected: Lean.Json): MainM LSpec.TestSeq := do
|
||||||
let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload }
|
let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload }
|
||||||
return LSpec.test s!"{cmd}" (toString result = toString expected)
|
return LSpec.test name (toString result = toString expected)
|
||||||
|
def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
|
||||||
|
(expected: Lean.Json): MainM LSpec.TestSeq := subroutine_named_step cmd cmd payload expected
|
||||||
|
|
||||||
def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
|
def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
|
||||||
-- Setup the environment for execution
|
-- Setup the environment for execution
|
||||||
|
@ -69,10 +71,15 @@ def test_option_modify : IO LSpec.TestSeq :=
|
||||||
def test_malformed_command : IO LSpec.TestSeq :=
|
def test_malformed_command : IO LSpec.TestSeq :=
|
||||||
let invalid := "invalid"
|
let invalid := "invalid"
|
||||||
subroutine_runner [
|
subroutine_runner [
|
||||||
subroutine_step invalid
|
subroutine_named_step "Invalid command" invalid
|
||||||
[("name", .str "Nat.add_one")]
|
[("name", .str "Nat.add_one")]
|
||||||
(Lean.toJson ({
|
(Lean.toJson ({
|
||||||
error := "command", desc := s!"Unknown command {invalid}"}:
|
error := "command", desc := s!"Unknown command {invalid}"}:
|
||||||
|
Commands.InteractionError)),
|
||||||
|
subroutine_named_step "JSON Deserialization" "expr.echo"
|
||||||
|
[(invalid, .str "Random garbage data")]
|
||||||
|
(Lean.toJson ({
|
||||||
|
error := "command", desc := s!"Unable to parse json: Pantograph.Commands.ExprEcho.expr: String expected"}:
|
||||||
Commands.InteractionError))
|
Commands.InteractionError))
|
||||||
]
|
]
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue