From 12544b81ee10c1fa59d2425c99590b839ba5c2ac Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 12 Dec 2023 18:56:25 -0800 Subject: [PATCH] chore: Rename lib. commands to env. This is done to improve clarity and align with Lean's terminology --- Pantograph.lean | 8 ++++---- Pantograph/Protocol.lean | 8 ++++---- README.md | 10 +++++----- Test/Catalog.lean | 3 +-- Test/Integration.lean | 8 ++++---- 5 files changed, 18 insertions(+), 19 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index a66db35..c376999 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -33,8 +33,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | "reset" => run reset | "stat" => run stat | "expr.echo" => run expr_echo - | "lib.catalog" => run lib_catalog - | "lib.inspect" => run lib_inspect + | "env.catalog" => run env_catalog + | "env.inspect" => run env_inspect | "options.set" => run options_set | "options.print" => run options_print | "goal.start" => run goal_start @@ -60,14 +60,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let nGoals := state.goalStates.size return .ok { nGoals } - lib_catalog (_: Protocol.LibCatalog): MainM (CR Protocol.LibCatalogResult) := do + env_catalog (_: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := 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 } - lib_inspect (args: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do + env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do let state ← get let env ← Lean.MonadEnv.getEnv let name := args.name.toName diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index a88a54a..b544881 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -102,13 +102,13 @@ structure ExprEchoResult where deriving Lean.ToJson -- Print all symbols in environment -structure LibCatalog where +structure EnvCatalog where deriving Lean.FromJson -structure LibCatalogResult where +structure EnvCatalogResult where symbols: Array String deriving Lean.ToJson -- Print the type of a symbol -structure LibInspect where +structure EnvInspect where name: String -- If true/false, show/hide the value expressions; By default definitions -- values are shown and theorem values are hidden. @@ -116,7 +116,7 @@ structure LibInspect where -- If true, show the type and value dependencies dependency?: Option Bool := .some false deriving Lean.FromJson -structure LibInspectResult where +structure EnvInspectResult where type: Expression value?: Option Expression := .none module?: Option String := .none diff --git a/README.md b/README.md index 2b8425c..1ca4d7b 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) ``` $ pantograph Init -lib.catalog -lib.inspect {"name": "Nat.le_add_left"} +env.catalog +env.inspect {"name": "Nat.le_add_left"} ``` Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) ``` $ pantograph Mathlib.Analysis.Seminorm -lib.catalog +env.catalog ``` Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof ``` @@ -68,8 +68,8 @@ where the application of `assumption` should lead to a failure. See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. - `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 +- `env.catalog`: Display a list of all safe Lean symbols in the current environment +- `env.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. - `options.set { key: value, ... }`: Set one or more options (not Lean options; those diff --git a/Test/Catalog.lean b/Test/Catalog.lean index e082369..99447e7 100644 --- a/Test/Catalog.lean +++ b/Test/Catalog.lean @@ -10,8 +10,7 @@ open Lean def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do let entries: List (Name × Bool) := [ ("Nat.add_comm".toName, false), - ("Lean.Name".toName, true), - ("_private.Init.0.Lean.Name".toName, true) + ("Lean.Name".toName, true) ] let suite := entries.foldl (λ suites (symbol, target) => let constant := env.constants.find! symbol diff --git a/Test/Integration.lean b/Test/Integration.lean index 65c2da6..44faf1b 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -49,20 +49,20 @@ def test_option_modify : IO LSpec.TestSeq := let module? := Option.some "Init.Data.Nat.Basic" let options: Protocol.Options := {} subroutine_runner [ - subroutine_step "lib.inspect" + subroutine_step "env.inspect" [("name", .str "Nat.add_one")] (Lean.toJson ({ type := { pp? }, module? }: - Protocol.LibInspectResult)), + Protocol.EnvInspectResult)), subroutine_step "options.set" [("printExprAST", .bool true)] (Lean.toJson ({ }: Protocol.OptionsSetResult)), - subroutine_step "lib.inspect" + subroutine_step "env.inspect" [("name", .str "Nat.add_one")] (Lean.toJson ({ type := { pp?, sexp? }, module? }: - Protocol.LibInspectResult)), + Protocol.EnvInspectResult)), subroutine_step "options.print" [] (Lean.toJson ({ options with printExprAST := true }: