Merge pull request #34 from lenianiva/doc/main

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,6 +16,8 @@ jobs:
       id-token: write
     steps:
     - uses: actions/checkout@v3
+      with:
+        submodules: true
 
     # Install dependencies
     - name: Set up Python 3.11
@@ -23,10 +25,25 @@ jobs:
       with:
         python-version: 3.11
 
-    # Build the book
+    - name: Install elan
-    - name: Build the book
       run: |
-        jupyter-book build docs
+        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: |
+        poetry run jupyter-book build docs
 
     # Upload the book's HTML as an artifact
     - name: Upload artifact

docs/_config.yml

@@ -9,7 +9,7 @@ author: Leni Aniva
 # Force re-execution of notebooks on each build.
 # See https://jupyterbook.org/content/execute.html
 execute:
-  execute_notebooks: force
+  execute_notebooks: 'off'
 
 # Define the name of the latex output file for PDF builds
 latex:

docs/_toc.yml

@@ -3,9 +3,14 @@ root: intro
 parts:
 - caption: Features
   chapters:
+  - file: setup
   - file: goal
-  - file: proof_search
+  - file: agent-search
+  - file: data
+  - file: drafting
 - caption: API Documentation
   chapters:
   - file: api-server
   - file: api-search
+  - file: api-expr
+  - file: api-data

docs/agent-search.ipynb

@@ -0,0 +1,155 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "ec3abb52-d7cd-471f-b3b7-2d9681c79360",
+   "metadata": {},
+   "source": [
+    "# Search\n",
+    "\n",
+    "Pantograph supports basic proof search. In this case, Pantograph treats goals as nodes on an and-or tree. The user supplies an agent which should provide two functions:\n",
+    "\n",
+    "1. *Tactic*: Which tactic should be used on a goal?\n",
+    "2. *Guidance*: What is the search priority on a goal?\n",
+    "\n",
+    "The user agent should inherit from `pantograph.search.Agent`. Here is a brute force agent example:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "id": "959458f5-02e4-4f73-ae28-16a756aebed9",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from typing import Optional\n",
+    "import collections\n",
+    "from pantograph import Server\n",
+    "from pantograph.search import Agent\n",
+    "from pantograph.expr import GoalState, Tactic"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "id": "8b402602-3ae5-43e4-9a62-2fa9e2c039fa",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "class DumbAgent(Agent):\n",
+    "\n",
+    "    def __init__(self):\n",
+    "        super().__init__()\n",
+    "\n",
+    "        self.goal_tactic_id_map = collections.defaultdict(lambda : 0)\n",
+    "        self.intros = [\n",
+    "            \"intro\",\n",
+    "        ]\n",
+    "        self.tactics = [\n",
+    "            \"intro h\",\n",
+    "            \"cases h\",\n",
+    "            \"apply Or.inl\",\n",
+    "            \"apply Or.inr\",\n",
+    "        ]\n",
+    "        self.no_space_tactics = [\n",
+    "            \"assumption\",\n",
+    "        ]\n",
+    "\n",
+    "    def next_tactic(\n",
+    "            self,\n",
+    "            state: GoalState,\n",
+    "            goal_id: int,\n",
+    "    ) -> Optional[Tactic]:\n",
+    "        key = (state.state_id, goal_id)\n",
+    "        i = self.goal_tactic_id_map[key]\n",
+    "\n",
+    "        target = state.goals[goal_id].target\n",
+    "        if target.startswith('∀'):\n",
+    "            tactics = self.intros\n",
+    "        elif ' ' in target:\n",
+    "            tactics = self.tactics\n",
+    "        else:\n",
+    "            tactics = self.no_space_tactics\n",
+    "\n",
+    "        if i >= len(tactics):\n",
+    "            return None\n",
+    "\n",
+    "        self.goal_tactic_id_map[key] = i + 1\n",
+    "        return tactics[i]"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "665db9d0-5fff-4b26-9cea-32d06a6e1e04",
+   "metadata": {},
+   "source": [
+    "Execute the search with `agent.search`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "id": "1c7961d1-b1fa-498c-ab75-16feb784ca2c",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "SearchResult(n_goals_root=1, duration=0.7717759609222412, success=True, steps=16)"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "server = Server()\n",
+    "agent = DumbAgent()\n",
+    "goal_state = server.goal_start(\"∀ (p q: Prop), Or p q -> Or q p\")\n",
+    "agent.search(server=server, goal_state=goal_state, verbose=False)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "141e0116-cbb6-4957-aaea-2a1100f80ece",
+   "metadata": {},
+   "source": [
+    "## Automatic and Manual Modes\n",
+    "\n",
+    "The agent chooses one goal and executes a tactic on this goal. What happens to the other goals that are not chosen? By default, the server runs in automatic mode. In automatic mode, all other goals are automatically inherited by a child state, so a user agent could declare a proof finished when there are no more goals remaining in the current goal state.\n",
+    "\n",
+    "Some users may wish to handle sibling goals manually. For example, Aesop's treatment of metavariable coupling is not automatic. To do this, pass the flag `options={ \"automaticMode\" : False }` to the `Server` constructor."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "2090e538-d196-4923-937c-b83fedf1d9a2",
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3 (ipykernel)",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.12.6"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}

docs/api-data.rst

@@ -0,0 +1,5 @@
+Data
+=============
+
+.. automodule:: pantograph.compiler
+    :members:

docs/api-expr.rst

@@ -0,0 +1,8 @@
+Expr
+=============
+
+.. automodule:: pantograph.expr
+    :members:
+
+.. autodata:: pantograph.expr.Expr
+.. autodata:: pantograph.expr.Tactic

docs/data.ipynb

@@ -0,0 +1,167 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "fe7a3037-5c49-4097-9a5d-575b958cc7f8",
+   "metadata": {},
+   "source": [
+    "# Data Extraction"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "id": "fc68ad1d-e64c-48b7-9461-50d872d30473",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import os\n",
+    "from pathlib import Path\n",
+    "from pantograph.server import Server"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "fd13c644-d731-4f81-964e-584bbd43e51c",
+   "metadata": {},
+   "source": [
+    "## Tactic Invocation\n",
+    "\n",
+    "Pantograph can extract tactic invocation data from a Lean file. A **tactic\n",
+    "invocation** is a tuple containing the before and after goal states, and the\n",
+    "tactic which converts the \"before\" state to the \"after\" state.\n",
+    "\n",
+    "To extract tactic invocation data, use `server.tactic_invocations(file_name)`\n",
+    "and supply the file name of the input Lean file."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "id": "a0a2a661-e357-4b80-92d1-4172670ab061",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example\n",
+      "==== #0 ====\n",
+      "/-- Ensure that Aesop is running -/\n",
+      "example : α → α :=\n",
+      "  by aesop\n",
+      "\n",
+      "\n",
+      "==== #1 ====\n",
+      "example : ∀ (p q: Prop), p ∨ q → q ∨ p := by\n",
+      "  intro p q h\n",
+      "  -- Here are some comments\n",
+      "  cases h\n",
+      "  . apply Or.inr\n",
+      "    assumption\n",
+      "  . apply Or.inl\n",
+      "    assumption\n",
+      "\n",
+      "==== Invocations ====\n",
+      "α : Sort ?u.7\n",
+      "⊢ α → α\n",
+      "aesop\n",
+      "\n",
+      "\n",
+      "⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
+      "intro p q h\n",
+      "p q : Prop\n",
+      "h : p ∨ q\n",
+      "⊢ q ∨ p\n",
+      "\n",
+      "p q : Prop\n",
+      "h : p ∨ q\n",
+      "⊢ q ∨ p\n",
+      "cases h\n",
+      "case inl\n",
+      "p q : Prop\n",
+      "h✝ : p\n",
+      "⊢ q ∨ p\n",
+      "case inr p q : Prop h✝ : q ⊢ q ∨ p\n",
+      "\n",
+      "case inl\n",
+      "p q : Prop\n",
+      "h✝ : p\n",
+      "⊢ q ∨ p\n",
+      "apply Or.inr\n",
+      "case inl.h\n",
+      "p q : Prop\n",
+      "h✝ : p\n",
+      "⊢ p\n",
+      "\n",
+      "case inl.h\n",
+      "p q : Prop\n",
+      "h✝ : p\n",
+      "⊢ p\n",
+      "assumption\n",
+      "\n",
+      "\n",
+      "case inr\n",
+      "p q : Prop\n",
+      "h✝ : q\n",
+      "⊢ q ∨ p\n",
+      "apply Or.inl\n",
+      "case inr.h\n",
+      "p q : Prop\n",
+      "h✝ : q\n",
+      "⊢ q\n",
+      "\n",
+      "case inr.h\n",
+      "p q : Prop\n",
+      "h✝ : q\n",
+      "⊢ q\n",
+      "assumption\n",
+      "\n",
+      "\n"
+     ]
+    }
+   ],
+   "source": [
+    "project_path = Path(os.getcwd()).parent.resolve() / 'examples/Example'\n",
+    "print(f\"$PWD: {project_path}\")\n",
+    "server = Server(imports=['Example'], project_path=project_path)\n",
+    "units, invocations = server.tactic_invocations(project_path / \"Example.lean\")\n",
+    "for i, u in enumerate(units):\n",
+    "    print(f\"==== #{i} ====\")\n",
+    "    print(u)\n",
+    "print(\"==== Invocations ====\")\n",
+    "for i in invocations:\n",
+    "    print(f\"{i.before}\\n{i.tactic}\\n{i.after}\\n\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "51f5398b-5416-4dc1-81cd-6d2514758232",
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3 (ipykernel)",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.12.6"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}

docs/drafting.ipynb

@@ -0,0 +1,165 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "aecc5260-56ad-4734-8917-3a4d92910309",
+   "metadata": {},
+   "source": [
+    "# Drafting\n",
+    "\n",
+    "Pantograph supports drafting (technically the sketch step) from\n",
+    "[Draft-Sketch-Prove](https://github.com/wellecks/ntptutorial/tree/main/partII_dsp).\n",
+    "Pantograph's drafting feature is more powerful. At any place in the proof, you\n",
+    "can replace an expression with `sorry`, and the `sorry` will become a goal.\n",
+    "\n",
+    "At this point we must introduce the idea of compilation units. Each Lean\n",
+    "definition, theorem, constant, etc., is a *compilation unit*. When Pantograph\n",
+    "extracts data from Lean source code, it sections the data into these compilation\n",
+    "units.\n",
+    "\n",
+    "For example, consider this sketch produced by a language model prover:\n",
+    "```lean\n",
+    "theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by\n",
+    "   intros n m\n",
+    "   induction n with\n",
+    "   | zero =>\n",
+    "     have h_base: 0 + m = m := sorry\n",
+    "     have h_symm: m + 0 = m := sorry\n",
+    "     sorry\n",
+    "   | succ n ih =>\n",
+    "     have h_inductive: n + m = m + n := sorry\n",
+    "     have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry\n",
+    "     have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry\n",
+    "     have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry\n",
+    "     sorry\n",
+    "```\n",
+    "There are some `sorry`s that we want to solve automatically with hammer tactics. We can do this by drafting. Feeding this into the drafting feature produces one goal state (corresponding to the one compilation unit) containing as many goals as the draft has `sorry`s:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "id": "52bd153d-235c-47fa-917e-415d444867a5",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "m : Nat\n",
+      "⊢ 0 + m = m\n",
+      "m : Nat\n",
+      "h_base : 0 + m = m\n",
+      "⊢ m + 0 = m\n",
+      "m : Nat\n",
+      "h_base : 0 + m = m\n",
+      "h_symm : m + 0 = m\n",
+      "⊢ 0 + m = m + 0\n",
+      "m : Nat\n",
+      "n : Nat\n",
+      "ih : n + m = m + n\n",
+      "⊢ n + m = m + n\n",
+      "m : Nat\n",
+      "n : Nat\n",
+      "ih : n + m = m + n\n",
+      "h_inductive : n + m = m + n\n",
+      "⊢ m + n.succ = (m + n).succ\n",
+      "m : Nat\n",
+      "n : Nat\n",
+      "ih : n + m = m + n\n",
+      "h_inductive : n + m = m + n\n",
+      "h_pull_succ_out_from_right : m + n.succ = (m + n).succ\n",
+      "⊢ (n + m).succ = (m + n).succ\n",
+      "m : Nat\n",
+      "n : Nat\n",
+      "ih : n + m = m + n\n",
+      "h_inductive : n + m = m + n\n",
+      "h_pull_succ_out_from_right : m + n.succ = (m + n).succ\n",
+      "h_flip_n_plus_m : (n + m).succ = (m + n).succ\n",
+      "⊢ n.succ + m = (n + m).succ\n",
+      "m : Nat\n",
+      "n : Nat\n",
+      "ih : n + m = m + n\n",
+      "h_inductive : n + m = m + n\n",
+      "h_pull_succ_out_from_right : m + n.succ = (m + n).succ\n",
+      "h_flip_n_plus_m : (n + m).succ = (m + n).succ\n",
+      "h_pull_succ_out_from_left : n.succ + m = (n + m).succ\n",
+      "⊢ n + 1 + m = m + (n + 1)\n"
+     ]
+    }
+   ],
+   "source": [
+    "from pantograph import Server\n",
+    "\n",
+    "sketch = \"\"\"\n",
+    "theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by\n",
+    "   -- Consider some n and m in Nats.\n",
+    "   intros n m\n",
+    "   -- Perform induction on n.\n",
+    "   induction n with\n",
+    "   | zero =>\n",
+    "     -- Base case: When n = 0, we need to show 0 + m = m + 0.\n",
+    "     -- We have the fact 0 + m = m by the definition of addition.\n",
+    "     have h_base: 0 + m = m := sorry\n",
+    "     -- We also have the fact m + 0 = m by the definition of addition.\n",
+    "     have h_symm: m + 0 = m := sorry\n",
+    "     -- Combine facts to close goal\n",
+    "     sorry\n",
+    "   | succ n ih =>\n",
+    "     -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n.\n",
+    "     -- By the inductive hypothesis, we have n + m = m + n.\n",
+    "     have h_inductive: n + m = m + n := sorry\n",
+    "     -- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ.\n",
+    "     have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry\n",
+    "     -- 2. then to flip m + S n to something like S (n + m) we need to use the IH.\n",
+    "     have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry\n",
+    "     -- 3. Now the n & m are on the correct sides Nat.succ n + m = Nat.succ (n + m), so let's use the def of addition to pull out the succ from the addition on the left using Nat.succ_add.\n",
+    "     have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry\n",
+    "     -- Combine facts to close goal\n",
+    "     sorry\n",
+    "\"\"\"\n",
+    "\n",
+    "server = Server()\n",
+    "state0, = server.load_sorry(sketch)\n",
+    "print(state0)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "0d4dda56-7b7f-4c4c-b59d-af6f857d7788",
+   "metadata": {},
+   "source": [
+    "For an in-depth example, see `experiments/dsp`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "eaf8e506-a6d1-4e9a-ad7a-f7bbb82e01c6",
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3 (ipykernel)",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.12.6"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}

docs/goal.ipynb

@@ -0,0 +1,315 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "c5106980-4850-4bea-a333-5a1b2e4d1dc5",
+   "metadata": {},
+   "source": [
+    "# Goals and Tactics\n",
+    "\n",
+    "Executing tactics in Pantograph is simple. To start a proof, call the\n",
+    "`Server.goal_start` function and supply an expression."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "id": "3257de2b-41ca-4cfe-b66c-1ef4781c98b0",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from pantograph import Server\n",
+    "from pantograph.expr import TacticHave, TacticCalc, TacticExpr"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "id": "6783d478-d8c7-4c4e-a56e-8170384297ef",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "server = Server()\n",
+    "state0 = server.goal_start(\"forall (p q: Prop), Or p q -> Or q p\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "bfe5a9df-33c2-4538-a9ce-fc0e02c92ff2",
+   "metadata": {},
+   "source": [
+    "This creates a *goal state*, which consists of a finite number of goals. In this\n",
+    "case since it is the beginning of a state, it has only one goal."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "id": "eefc9094-9574-4f92-9aa2-c39beb85389b",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "\n",
+      "⊢ forall (p q: Prop), Or p q -> Or q p\n"
+     ]
+    }
+   ],
+   "source": [
+    "print(state0)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "26dbe212-e09e-42dd-ab15-65ee2fba6234",
+   "metadata": {},
+   "source": [
+    "To execute a tactic on a goal state, use `Server.goal_tactic`. This function\n",
+    "takes a goal id and a tactic. Most Lean tactics are strings."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "id": "c907dbb6-4d6a-4aa7-b173-60220165ba9e",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "a : Prop\n",
+      "⊢ ∀ (q : Prop), a ∨ q → q ∨ a\n"
+     ]
+    }
+   ],
+   "source": [
+    "state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro a\")\n",
+    "print(state1)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "9978fdcf-a12b-4f22-9551-5e04c262e5e0",
+   "metadata": {},
+   "source": [
+    "Executing a tactic produces a new goal state. If this goal state has no goals,\n",
+    "the proof is complete. You can recover the usual form of a goal with `str()`"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "id": "16595c5e-2285-49d5-8340-397ad1e6c9e7",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "'a : Prop\\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a'"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "str(state1.goals[0])"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "67f2a75d-6851-4393-bac9-a091400f1906",
+   "metadata": {},
+   "source": [
+    "## Error Handling and GC\n",
+    "\n",
+    "When a tactic fails, it throws an exception:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "id": "c9784ba2-3810-4f80-a6c4-33d5eef3003e",
+   "metadata": {
+    "scrolled": true
+   },
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "[\"tactic 'assumption' failed\\na : Prop\\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a\"]\n"
+     ]
+    }
+   ],
+   "source": [
+    "try:\n",
+    "    state2 = server.goal_tactic(state1, goal_id=0, tactic=\"assumption\")\n",
+    "    print(\"Should not reach this\")\n",
+    "except Exception as e:\n",
+    "    print(e)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "1ae60d9e-8656-4f26-b495-d04bced250fc",
+   "metadata": {},
+   "source": [
+    "A state with no goals is considered solved"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "id": "1cb96b19-d3bb-4533-abeb-a7dbc5bc8c3e",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "GoalState(state_id=5, goals=[], _sentinel=[0, 1])"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "state0 = server.goal_start(\"forall (p : Prop), p -> p\")\n",
+    "state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro\")\n",
+    "state2 = server.goal_tactic(state1, goal_id=0, tactic=\"intro h\")\n",
+    "state3 = server.goal_tactic(state2, goal_id=0, tactic=\"exact h\")\n",
+    "state3"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "a2945e71-e583-4ae0-9c0f-83035f0492f2",
+   "metadata": {},
+   "source": [
+    "Execute `server.gc()` once in a while to delete unused goals."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "id": "d53624ff-c720-4847-98f7-28e109eb76e7",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "server.gc()"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "0b59e05e-7d8c-4fad-b8ca-375ea995ea5b",
+   "metadata": {},
+   "source": [
+    "## Special Tactics\n",
+    "\n",
+    "Lean has special provisions for some tactics. This includes `have`, `let`,\n",
+    "`calc`. To execute one of these tactics, create a `TacticHave`, `TacticLet`,\n",
+    "`TacticCalc` instance and feed it into `server.goal_tactic`"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "id": "526d620b-064f-4ec0-a7b2-6a1ef3c6f6e7",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "\n",
+      "⊢ 2 = 1 + 1\n",
+      "h : 2 = 1 + 1\n",
+      "⊢ 1 + 1 = 2\n"
+     ]
+    }
+   ],
+   "source": [
+    "state0 = server.goal_start(\"1 + 1 = 2\")\n",
+    "state1 = server.goal_tactic(state0, goal_id=0, tactic=TacticHave(branch=\"2 = 1 + 1\", binder_name=\"h\"))\n",
+    "print(state1)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "c415d436-ed0d-475f-bf5e-b8dc63954c7e",
+   "metadata": {},
+   "source": [
+    "The `TacticExpr` \"tactic\" parses an expression and assigns it to the current\n",
+    "goal.  This leverages Lean's type unification system and is as expressive as\n",
+    "Lean expressions. Many proofs in Mathlib4 are written in a mixture of expression\n",
+    "and tactic forms."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "id": "e1f06441-4d77-45a7-a1c3-b800b96a8105",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "\n"
+     ]
+    }
+   ],
+   "source": [
+    "state0 = server.goal_start(\"forall (p : Prop), p -> p\")\n",
+    "state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro p\")\n",
+    "state2 = server.goal_tactic(state1, goal_id=0, tactic=TacticExpr(\"fun h => h\"))\n",
+    "print(state2)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "d6bcd026-507b-4b1c-8dee-006df53636b0",
+   "metadata": {},
+   "source": [
+    "To execute the `conv` tactic, use `server.goal_conv_begin` to enter conv mode on\n",
+    "one goal, and use `server.goal_conv_end` to exit from conv mode. Pantograph will\n",
+    "provide interactive feedback upon every tactic executed in `conv` mode."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "2b0b27c6-0c69-4255-aed1-c0713c227ccc",
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3 (ipykernel)",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.12.6"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}

docs/goal.md

@@ -1,12 +0,0 @@
-# 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,6 +1,6 @@
-# Intro
+# Introduction
 
-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 +0,0 @@
-# Proof Search
-
-About search ...
-

docs/setup.md

@@ -0,0 +1,47 @@
+# 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
+
+The server created from `Server()` is sufficient for basic theorem proving tasks
+reliant on Lean's `Init` library. Some users may find this insufficient and want
+to use non-builtin libraries such as Aesop or Mathlib4.
+
+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).
+
+After creating this initial Lean repository, execute in the repository
+```sh
+lake build
+```
+
+to build all files from the repository. This step is necessary after any file in
+the repository is modified.
+
+Then, feed the repository's path to the server
+```python
+server = Server(project_path="./path-to-lean-repo/")
+```
+
+For a complete example, see `examples/`.

examples/all.ipynb

@@ -239,14 +239,9 @@
    "source": [
     "import subprocess, os\n",
     "from pathlib import Path\n",
-    "def get_project_and_lean_path():\n",
+    "project_path = Path(os.getcwd()).resolve() / 'Example'\n",
-    "    cwd = Path(os.getcwd()).resolve() / 'Example'\n",
-    "    p = subprocess.check_output(['lake', 'env', 'printenv', 'LEAN_PATH'], cwd=cwd)\n",
-    "    return cwd, p\n",
-    "project_path, lean_path = get_project_and_lean_path()\n",
     "print(f\"$PWD: {project_path}\")\n",
-    "print(f\"$LEAN_PATH: {lean_path}\")\n",
+    "server = Server(imports=['Example'], project_path=project_path)"
-    "server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)"
    ]
   },
   {
@@ -445,7 +440,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.12.4"
+   "version": "3.12.6"
   }
  },
  "nbformat": 4,

pantograph/compiler.py

@@ -2,6 +2,10 @@ from dataclasses import dataclass
 
 @dataclass(frozen=True)
 class TacticInvocation:
+    """
+    One tactic invocation with the before/after goals extracted from Lean source
+    code.
+    """
     before: str
     after: str
     tactic: str

pantograph/expr.py

@@ -2,11 +2,14 @@
 Data structuers for expressions and goals
 """
 from dataclasses import dataclass, field
-from typing import Optional, Union
+from typing import Optional, TypeAlias
 
-Expr = str
+Expr: TypeAlias = str
 
 def parse_expr(payload: dict) -> Expr:
+    """
+    :meta private:
+    """
     return payload["pp"]
 
 @dataclass(frozen=True)
@@ -25,6 +28,9 @@ class Variable:
         return Variable(t, v, name)
 
     def __str__(self):
+        """
+        :meta public:
+        """
         result = self.name if self.name else "_"
         result += f" : {self.t}"
         if self.v:
@@ -41,6 +47,9 @@ class Goal:
 
     @staticmethod
     def sentence(target: Expr):
+        """
+        :meta public:
+        """
         return Goal(variables=[], target=target)
 
     @staticmethod
@@ -56,6 +65,9 @@ class Goal:
         return Goal(variables, target, sibling_dep, name, is_conversion)
 
     def __str__(self):
+        """
+        :meta public:
+        """
         front = "|" if self.is_conversion else "⊢"
         return "\n".join(str(v) for v in self.variables) + \
             f"\n{front} {self.target}"
@@ -74,6 +86,8 @@ class GoalState:
     def is_solved(self) -> bool:
         """
         WARNING: Does not handle dormant goals.
+
+        :meta public:
         """
         return not self.goals
 
@@ -87,6 +101,9 @@ class GoalState:
         return GoalState.parse_inner(payload["nextStateId"], payload["goals"], _sentinel)
 
     def __str__(self):
+        """
+        :meta public:
+        """
         return "\n".join([str(g) for g in self.goals])
 
 @dataclass(frozen=True)
@@ -102,7 +119,7 @@ class TacticHave:
 @dataclass(frozen=True)
 class TacticLet:
     """
-    The `have` tactic, equivalent to
+    The `let` tactic, equivalent to
     ```lean
     let {binder_name} : {branch} := ...
     ```
@@ -126,4 +143,4 @@ class TacticExpr:
     """
     expr: str
 
-Tactic = Union[str, TacticHave, TacticLet, TacticCalc, TacticExpr]
+Tactic: TypeAlias = str | TacticHave | TacticLet | TacticCalc | TacticExpr

pantograph/server.py

@@ -24,12 +24,28 @@ def _get_proc_cwd():
 def _get_proc_path():
     return _get_proc_cwd() / "pantograph-repl"
 
-class TacticFailure(Exception):
+def get_lean_path(project_path):
-    pass
+    """
-class ServerError(Exception):
+    Extracts the `LEAN_PATH` variable from a project path.
-    pass
+    """
+    import subprocess
+    p = subprocess.check_output(
+        ['lake', 'env', 'printenv', 'LEAN_PATH'],
+        cwd=project_path,
+    )
+    return p
 
-DEFAULT_CORE_OPTIONS=["maxHeartbeats=0", "maxRecDepth=100000"]
+class TacticFailure(Exception):
+    """
+    Indicates a tactic failed to execute
+    """
+class ServerError(Exception):
+    """
+    Indicates a logical error in the server.
+    """
+
+
+DEFAULT_CORE_OPTIONS = ["maxHeartbeats=0", "maxRecDepth=100000"]
 
 
 class Server:
@@ -54,6 +70,8 @@ class Server:
         self.timeout = timeout
         self.imports = imports
         self.project_path = project_path if project_path else _get_proc_cwd()
+        if project_path and not lean_path:
+            lean_path = get_lean_path(project_path)
         self.lean_path = lean_path
         self.maxread = maxread
         self.proc_path = _get_proc_path()
@@ -68,6 +86,9 @@ class Server:
         self.to_remove_goal_states = []
 
     def is_automatic(self):
+        """
+        Check if the server is running in automatic mode
+        """
         return self.options.get("automaticMode", True)
 
     def restart(self):
@@ -100,6 +121,8 @@ class Server:
     def run(self, cmd, payload):
         """
         Runs a raw JSON command. Preferably use one of the commands below.
+
+        :meta private:
         """
         assert self.proc
         s = json.dumps(payload)
@@ -123,9 +146,7 @@ class Server:
 
     def gc(self):
         """
-        Garbage collect deleted goal states.
+        Garbage collect deleted goal states to free up memory.
-
-        Must be called periodically.
         """
         if not self.to_remove_goal_states:
             return
@@ -145,6 +166,9 @@ class Server:
         return parse_expr(result["type"])
 
     def goal_start(self, expr: Expr) -> GoalState:
+        """
+        Create a goal state with one root goal, whose target is `expr`
+        """
         result = self.run('goal.start', {"expr": str(expr)})
         if "error" in result:
             print(f"Cannot start goal: {expr}")
@@ -152,6 +176,9 @@ class Server:
         return GoalState(state_id=result["stateId"], goals=[Goal.sentence(expr)], _sentinel=self.to_remove_goal_states)
 
     def goal_tactic(self, state: GoalState, goal_id: int, tactic: Tactic) -> GoalState:
+        """
+        Execute a tactic on `goal_id` of `state`
+        """
         args = {"stateId": state.state_id, "goalId": goal_id}
         if isinstance(tactic, str):
             args["tactic"] = tactic
@@ -179,6 +206,9 @@ class Server:
         return GoalState.parse(result, self.to_remove_goal_states)
 
     def goal_conv_begin(self, state: GoalState, goal_id: int) -> GoalState:
+        """
+        Start conversion tactic mode on one goal
+        """
         result = self.run('goal.tactic', {"stateId": state.state_id, "goalId": goal_id, "conv": True})
         if "error" in result:
             raise ServerError(result["desc"])
@@ -189,6 +219,9 @@ class Server:
         return GoalState.parse(result, self.to_remove_goal_states)
 
     def goal_conv_end(self, state: GoalState) -> GoalState:
+        """
+        Exit conversion tactic mode on all goals
+        """
         result = self.run('goal.tactic', {"stateId": state.state_id, "goalId": 0, "conv": False})
         if "error" in result:
             raise ServerError(result["desc"])
@@ -213,7 +246,7 @@ class Server:
         with open(file_name, 'rb') as f:
             content = f.read()
             units = [
-                content[unit["bounary"][0]:unit["boundary"][1]].decode('utf-8')
+                content[unit["boundary"][0]:unit["boundary"][1]].decode('utf-8')
                 for unit in result['units']
             ]
             invocations = [

poetry.lock

@@ -730,20 +730,6 @@ docs = ["furo (>=2024.8.6)", "sphinx (>=8.0.2)", "sphinx-autodoc-typehints (>=2.
 testing = ["covdefaults (>=2.3)", "coverage (>=7.6.1)", "diff-cover (>=9.2)", "pytest (>=8.3.3)", "pytest-asyncio (>=0.24)", "pytest-cov (>=5)", "pytest-mock (>=3.14)", "pytest-timeout (>=2.3.1)", "virtualenv (>=20.26.4)"]
 typing = ["typing-extensions (>=4.12.2)"]
 
-[[package]]
-name = "fire"
-version = "0.6.0"
-description = "A library for automatically generating command line interfaces."
-optional = false
-python-versions = "*"
-files = [
-    {file = "fire-0.6.0.tar.gz", hash = "sha256:54ec5b996ecdd3c0309c800324a0703d6da512241bc73b553db959d98de0aa66"},
-]
-
-[package.dependencies]
-six = "*"
-termcolor = "*"
-
 [[package]]
 name = "fonttools"
 version = "4.54.1"
@@ -4774,4 +4760,4 @@ type = ["pytest-mypy"]
 [metadata]
 lock-version = "2.0"
 python-versions = "^3.10"
-content-hash = "aa77c3311618b388d51c1739124cae9be0406e50e003b8ee2ee6eb1915aa7a90"
+content-hash = "12935bf20e5ac4351734a47b1a71486daccbc0eed1239abe67858b3b17df8b37"

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]