From e8fdd906aaf807a3132bffea67cbe14bbf4e8e6c Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 11 Jul 2025 20:09:54 -0700
Subject: [PATCH 1/3] doc: Remove stale documentation

---
 README.md | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 963ef97..7e1e416 100644
--- a/README.md
+++ b/README.md
@@ -17,17 +17,21 @@ nix build .#{sharedLib,executable}
 ```
 to build either the shared library or executable.
 
-Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and
-run
+For non-Nix users, install `lake` and `lean` fixed to the version of the
+`lean-toolchain` file, and run
 
 ``` sh
 lake build
 ```
-This builds the executable in `.lake/build/bin/pantograph-repl`.
+This builds the executable in `.lake/build/bin/repl`.
 
 ### Executable Usage
 
-See [Executable Usage](./doc/repl.md)
+The default build target is a Read-Eval-Print-Loop (REPL). See [REPL
+Documentation](./doc/repl.md)
+
+Another executable is the `tomograph`, which processes a Lean file and displays
+syntax or elaboration level data.
 
 ### Library Usage
 
@@ -39,7 +43,7 @@ Inject any project path via the `pantograph_init_search` function.
 
 ## Development
 
-A Lean development shell is provided in the Nix flake.
+A Lean development shell is provided in the Nix flake. Nix usage is optional.
 
 ### Testing
 

From 40bf3b2100cffc6143044209cbd7e20e058265cd Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 11 Jul 2025 20:15:14 -0700
Subject: [PATCH 2/3] doc: Remove stale repl documentation

---
 doc/repl.md | 33 ++++++++++++++++++++++-----------
 1 file changed, 22 insertions(+), 11 deletions(-)

diff --git a/doc/repl.md b/doc/repl.md
index 7ee9750..62dbaf4 100644
--- a/doc/repl.md
+++ b/doc/repl.md
@@ -4,37 +4,48 @@ This documentation is about interacting with the REPL.
 
 ## Examples
 
+After building the `repl`, it will be available in `.lake/build/bin/repl`.
+Execute it by either directly referring to its name, or `lake exe repl`.
+
 ``` sh
-pantograph-repl MODULES|LEAN_OPTIONS
+repl MODULES|LEAN_OPTIONS
 ```
 
-The `pantograph-repl` executable must be run with a list of modules to import.
-It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
+The `repl` executable must be given with a list of modules to import. By default
+it will import nothing, not even `Init`. It can also accept lean options of the
+form `--key=value` e.g. `--pp.raw=true`.
 
 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
+result of a command execution. It accepts commands in one of two formats
+
 ```
 command { ... }
 { "cmd": command, "payload": ... }
 ```
-The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
-empty command aborts the REPL.
+
+The list of available commands can be found below. An empty command aborts the
+REPL.
 
 Example: (~5k symbols)
 ```
-$ pantograph Init
+$ repl Init
 env.catalog
 env.inspect {"name": "Nat.le_add_left"}
 ```
+
 Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
+
 ```
-$ pantograph Mathlib.Analysis.Seminorm
+$ repl Mathlib.Analysis.Seminorm
 env.catalog
 ```
-Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
+
+Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`)
+to prime the proof
+
 ```
-$ pantograph Init
+$ repl Init
 goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
 goal.tactic {"stateId": 0, "tactic": "intro n m"}
 goal.tactic {"stateId": 1, "tactic": "assumption"}
@@ -59,7 +70,7 @@ LIB="../lib"
 LIB_MATHLIB="$LIB/mathlib4/.lake"
 export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
 
-LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
+LEAN_PATH=$LEAN_PATH repl $@
 ```
 The `$LEAN_PATH` executable of any project can be extracted by
 ``` sh

From c013e6614474addffbcc2b4705ef03d9509123e6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 11 Jul 2025 20:17:27 -0700
Subject: [PATCH 3/3] doc: Wording

---
 doc/repl.md | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/doc/repl.md b/doc/repl.md
index 62dbaf4..9c1f3ba 100644
--- a/doc/repl.md
+++ b/doc/repl.md
@@ -15,9 +15,10 @@ The `repl` executable must be given with a list of modules to import. By default
 it will import nothing, not even `Init`. It can also accept lean options of the
 form `--key=value` e.g. `--pp.raw=true`.
 
-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. It accepts commands in one of two formats
+After it emits the `ready.` signal, `repl` 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 must be
+given in one of two formats
 
 ```
 command { ... }