diff --git a/README.md b/README.md
index 04213ae..bfd391b 100644
--- a/README.md
+++ b/README.md
@@ -7,6 +7,8 @@ A Machine-to-Machine interaction system for Lean 4.
Pantograph provides interfaces to execute proofs, construct expressions, and
examine the symbol list of a Lean project for machine learning.
+See [documentations](doc/) for design rationale and references.
+
## Installation
For Nix users, run
@@ -15,7 +17,9 @@ nix build .#{sharedLib,executable}
```
to build either the shared library or executable.
-Install `elan` and `lake`, and run
+Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and
+run
+
``` sh
lake build
```
@@ -24,9 +28,12 @@ This builds the executable in `.lake/build/bin/pantograph-repl`.
## Executable Usage
``` sh
-pantograph MODULES|LEAN_OPTIONS
+pantograph-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 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
@@ -37,8 +44,6 @@ command { ... }
The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
empty command aborts the REPL.
-The `pantograph` 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`.
Example: (~5k symbols)
```
diff --git a/doc/icon.svg b/doc/icon.svg
index 394b412..eb26a19 100644
--- a/doc/icon.svg
+++ b/doc/icon.svg
@@ -4,17 +4,17 @@
+ id="layer4"
+ inkscape:label="bg" />
+
+
+
+
+
+
+
+
+
+
+
diff --git a/doc/rationale.md b/doc/rationale.md
new file mode 100644
index 0000000..87c1606
--- /dev/null
+++ b/doc/rationale.md
@@ -0,0 +1,30 @@
+# Design Rationale
+
+A great problem in machine learning is to use ML agents to automatically prove
+mathematical theorems. This sort of proof necessarily involves *search*.
+Compatibility for search is the main reason for creating Pantograph. The Lean 4
+LSP interface is not conducive to search. Pantograph is designed with this in
+mind. It emphasizes the difference between 3 views of a proof:
+
+- **Presentation View**: The view of a written, polished proof. e.g. Mathlib and
+ math papers are almost always written in this form.
+- **Search View**: The view of a proof exploration trajectory. This is not
+ explicitly supported by Lean LSP.
+- **Kernel View**: The proof viewed as a set of metavariables.
+
+Pantograph enables proof agents to operate on the search view.
+
+## Name
+
+The name Pantograph is a pun. It means two things
+- A pantograph is an instrument for copying down writing. As an agent explores
+ the vast proof search space, Pantograph records the current state to ensure
+ the proof is sound.
+- A pantograph is also an equipment for an electric train. It supplies power to
+ a locomotive. In comparison the (relatively) simple Pantograph software powers
+ theorem proving projects.
+
+## References
+
+* [Pantograph Paper](https://arxiv.org/abs/2410.16429)
+