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
+  | "env.catalog"   => run env_catalog
-  | "lib.inspect"   => run lib_inspect
+  | "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

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

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
+env.catalog
-lib.inspect {"name": "Nat.le_add_left"}
+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": <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
+- `env.catalog`: Display a list of all safe Lean symbols in the current environment
-- `lib.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
+- `env.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.
 - `options.set { key: value, ... }`: Set one or more options (not Lean options; those

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),
+    ("Lean.Name".toName, true)
-    ("_private.Init.0.Lean.Name".toName, true)
   ]
   let suite := entries.foldl (λ suites (symbol, target) =>
     let constant := env.constants.find! symbol

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 }: