From 7a2278cb7009e39d8c6d7400d5b2aea003f90a3b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 20 Oct 2024 19:22:35 -0700 Subject: [PATCH] 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 | 35 ++++- 12 files changed, 858 insertions(+), 63 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" +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 + class TacticFailure(Exception): - pass + """ + Indicates a tactic failed to execute + """ class ServerError(Exception): - pass + """ + Indicates a logical error in the server. + """ -DEFAULT_CORE_OPTIONS=["maxHeartbeats=0", "maxRecDepth=100000"] + +DEFAULT_CORE_OPTIONS = ["maxHeartbeats=0", "maxRecDepth=100000"] class Server: @@ -54,6 +70,8 @@ def __init__(self, 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 @@ def __init__(self, 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 @@ def goal_tactic(self, state: GoalState, goal_id: int, tactic: Tactic) -> GoalSta 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 @@ def goal_conv_begin(self, state: GoalState, goal_id: int) -> GoalState: 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 @@ def tactic_invocations(self, file_name: Union[str, Path]) -> tuple[list[str], li 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 = [