Rename tactic failure mode to avoid confusion

Clean up README
This commit is contained in:
Leni Aniva 2023-05-24 22:33:10 -07:00
parent da1cdf3d16
commit e0c5f76451
3 changed files with 29 additions and 22 deletions

View File

@ -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)

View File

@ -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

View File

@ -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"}