From 8dd59bb8911a8e9d8f387f330e4dcf26286bc584 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 17 Oct 2024 21:28:23 -0700
Subject: [PATCH] doc: Build instructions

---
 README.md                           | 12 ++++++++++++
 docs/_toc.yml                       |  5 +++--
 docs/goal.md                        | 12 ++++++++++++
 docs/intro.md                       | 23 +++++++++++++++++++++++
 docs/{search.md => proof_search.md} |  2 +-
 5 files changed, 51 insertions(+), 3 deletions(-)
 create mode 100644 docs/goal.md
 rename docs/{search.md => proof_search.md} (55%)

diff --git a/README.md b/README.md
index 96829fc..549e235 100644
--- a/README.md
+++ b/README.md
@@ -16,6 +16,18 @@ poetry build
 poetry install
 ```
 
+## Documentation
+
+Build the documentations by
+```sh
+jupyter-book build docs
+```
+Then serve
+```sh
+cd docs/_build/html
+python3 -m http.server -d .
+```
+
 ## Examples
 
 For API interaction examples, see `examples/README.md`
diff --git a/docs/_toc.yml b/docs/_toc.yml
index d7af6bd..d043bd5 100644
--- a/docs/_toc.yml
+++ b/docs/_toc.yml
@@ -1,6 +1,7 @@
 format: jb-book
 root: intro
 parts:
-- caption: Basic examples 🪄
+- caption: Features
   chapters:
-  - file: search
+  - file: goal
+  - file: proof_search
diff --git a/docs/goal.md b/docs/goal.md
new file mode 100644
index 0000000..4dc5d65
--- /dev/null
+++ b/docs/goal.md
@@ -0,0 +1,12 @@
+# Goals and Tactics
+
+Executing tactics in Pantograph is very simple.
+
+```python
+from pantograph import Server
+
+server = Server()
+state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
+state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a")
+```
+
diff --git a/docs/intro.md b/docs/intro.md
index fc44b48..d25426c 100644
--- a/docs/intro.md
+++ b/docs/intro.md
@@ -1,2 +1,25 @@
 # Intro
 
+This is PyPantograph, an machine-to-machine interaction interface for Lean 4.
+Its main purpose is to train and evaluate theorem proving agents. The main
+features are:
+1. Interfacing via the Python library, REPL, or C Library
+2. A mixture of expression-based and tactic-based proofs
+3. Pantograph has been designed with facilitating search in mind. A theorem
+   proving agent can simultaneously explore multiple branches of the proof.
+4. Handling of metavariable coupling
+5. Reading/Adding symbols from the environment
+6. Extraction of tactic training data
+7. Support for drafting
+
+## Design Rationale
+
+The Lean 4 interface is not conducive to search. Readers familiar with Coq may
+know that the Coq Serapi was superseded by CoqLSP. In the opinion of the
+authors, this is a mistake. An interface conducive for human operators to write
+proofs is often not an interface conductive to search.
+
+LeanDojo has architectural limitations that prevent it from gaining new features
+such as drafting without refactoring. Almost all of Pantograph's business logic
+is written in Lean, and Pantograph achieves tighter coupling between the data
+extraction and proof search components.
diff --git a/docs/search.md b/docs/proof_search.md
similarity index 55%
rename from docs/search.md
rename to docs/proof_search.md
index 6b9a2fe..7b2ef6f 100644
--- a/docs/search.md
+++ b/docs/proof_search.md
@@ -1,4 +1,4 @@
-# Search
+# Proof Search
 
 About search ...