Rename tactic failure mode to avoid confusion
Clean up README
This commit is contained in:
parent
9b8aff95e5
commit
5beb911db5
21
Main.lean
21
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)
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
20
README.md
20
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"}
|
||||
|
|
Loading…
Reference in New Issue