diff --git a/Main.lean b/Main.lean index 70f2494..10fc6b0 100644 --- a/Main.lean +++ b/Main.lean @@ -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 diff --git a/Pantograph.lean b/Pantograph.lean index e40a3e7..e3501aa 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -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 diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 57c5ddc..8d17b0e 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -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 diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index a9c55b5..9cf39ff 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,5 +1,5 @@ namespace Pantograph -def version := "0.2.1" +def version := "0.2.2" end Pantograph diff --git a/README.md b/README.md index 309303b..f413d31 100644 --- a/README.md +++ b/README.md @@ -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": , "value": }`: Show the type and package of a +- `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 +- `lib.inspect {"name": , "value": }`: 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": }`: 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": ], ["expr": ], ["copyFrom": ]}`: Start a new proof state from a given expression or symbol - `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 diff --git a/Test/Integration.lean b/Test/Integration.lean index cfcf557..ae73d82 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -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 }: