doc: Documentations in pages

.github/workflows/docs.yaml

@@ -5,7 +5,7 @@ on:
   push:
     branches:
     - main
-    - docs/main
+    - doc/main
 
 # This job installs dependencies, builds the book, and pushes it to `gh-pages`
 jobs:
@@ -16,17 +16,34 @@ jobs:
       id-token: write
     steps:
     - uses: actions/checkout@v3
+      with:
+        submodules: true
 
     # Install dependencies
     - name: Set up Python 3.11
       uses: actions/setup-python@v4
       with:
         python-version: 3.11
 
-    # Build the book
-    - name: Build the book
+    - name: Install elan
+      run: |
+        set -o pipefail
+        curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+        ./elan-init -y --default-toolchain none
+        echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
+    - name: Install Lean
+      run: |
+        elan toolchain install $(<src/lean-toolchain)
+
+    - name: Install poetry
+      run: |
+        pip install poetry
+        poetry install --only doc
+
+    - name: Build documentations
       run: |
-        jupyter-book build docs
+        poetry run jupyter-book build docs
 
     # Upload the book's HTML as an artifact
     - name: Upload artifact

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

pyproject.toml

@@ -16,7 +16,6 @@ script = "build.py"
 
 [tool.poetry.group.dev.dependencies]
 # Experiment related dependencies here to not clutter the main project dependencies.
-fire = "0.6.0"
 notebook = "^7.2.1"
 numpy = "^1.26.4"
 openai = "^1.31.0"
@@ -30,6 +29,10 @@ termcolor = "^2.4.0"
 matplotlib = "^3.9.2"
 seaborn = "^0.13.2"
 pandas = "^2.2.3"
+
+[tool.poetry.group.doc]
+optional = true
+[tool.poetry.group.doc.dependencies]
 jupyter-book = "^1.0.3"
 
 [build-system]