doc: Build instructions

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`

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

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")
+```
+

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.

docs/proof_search.md

@@ -1,4 +1,4 @@
-# Search
+# Proof Search
 
 About search ...