feat: Example Jupyter notebook
This commit is contained in:
parent
c9cc0ff2e2
commit
695374a3e4
GPG Key ID:
4D9B1C8D10EA4C50
|
|
@ -22,3 +22,6 @@ python -m pantograph.server
|
|||
```
|
||||
The tests in `pantograph/server.py` also serve as simple interaction examples
|
||||
|
||||
## Examples
|
||||
|
||||
See `examples/README.md`
|
||||
|
|
|
|||
|
|
@ -1,4 +1,9 @@
|
|||
# Usage Example
|
||||
# Examples
|
||||
|
||||
For a quick introduction of the API, fire up Jupyter and open `all.ipynb`.
|
||||
``` sh
|
||||
poetry run jupyter notebook
|
||||
```
|
||||
|
||||
This example showcases how to bind library dependencies and execute the `Aesop`
|
||||
tactic in Lean. First build the example project:
|
||||
|
|
|
|||
|
|
@ -0,0 +1,420 @@
|
|||
{
|
||||
"cells": [
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "a1078f98-fcaf-4cda-8ad4-3cbab44f114b",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"# Pantograph Example\n",
|
||||
"\n",
|
||||
"The only interface for interacting with Pantograph is the `Server` class. It can be used either standalone (with no Lean project specified) or in a Lean project in order to access the project's symbols.\n",
|
||||
"\n",
|
||||
"The server's `imports` argument must be specified as a list of Lean modules to import. With no import statements, there are no symbols available and no useful work can be done. By default, `imports` is `[\"Init\"]`."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 2,
|
||||
"id": "101f4591-ec31-4000-96a6-ac3fc3dd0fa2",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"from pantograph import Server\n",
|
||||
"\n",
|
||||
"server = Server()"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "1fbdb837-740e-44ef-a7e9-c40f79584639",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"We can initialize a proof by providing the target statement."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 3,
|
||||
"id": "4affc375-360b-40cf-8d22-4fdcc12dba0d",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"state0 = server.goal_start(\"forall (p : Prop), p -> p\")"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "deb7994a-273f-4b52-be2d-e1086d4c1d55",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"This invocation creates a *goal state*, which consists of a finite number of goals. "
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 6,
|
||||
"id": "29f7ae15-7f69-4740-a6fa-71fbb1ccabd8",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"GoalState(state_id=0, goals=[Goal(variables=[], target='forall (p : Prop), p -> p', name=None, is_conversion=False)], _sentinel=[])"
|
||||
]
|
||||
},
|
||||
"execution_count": 6,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"state0"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "274f50da-85c1-445e-bf9f-cb716f66e36f",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Execute tactics on the goal state via `Server.goal_tactic`:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 8,
|
||||
"id": "bfbd5512-fcb0-428d-8131-4da4005e743c",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"GoalState(state_id=2, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p✝')], target='p✝ → p✝', name=None, is_conversion=False)], _sentinel=[1])"
|
||||
]
|
||||
},
|
||||
"execution_count": 8,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"state1 = server.goal_tactic(state0, goal_id=0, tactic=\"intro\")\n",
|
||||
"state1"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "1c1c5ab4-5518-40b0-8a2f-50e095a3702a",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Recover the usual string form of a goal by the `str` function:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 9,
|
||||
"id": "2d18d6dc-7936-4bb6-b47d-f781dd8ddacd",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"'p✝ : Prop\\n⊢ p✝ → p✝'"
|
||||
]
|
||||
},
|
||||
"execution_count": 9,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"str(state1.goals[0])"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "fc560b88-0222-4e40-bff9-37ab70af075e",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"When a tactic fails, it throws an exception:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 12,
|
||||
"id": "a0fdd3b3-9b38-4602-84a3-89065822f6e8",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"[\"tactic 'assumption' failed\\np✝ : Prop\\n⊢ p✝ → p✝\"]\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": "c801bbb4-9248-4f75-945b-1dd665bb08d1",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"A state with no goals is considered solved"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 15,
|
||||
"id": "9d18045a-9734-415c-8f40-7aadb6cb18f4",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"GoalState(state_id=7, goals=[], _sentinel=[1, 3, 4, 5])"
|
||||
]
|
||||
},
|
||||
"execution_count": 15,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"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": "aa5a2800-cae3-48df-b746-d19a8d84eaf5",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Execute `Server.gc()` to clean up unused goals once in a while"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 16,
|
||||
"id": "ee98de99-3cfc-4449-8d62-00e8eaee03db",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"server.gc()"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "78cfb9ac-c5ec-4901-97a5-4d19e6b8ecbb",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Loading Projects\n",
|
||||
"\n",
|
||||
"Pantograph would not be useful if it could not load symbols from other projects. In `examples/Example` is a standard Lean 4 project, with its toolchain version precisely equal to the toolchain version of Pantograph. Executing `lake new PROJECT_NAME` or `lake init` in an empty folder initializes a project according to this specification. To use a project in Pantograph, compile the project by running `lake build` in its root directory. This sets up output folders and builds the binary Lean files.\n",
|
||||
"\n",
|
||||
"Load the example project by providing `project_path` and `lean_path` to `Server`:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 19,
|
||||
"id": "ecf5d9d3-e53e-4f67-969e-d38e3d97c65e",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"$PWD: /Users/aniva/Projects/atp/PyPantograph/examples/Example\n",
|
||||
"$LEAN_PATH: b'././.lake/packages/std/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/build/lib:/Users/aniva/.elan/toolchains/leanprover--lean4---v4.8.0-rc1/lib/lean\\n'\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"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",
|
||||
"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)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "67123741-3d23-4077-98ab-91110b4e39f1",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"With the project loaded, all dependencies of the project, be it Mathlib or Aesop, are now available."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 20,
|
||||
"id": "bf485778-baa9-4c1c-80fa-960f9cf9bc8a",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"True"
|
||||
]
|
||||
},
|
||||
"execution_count": 20,
|
||||
"metadata": {},
|
||||
"output_type": "execute_result"
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"state0 = server.goal_start(\"forall (p q: Prop), Or p q -> Or q p\")\n",
|
||||
"state1 = server.goal_tactic(state0, goal_id=0, tactic=\"aesop\")\n",
|
||||
"state1.is_solved"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "8c3f9d90-bacc-4cba-95a4-23cc31a58a4f",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Reading Symbols\n",
|
||||
"\n",
|
||||
"Pantograph can also query proof states from a project by directly calling into Lean's compiler internals. Run the Lean compiler on a project module via `Server.compile_unit`."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 21,
|
||||
"id": "8ff6007b-50df-4449-9a86-6d3eb0bc0caa",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"==== #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",
|
||||
"==== #2 ====\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": [
|
||||
"units, invocations = server.compile_unit(\"Example\")\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": "cb5bbbcc-01dc-4a35-81ba-e155cedb9a91",
|
||||
"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.4"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
"nbformat_minor": 5
|
||||
}
|
||||
|
|
@ -0,0 +1 @@
|
|||
from pantograph.server import Server
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -14,6 +14,9 @@ pexpect = "^4.9.0"
|
|||
generate-setup-file = false
|
||||
script = "build.py"
|
||||
|
||||
[tool.poetry.group.dev.dependencies]
|
||||
notebook = "^7.2.1"
|
||||
|
||||
[build-system]
|
||||
requires = ["poetry-core"]
|
||||
build-backend = "poetry.core.masonry.api"
|
||||
|
|
|
|||
Loading…
Reference in New Issue