From 95d26a2f50c2f397bbc91e16c768ae02b3418b5b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 24 Aug 2023 22:51:40 -0700 Subject: [PATCH 1/2] Classify JSON error as command error Also add documentation for this --- Pantograph.lean | 5 +++-- README.md | 19 +++++++++++++++++-- 2 files changed, 20 insertions(+), 4 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 8a8e91a..18ead6b 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -27,7 +27,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do match (← comm args) with | .ok result => return Lean.toJson result | .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 | "reset" => run reset | "expr.echo" => run expr_echo @@ -40,10 +40,11 @@ def execute (command: Commands.Command): MainM Lean.Json := do | "proof.printTree" => run proof_print_tree | cmd => let error: Commands.InteractionError := - { error := "command", desc := s!"Unknown command {cmd}" } + errorCommand s!"Unknown command {cmd}" return Lean.toJson error where errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc } + errorCommand := errorI "command" errorIndex := errorI "index" -- Command Functions reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do diff --git a/README.md b/README.md index f413d31..82d3db3 100644 --- a/README.md +++ b/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 -`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 ``` command { ... } @@ -64,7 +64,7 @@ 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/Commands.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 @@ -78,6 +78,21 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va - `proof.tactic {"treeId": , "stateId": , "goalId": , "tactic": string}`: Execute a tactic on a given proof state - `proof.printTree {"treeId": }`: 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 If lean encounters stack overflow problems when printing catalog, execute this before running lean: -- 2.44.1 From 51edc701fe18806cdc3f4860d9ef442a1c9abcf4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 24 Aug 2023 23:12:18 -0700 Subject: [PATCH 2/2] Add test cases for command error categories --- Test/Integration.lean | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/Test/Integration.lean b/Test/Integration.lean index 83cdb70..ab31110 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -5,10 +5,12 @@ import Pantograph namespace Pantograph.Test 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 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 -- Setup the environment for execution @@ -69,10 +71,15 @@ def test_option_modify : IO LSpec.TestSeq := def test_malformed_command : IO LSpec.TestSeq := let invalid := "invalid" subroutine_runner [ - subroutine_step invalid + subroutine_named_step "Invalid command" invalid [("name", .str "Nat.add_one")] (Lean.toJson ({ 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)) ] -- 2.44.1