From 39b9e0736ae8bfa44e22bbd1809dc296131cd50c Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 18 Oct 2024 15:19:58 -0700
Subject: [PATCH] doc: Stub on setup and drafting

---
 docs/_toc.yml        |  2 ++
 docs/drafting.md     |  9 +++++++++
 docs/goal.md         | 16 +++++++++++++++-
 docs/intro.md        |  2 +-
 docs/proof_search.md | 12 +++++++++++-
 docs/setup.md        | 28 ++++++++++++++++++++++++++++
 6 files changed, 66 insertions(+), 3 deletions(-)
 create mode 100644 docs/drafting.md
 create mode 100644 docs/setup.md

diff --git a/docs/_toc.yml b/docs/_toc.yml
index 3fafd4b..90338a9 100644
--- a/docs/_toc.yml
+++ b/docs/_toc.yml
@@ -3,8 +3,10 @@ root: intro
 parts:
 - caption: Features
   chapters:
+  - file: setup
   - file: goal
   - file: proof_search
+  - file: drafting
 - caption: API Documentation
   chapters:
   - file: api-server
diff --git a/docs/drafting.md b/docs/drafting.md
new file mode 100644
index 0000000..a9b0f53
--- /dev/null
+++ b/docs/drafting.md
@@ -0,0 +1,9 @@
+# Drafting
+
+Pantograph supports drafting from
+[Draft-Sketch-Prove](https://github.com/wellecks/ntptutorial/tree/main/partII_dsp).
+Pantograph's drafting feature is more powerful. At any place in the proof, you
+can replace an expression with `sorry`, and the `sorry` will become a goal.
+
+For an in-depth example, see `experiments/dsp`.
+
diff --git a/docs/goal.md b/docs/goal.md
index 4dc5d65..eaac79e 100644
--- a/docs/goal.md
+++ b/docs/goal.md
@@ -1,12 +1,26 @@
 # Goals and Tactics
 
-Executing tactics in Pantograph is very simple.
+Executing tactics in Pantograph is very simple. To start a proof, call the
+`Server.goal_start` function and supply an expression.
 
 ```python
 from pantograph import Server
 
 server = Server()
 state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
+```
+
+This creates a *goal state*, which consists of a finite number of goals. In this
+case since it is the beginning of a state, it has only one goal. `print(state0)` gives
+
+```
+GoalState(state_id=0, goals=[Goal(variables=[], target='forall (p : Prop), p -> p', name=None, is_conversion=False)], _sentinel=[])
+```
+
+To execute a tactic on a goal state, use `Server.goal_tactic`. This function
+takes a goal id and a tactic. Most Lean tactics are strings.
+
+```python
 state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a")
 ```
 
diff --git a/docs/intro.md b/docs/intro.md
index d25426c..0c21794 100644
--- a/docs/intro.md
+++ b/docs/intro.md
@@ -1,6 +1,6 @@
 # Intro
 
-This is PyPantograph, an machine-to-machine interaction interface for Lean 4.
+This is Pantograph, 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
diff --git a/docs/proof_search.md b/docs/proof_search.md
index 7b2ef6f..de6001f 100644
--- a/docs/proof_search.md
+++ b/docs/proof_search.md
@@ -1,4 +1,14 @@
 # Proof Search
 
-About search ...
+Inherit from the `pantograph.search.Agent` class to create your own search agent.
+```python
+from pantograph.search import Agent
+
+class UnnamedAgent(Agent):
+
+	def next_tactic(self, state, goal_id):
+		pass
+	def guidance(self, state):
+		pass
+```
 
diff --git a/docs/setup.md b/docs/setup.md
new file mode 100644
index 0000000..bc90b43
--- /dev/null
+++ b/docs/setup.md
@@ -0,0 +1,28 @@
+# Setup
+
+Install `poetry`. Then, run
+```sh
+poetry build
+```
+This builds a wheel of Pantograph which can then be installed.
+
+To run the examples and experiments, setup a poetry shell:
+```sh
+poetry install
+poetry shell
+```
+This drops the current shell into an environment where the development packages are available.
+
+All interactions with Lean pass through the `Server` class. Create an instance
+with
+```python
+from pantograph import Server
+server = Server()
+```
+
+## Lean Dependencies
+
+To use external Lean dependencies such as
+[Mathlib4](https://github.com/leanprover-community/mathlib4), Pantograph relies
+on an existing Lean repository. Instructions for creating this repository can be
+found [here](https://docs.lean-lang.org/lean4/doc/setup.html#lake).