From 5beb911db5490dd669162392f3c363eaa20a979e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 24 May 2023 22:33:10 -0700 Subject: [PATCH] Rename tactic failure mode to avoid confusion Clean up README --- Main.lean | 21 +++++++++++---------- Pantograph/Commands.lean | 10 +++++++--- README.md | 20 +++++++++++--------- 3 files changed, 29 insertions(+), 22 deletions(-) diff --git a/Main.lean b/Main.lean index 7db7233..1430ec6 100644 --- a/Main.lean +++ b/Main.lean @@ -62,8 +62,9 @@ def execute (command: Command): Subroutine Lean.Json := do let error: InteractionError := { error := "unknown", desc := s!"Unknown command {cmd}" } return Lean.toJson error where - errorJson (s: String) := Lean.toJson ({ error := "json", desc := s }: InteractionError) - errorIndex (s: String) := Lean.toJson ({ error := "index", desc := s }: InteractionError) + errorI (type desc: String) := Lean.toJson ({ error := type, desc := desc }: InteractionError) + errorJson := errorI "json" + errorIndex := errorI "index" catalog (_: Catalog): Subroutine Lean.Json := do let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := []) (λ es name info => @@ -76,7 +77,7 @@ def execute (command: Command): Subroutine Lean.Json := do let name := str_to_name args.name let info? := env.find? name match info? with - | none => return Lean.toJson <| errorIndex s!"Symbol not found {args.name}" + | none => return errorIndex s!"Symbol not found {args.name}" | some info => let format ← Lean.Meta.ppExpr info.toConstantVal.type let module? := env.getModuleIdxFor? name >>= @@ -95,18 +96,18 @@ def execute (command: Command): Subroutine Lean.Json := do let expr?: Except Lean.Json Lean.Expr ← (match args.expr, args.copyFrom with | .some expr, .none => (match syntax_from_str env expr with - | .error str => return .error <| Lean.toJson ({ error := "parsing", desc := str }: InteractionError) + | .error str => return .error <| errorI "parsing" str | .ok syn => do (match (← syntax_to_expr syn) with - | .error str => return .error <| Lean.toJson ({ error := "elab", desc := str }: InteractionError) + | .error str => return .error <| errorI "elab" str | .ok expr => return .ok expr)) | .none, .some copyFrom => (match env.find? <| str_to_name copyFrom with | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" | .some cInfo => return .ok cInfo.type) | .none, .none => - return .error <| Lean.toJson ({ error := "arguments", desc := "At least one of {expr, copyFrom} must be supplied" }: InteractionError) - | _, _ => return .error <| Lean.toJson ({ error := "arguments", desc := "Cannot populate both of {expr, copyFrom}" }: InteractionError)) + return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied" + | _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}") match expr? with | .error error => return error | .ok expr => @@ -118,7 +119,7 @@ def execute (command: Command): Subroutine Lean.Json := do proof_tactic (args: ProofTactic): Subroutine Lean.Json := do let state ← get match state.proofTrees.get? args.treeId with - | .none => return Lean.toJson <| errorIndex "Invalid tree index {args.treeId}" + | .none => return errorIndex "Invalid tree index {args.treeId}" | .some tree => let (result, nextTree) ← ProofTree.execute (stateId := args.stateId) @@ -130,11 +131,11 @@ def execute (command: Command): Subroutine Lean.Json := do set { state with proofTrees := state.proofTrees.set! args.treeId nextTree } return Lean.toJson ({ nextId? := nextId?, goals := goals }: ProofTacticResultSuccess) | .failure messages => - return Lean.toJson ({ errorMessages := messages }: ProofTacticResultFailure) + return Lean.toJson ({ tacticErrors := messages }: ProofTacticResultFailure) proof_print_tree (args: ProofPrintTree): Subroutine Lean.Json := do let state ← get match state.proofTrees.get? args.treeId with - | .none => return Lean.toJson <| errorIndex "Invalid tree index {args.treeId}" + | .none => return errorIndex "Invalid tree index {args.treeId}" | .some tree => return Lean.toJson ({parents := tree.structure_array}: ProofPrintTreeResult) diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 51d08fd..751510a 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -1,4 +1,9 @@ --- All the command input/output structures are stored here +/- +All the command input/output structures are stored here + +Note that no command other than `InteractionError` may have `error` as one of +its field names to avoid confusion with error messages generated by the REPL. +-/ import Lean.Data.Json import Pantograph.Serial @@ -44,7 +49,6 @@ structure ProofStart where copyFrom: Option String -- Theorem name deriving Lean.FromJson structure ProofStartResult where - error: String := "" treeId: Nat := 0 -- Proof tree id deriving Lean.ToJson @@ -60,7 +64,7 @@ structure ProofTacticResultSuccess where nextId?: Option Nat -- Next proof state id deriving Lean.ToJson structure ProofTacticResultFailure where - errorMessages: Array String -- Error messages generated by tactic + tacticErrors: Array String -- Error messages generated by tactic deriving Lean.ToJson structure ProofPrintTree where diff --git a/README.md b/README.md index f87d6f8..ff4b8e1 100644 --- a/README.md +++ b/README.md @@ -9,21 +9,23 @@ Install `elan` and `lean4`. Then, execute lake build ``` In order to use `mathlib`, its binary must also be built - ``` sh lake build Qq lake build aesop lake build std lake build mathlib ``` +In a future version, the dependencies of mathlib will be removed and the user will be responsible for adding such library paths to `LEAN_PATH`. ## Usage -The binary must be run inside a `lake env` environment. i.e. `lake env -build/bin/pantograph OPTIONS|MODULES`. 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 result of a command execution. -The command can be passed in one of two formats +``` sh +build/bin/pantograph OPTIONS|MODULES +``` + +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 +result of a command execution. The command can be passed in one of two formats ``` command { ... } { "cmd": command, "payload": ... } @@ -36,18 +38,18 @@ also accept options of the form `--key=value` e.g. `--pp.raw=true`. Example: (~5k symbols) ``` -$ lake env build/bin/Pantograph "Init" +$ build/bin/Pantograph Init catalog inspect {"name": "Nat.le_add_left"} ``` Example with `mathlib` (~90k symbols) ``` -$ lake env build/bin/Pantograph "Mathlib.Analysis.Seminorm" +$ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm catalog ``` Example proving a theorem: (alternatively use `proof.start {"copyFrom": "Nat.add_comm"}`) to prime the proof ``` -$ lake env build/bin/Pantograph "Init" +$ env build/bin/Pantograph Init proof.start {"expr": "∀ (n m : Nat), n + m = m + n"} proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro n m"} proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"}