doc: Stub on setup and drafting

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

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`.
+

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

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

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

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).