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,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/_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