Add compressed json print option; Rearrange commands into hierarchy

This commit is contained in:
Leni Aniva 2023-08-16 19:25:32 -07:00
parent 0e61093f47
commit ddf7ec21c8
6 changed files with 88 additions and 82 deletions

View File

@ -8,15 +8,20 @@ import Pantograph
open Pantograph
unsafe def loop : MainM Unit := do
let state ← get
let command ← (← IO.getStdin).getLine
if command.trim.length = 0 then return ()
match parse_command command with
| .error error =>
let error := Lean.toJson ({ error := "json", desc := error }: Commands.InteractionError)
IO.println (toString error)
-- Using `Lean.Json.compress` here to prevent newline
IO.println error.compress
| .ok command =>
let ret ← execute command
IO.println <| toString <| ret
let str := match state.options.printJsonPretty with
| true => ret.pretty
| false => ret.compress
IO.println str
loop
namespace Lean

View File

@ -44,12 +44,12 @@ def execute (command: Commands.Command): MainM Lean.Json := do
| .error ierror => return Lean.toJson ierror
| .error error => pure $ error
match command.cmd with
| "reset" => run reset
| "expr.echo" => run expr_echo
| "lib.catalog" => run lib_catalog
| "lib.inspect" => run lib_inspect
| "options.set" => run options_set
| "options.print" => run options_print
| "catalog" => run catalog
| "inspect" => run inspect
| "clear" => run clear
| "expr.echo" => run expr_echo
| "proof.start" => run proof_start
| "proof.tactic" => run proof_tactic
| "proof.printTree" => run proof_print_tree
@ -61,30 +61,19 @@ def execute (command: Commands.Command): MainM Lean.Json := do
errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
errorIndex := errorI "index"
-- Command Functions
options_set (args: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do
reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do
let state ← get
let options := state.options
set { state with
options := {
-- FIXME: This should be replaced with something more elegant
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
printExprAST := args.printExprAST?.getD options.printExprAST,
proofVariableDelta := args.proofVariableDelta?.getD options.proofVariableDelta,
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
}
}
return .ok { }
options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
return .ok (← get).options
catalog (_: Commands.Catalog): MainM (CR Commands.CatalogResult) := do
let nTrees := state.proofTrees.size
set { state with proofTrees := #[] }
return .ok { nTrees := nTrees }
lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := do
let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info =>
match to_filtered_symbol name info with
| .some x => acc.push x
| .none => acc)
return .ok { symbols := names }
inspect (args: Commands.Inspect): MainM (CR Commands.InspectResult) := do
lib_inspect (args: Commands.LibInspect): MainM (CR Commands.LibInspectResult) := do
let state ← get
let env ← Lean.MonadEnv.getEnv
let name := str_to_name args.name
@ -104,11 +93,6 @@ def execute (command: Commands.Command): MainM Lean.Json := do
value? := ← value?.mapM (λ v => serialize_expression state.options v),
module? := module?
}
clear (_: Commands.Clear): MainM (CR Commands.ClearResult) := do
let state ← get
let nTrees := state.proofTrees.size
set { state with proofTrees := #[] }
return .ok { nTrees := nTrees }
expr_echo (args: Commands.ExprEcho): MainM (CR Commands.ExprEchoResult) := do
let state ← get
let env ← Lean.MonadEnv.getEnv
@ -126,6 +110,23 @@ def execute (command: Commands.Command): MainM Lean.Json := do
}
catch exception =>
return .error $ errorI "typing" (← exception.toMessageData.toString)
options_set (args: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do
let state ← get
let options := state.options
set { state with
options := {
-- FIXME: This should be replaced with something more elegant
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
printExprAST := args.printExprAST?.getD options.printExprAST,
proofVariableDelta := args.proofVariableDelta?.getD options.proofVariableDelta,
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
}
}
return .ok { }
options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
return .ok (← get).options
proof_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do
let state ← get
let env ← Lean.MonadEnv.getEnv

View File

@ -11,6 +11,9 @@ namespace Pantograph.Commands
/-- Main Option structure, placed here to avoid name collision -/
structure Options where
-- When false, suppress newlines in Json objects. Useful for machine-to-machine interaction.
-- This should be false` by default to avoid any surprises with parsing.
printJsonPretty: Bool := false
-- When enabled, pretty print every expression
printExprPretty: Bool := true
-- When enabled, print the raw AST of expressions
@ -74,45 +77,10 @@ structure InteractionError where
--- Individual command and return types ---
/-- Set options; See `Options` struct above for meanings -/
structure OptionsSet where
printExprPretty?: Option Bool
printExprAST?: Option Bool
proofVariableDelta?: Option Bool
printAuxDecls?: Option Bool
printImplementationDetailHyps?: Option Bool
deriving Lean.FromJson
structure OptionsSetResult where
deriving Lean.ToJson
structure OptionsPrint where
structure Reset where
deriving Lean.FromJson
abbrev OptionsPrintResult := Options
-- Print all symbols in environment
structure Catalog where
deriving Lean.FromJson
structure CatalogResult where
symbols: Array String
deriving Lean.ToJson
-- Print the type of a symbol
structure Inspect where
name: String
-- If true/false, show/hide the value expressions; By default definitions
-- values are shown and theorem values are hidden.
value?: Option Bool := .some false
deriving Lean.FromJson
structure InspectResult where
type: Expression
value?: Option Expression := .none
module?: Option String
deriving Lean.ToJson
structure Clear where
deriving Lean.FromJson
structure ClearResult where
structure ResetResult where
nTrees: Nat
deriving Lean.ToJson
@ -125,6 +93,40 @@ structure ExprEchoResult where
type: Expression
deriving Lean.ToJson
-- Print all symbols in environment
structure LibCatalog where
deriving Lean.FromJson
structure LibCatalogResult where
symbols: Array String
deriving Lean.ToJson
-- Print the type of a symbol
structure LibInspect where
name: String
-- If true/false, show/hide the value expressions; By default definitions
-- values are shown and theorem values are hidden.
value?: Option Bool := .some false
deriving Lean.FromJson
structure LibInspectResult where
type: Expression
value?: Option Expression := .none
module?: Option String
deriving Lean.ToJson
/-- Set options; See `Options` struct above for meanings -/
structure OptionsSet where
printJsonPretty?: Option Bool
printExprPretty?: Option Bool
printExprAST?: Option Bool
proofVariableDelta?: Option Bool
printAuxDecls?: Option Bool
printImplementationDetailHyps?: Option Bool
deriving Lean.FromJson
structure OptionsSetResult where
deriving Lean.ToJson
structure OptionsPrint where
deriving Lean.FromJson
abbrev OptionsPrintResult := Options
structure ProofStart where
name: Option String -- Identifier of the proof
-- Only one of the fields below may be populated.
@ -134,7 +136,6 @@ structure ProofStart where
structure ProofStartResult where
treeId: Nat := 0 -- Proof tree id
deriving Lean.ToJson
structure ProofTactic where
-- Identifiers for tree, state, and goal
treeId: Nat
@ -150,7 +151,6 @@ structure ProofTacticResult where
-- Existence of this field shows failure
tacticErrors?: Option (Array String) := .none
deriving Lean.ToJson
structure ProofPrintTree where
treeId: Nat
deriving Lean.FromJson

View File

@ -1,5 +1,5 @@
namespace Pantograph
def version := "0.2.1"
def version := "0.2.2"
end Pantograph

View File

@ -42,13 +42,13 @@ also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
Example: (~5k symbols)
```
$ build/bin/Pantograph Init
catalog
inspect {"name": "Nat.le_add_left"}
lib.catalog
lib.inspect {"name": "Nat.le_add_left"}
```
Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
```
$ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm
catalog
lib.catalog
```
Example proving a theorem: (alternatively use `proof.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
```
@ -65,15 +65,15 @@ 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.
- `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.)
- `options.print`: Display the current set of options
- `catalog`: Display a list of all safe Lean symbols in the current context
- `inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
- `reset`: Delete all cached expressions and proof trees
- `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.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
given symbol; If value flag is set, the value is printed or hidden. By default
only the values of definitions are printed.
- `clear`: Delete all cached expressions and proof trees
- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
- `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.), for options, see `Pantograph/Commands.lean`
- `options.print`: Display the current set of options
- `proof.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new proof state from a given expression or symbol
- `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

View File

@ -47,20 +47,20 @@ def test_option_print : IO LSpec.TestSeq :=
let module? := Option.some "Init.Data.Nat.Basic"
let options: Commands.Options := {}
subroutine_runner [
subroutine_step "inspect"
subroutine_step "lib.inspect"
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp? }, module? }:
Commands.InspectResult)),
Commands.LibInspectResult)),
subroutine_step "options.set"
[("printExprAST", .bool true)]
(Lean.toJson ({ }:
Commands.OptionsSetResult)),
subroutine_step "inspect"
subroutine_step "lib.inspect"
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp?, sexp? }, module? }:
Commands.InspectResult)),
Commands.LibInspectResult)),
subroutine_step "options.print"
[]
(Lean.toJson ({ options with printExprAST := true }: