From 9a8d90880a6d017796eb110f54674ece5c210896 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 18 Oct 2024 14:56:08 -0700 Subject: [PATCH 01/13] fix: Install jupyter book dependency --- .github/workflows/docs.yaml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index c496398..dc814d9 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -23,6 +23,10 @@ jobs: with: python-version: 3.11 + - name: Install dependencies + run: | + pip install jupyter-book + # Build the book - name: Build the book run: | From 9fe5a557f2e86b83ae3b477cd85d733e6dae3639 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 18 Oct 2024 14:57:30 -0700 Subject: [PATCH 02/13] fix: Docs branch name --- .github/workflows/docs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index dc814d9..49a43b7 100644 --- a/.github/workflows/docs.yaml +++ b/.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: From 39b9e0736ae8bfa44e22bbd1809dc296131cd50c Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 18 Oct 2024 15:19:58 -0700 Subject: [PATCH 03/13] 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). From dd6efc848506cceae8997ed08fa47c02e611dc5a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 18 Oct 2024 15:27:57 -0700 Subject: [PATCH 04/13] fix: Doc building in poetry --- .github/workflows/docs.yaml | 5 +++-- poetry.lock | 16 +--------------- pyproject.toml | 5 ++++- 3 files changed, 8 insertions(+), 18 deletions(-) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index 49a43b7..70123d0 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -25,12 +25,13 @@ jobs: - name: Install dependencies run: | - pip install jupyter-book + pip install poetry + poetry install --only doc # Build the book - name: Build the book run: | - jupyter-book build docs + poetry run jupyter-book build docs # Upload the book's HTML as an artifact - name: Upload artifact diff --git a/poetry.lock b/poetry.lock index d2e7011..2a7ad49 100644 --- a/poetry.lock +++ b/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" diff --git a/pyproject.toml b/pyproject.toml index 0597021..ef55b3c 100644 --- a/pyproject.toml +++ b/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] From 5379b0abe29912c26abbf7a691f2f9dff299cd7d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 18 Oct 2024 15:30:12 -0700 Subject: [PATCH 05/13] fix: Install elan in pipeline --- .github/workflows/docs.yaml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index 70123d0..1603789 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -28,6 +28,13 @@ jobs: pip install poetry poetry install --only doc + - 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}" + # Build the book - name: Build the book run: | From 92edb0d0cd84caec544ab4330dbd5cd8c226cf45 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 18 Oct 2024 15:34:37 -0700 Subject: [PATCH 06/13] chore: Fix build task names and check lake --- .github/workflows/docs.yaml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index 1603789..a1024f5 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -23,20 +23,23 @@ jobs: with: python-version: 3.11 - - name: Install dependencies - run: | - pip install poetry - poetry install --only doc - - - name: install elan + - 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}" - # Build the book - - name: Build the book + - name: Print lean and lake versions + run: | + lake --version + + - name: Install poetry + run: | + pip install poetry + poetry install --only doc + + - name: Build documentations run: | poetry run jupyter-book build docs From 0fef9e292385056bc31f678223a6a5550fc33c87 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 18 Oct 2024 15:37:35 -0700 Subject: [PATCH 07/13] fix: Install Lean toolchain --- .github/workflows/docs.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index a1024f5..b6e6469 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -29,6 +29,7 @@ jobs: 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}" + elan toolchain install $( Date: Fri, 18 Oct 2024 15:38:18 -0700 Subject: [PATCH 08/13] fix: Move elan to next step --- .github/workflows/docs.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index b6e6469..6e7f7bd 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -29,10 +29,10 @@ jobs: 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}" - elan toolchain install $( Date: Fri, 18 Oct 2024 15:39:36 -0700 Subject: [PATCH 09/13] fix: Checkout submodules --- .github/workflows/docs.yaml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index 6e7f7bd..4462fe9 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -16,6 +16,8 @@ jobs: id-token: write steps: - uses: actions/checkout@v3 + with: + submodules: true # Install dependencies - name: Set up Python 3.11 From 1f3784d12ca75bf032ed00e694e3d17792785eaa Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 18 Oct 2024 15:40:52 -0700 Subject: [PATCH 10/13] fix: Remove lake version check --- .github/workflows/docs.yaml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index 4462fe9..b7a78ed 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -32,10 +32,9 @@ jobs: ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" - - name: Print lean and lake versions + - name: Install Lean run: | elan toolchain install $( Date: Sun, 20 Oct 2024 09:52:12 -0700 Subject: [PATCH 11/13] doc: autodocs for expr and data --- docs/_toc.yml | 2 ++ docs/api-data.rst | 5 +++++ docs/api-expr.rst | 8 ++++++++ pantograph/compiler.py | 4 ++++ pantograph/expr.py | 25 +++++++++++++++++++++---- pantograph/server.py | 12 +++++++++--- 6 files changed, 49 insertions(+), 7 deletions(-) create mode 100644 docs/api-data.rst create mode 100644 docs/api-expr.rst diff --git a/docs/_toc.yml b/docs/_toc.yml index 90338a9..75ef629 100644 --- a/docs/_toc.yml +++ b/docs/_toc.yml @@ -11,3 +11,5 @@ parts: chapters: - file: api-server - file: api-search + - file: api-expr + - file: api-data diff --git a/docs/api-data.rst b/docs/api-data.rst new file mode 100644 index 0000000..e853b1d --- /dev/null +++ b/docs/api-data.rst @@ -0,0 +1,5 @@ +Data +============= + +.. automodule:: pantograph.compiler + :members: diff --git a/docs/api-expr.rst b/docs/api-expr.rst new file mode 100644 index 0000000..532049b --- /dev/null +++ b/docs/api-expr.rst @@ -0,0 +1,8 @@ +Expr +============= + +.. automodule:: pantograph.expr + :members: + +.. autodata:: pantograph.expr.Expr +.. autodata:: pantograph.expr.Tactic diff --git a/pantograph/compiler.py b/pantograph/compiler.py index f2f01bc..e881cec 100644 --- a/pantograph/compiler.py +++ b/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 diff --git a/pantograph/expr.py b/pantograph/expr.py index 6cdad1c..5c8bbc2 100644 --- a/pantograph/expr.py +++ b/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 diff --git a/pantograph/server.py b/pantograph/server.py index ddab073..da8fb72 100644 --- a/pantograph/server.py +++ b/pantograph/server.py @@ -100,6 +100,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 +125,7 @@ class Server: def gc(self): """ - Garbage collect deleted goal states. - - Must be called periodically. + Garbage collect deleted goal states to free up memory. """ if not self.to_remove_goal_states: return @@ -145,6 +145,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 +155,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 From 7a2278cb7009e39d8c6d7400d5b2aea003f90a3b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 20 Oct 2024 19:22:35 -0700 Subject: [PATCH 12/13] doc: Add comprehensive documentation fix: Typo in `Server.tactic_invocations` --- docs/_toc.yml | 3 +- docs/agent-search.ipynb | 155 ++++++++++++++++++++ docs/data.ipynb | 167 +++++++++++++++++++++ docs/drafting.ipynb | 165 +++++++++++++++++++++ docs/drafting.md | 9 -- docs/goal.ipynb | 315 ++++++++++++++++++++++++++++++++++++++++ docs/goal.md | 26 ---- docs/intro.md | 2 +- docs/proof_search.md | 14 -- docs/setup.md | 19 +++ examples/all.ipynb | 11 +- pantograph/server.py | 39 ++++- 12 files changed, 860 insertions(+), 65 deletions(-) create mode 100644 docs/agent-search.ipynb create mode 100644 docs/data.ipynb create mode 100644 docs/drafting.ipynb delete mode 100644 docs/drafting.md create mode 100644 docs/goal.ipynb delete mode 100644 docs/goal.md delete mode 100644 docs/proof_search.md diff --git a/docs/_toc.yml b/docs/_toc.yml index 75ef629..77e77a9 100644 --- a/docs/_toc.yml +++ b/docs/_toc.yml @@ -5,7 +5,8 @@ parts: chapters: - file: setup - file: goal - - file: proof_search + - file: agent-search + - file: data - file: drafting - caption: API Documentation chapters: diff --git a/docs/agent-search.ipynb b/docs/agent-search.ipynb new file mode 100644 index 0000000..c3a626c --- /dev/null +++ b/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 +} diff --git a/docs/data.ipynb b/docs/data.ipynb new file mode 100644 index 0000000..cb616f6 --- /dev/null +++ b/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 +} diff --git a/docs/drafting.ipynb b/docs/drafting.ipynb new file mode 100644 index 0000000..f5dfd5a --- /dev/null +++ b/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 +} diff --git a/docs/drafting.md b/docs/drafting.md deleted file mode 100644 index a9b0f53..0000000 --- a/docs/drafting.md +++ /dev/null @@ -1,9 +0,0 @@ -# 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.ipynb b/docs/goal.ipynb new file mode 100644 index 0000000..b59748f --- /dev/null +++ b/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 +} diff --git a/docs/goal.md b/docs/goal.md deleted file mode 100644 index eaac79e..0000000 --- a/docs/goal.md +++ /dev/null @@ -1,26 +0,0 @@ -# Goals and Tactics - -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 0c21794..107c532 100644 --- a/docs/intro.md +++ b/docs/intro.md @@ -1,4 +1,4 @@ -# Intro +# Introduction 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 diff --git a/docs/proof_search.md b/docs/proof_search.md deleted file mode 100644 index de6001f..0000000 --- a/docs/proof_search.md +++ /dev/null @@ -1,14 +0,0 @@ -# Proof 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 index bc90b43..f1a4382 100644 --- a/docs/setup.md +++ b/docs/setup.md @@ -22,7 +22,26 @@ 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/`. diff --git a/examples/all.ipynb b/examples/all.ipynb index 8195cd4..121cd5a 100644 --- a/examples/all.ipynb +++ b/examples/all.ipynb @@ -239,14 +239,9 @@ "source": [ "import subprocess, os\n", "from pathlib import Path\n", - "def get_project_and_lean_path():\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", + "project_path = Path(os.getcwd()).resolve() / 'Example'\n", "print(f\"$PWD: {project_path}\")\n", - "print(f\"$LEAN_PATH: {lean_path}\")\n", - "server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)" + "server = Server(imports=['Example'], project_path=project_path)" ] }, { @@ -445,7 +440,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.4" + "version": "3.12.6" } }, "nbformat": 4, diff --git a/pantograph/server.py b/pantograph/server.py index da8fb72..db71c84 100644 --- a/pantograph/server.py +++ b/pantograph/server.py @@ -24,12 +24,28 @@ def _get_proc_cwd(): def _get_proc_path(): return _get_proc_cwd() / "pantograph-repl" -class TacticFailure(Exception): - pass -class ServerError(Exception): - pass +def get_lean_path(project_path): + """ + Extracts the `LEAN_PATH` variable from a project path. + """ + 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): @@ -185,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"]) @@ -195,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"]) @@ -219,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 = [ From 817d7087505c20765c9cf30aa63ccd1ff35df715 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 20 Oct 2024 19:29:27 -0700 Subject: [PATCH 13/13] fix: Disable notebook execution --- docs/_config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/_config.yml b/docs/_config.yml index 43746c3..0c52107 100644 --- a/docs/_config.yml +++ b/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: