Merge branch 'main' into dev
This commit is contained in:
commit
69b01d3879
GPG Key ID:
4D9B1C8D10EA4C50
|
|
@ -7,3 +7,4 @@
|
||||||
|
|
||||||
# Output
|
# Output
|
||||||
/dist
|
/dist
|
||||||
|
/venv
|
||||||
|
|
|
||||||
|
|
@ -1,3 +1,4 @@
|
||||||
[submodule "src"]
|
[submodule "src"]
|
||||||
path = src
|
path = src
|
||||||
url = https://git.leni.sh/aniva/Pantograph.git
|
url = https://git.leni.sh/aniva/Pantograph.git
|
||||||
|
|
||||||
11
README.md
11
README.md
|
|
@ -3,6 +3,14 @@
|
||||||
Python interface to the Pantograph library
|
Python interface to the Pantograph library
|
||||||
|
|
||||||
## Getting started
|
## Getting started
|
||||||
|
Update submodule
|
||||||
|
``` bash
|
||||||
|
git submodule update --init
|
||||||
|
```
|
||||||
|
Install dependencies
|
||||||
|
```bash
|
||||||
|
poetry install
|
||||||
|
```
|
||||||
|
|
||||||
Execute
|
Execute
|
||||||
```bash
|
```bash
|
||||||
|
|
@ -14,3 +22,6 @@ python -m pantograph.server
|
||||||
```
|
```
|
||||||
The tests in `pantograph/server.py` also serve as simple interaction examples
|
The tests in `pantograph/server.py` also serve as simple interaction examples
|
||||||
|
|
||||||
|
## Examples
|
||||||
|
|
||||||
|
See `examples/README.md`
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,14 @@
|
||||||
import Aesop
|
import Aesop
|
||||||
|
|
||||||
-- Ensure that Aesop is running
|
/-- Ensure that Aesop is running -/
|
||||||
example : α → α :=
|
example : α → α :=
|
||||||
by aesop
|
by aesop
|
||||||
|
|
||||||
|
example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
|
||||||
|
intro p q h
|
||||||
|
-- Here are some comments
|
||||||
|
cases h
|
||||||
|
. apply Or.inr
|
||||||
|
assumption
|
||||||
|
. apply Or.inl
|
||||||
|
assumption
|
||||||
|
|
|
||||||
|
|
@ -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`
|
This example showcases how to bind library dependencies and execute the `Aesop`
|
||||||
tactic in Lean. First build the example project:
|
tactic in Lean. First build the example project:
|
||||||
|
|
@ -7,9 +12,12 @@ pushd Example
|
||||||
lake build
|
lake build
|
||||||
popd
|
popd
|
||||||
```
|
```
|
||||||
This would generate compiled `.olean` files. Then run the example from the
|
This would generate compiled `.olean` files. Then run one of the examples from the
|
||||||
project root:
|
project root:
|
||||||
``` sh
|
``` sh
|
||||||
poetry run examples/aesop.py
|
poetry run examples/aesop.py
|
||||||
|
poetry run examples/data.py
|
||||||
```
|
```
|
||||||
|
|
||||||
|
Warning: If you make modifications to any Lean files, you must re-run `lake build`!
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -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,23 @@
|
||||||
|
#!/usr/bin/env python3
|
||||||
|
|
||||||
|
import subprocess
|
||||||
|
from pathlib import Path
|
||||||
|
from pantograph.server import Server
|
||||||
|
|
||||||
|
def get_project_and_lean_path():
|
||||||
|
cwd = Path(__file__).parent.resolve() / 'Example'
|
||||||
|
p = subprocess.check_output(['lake', 'env', 'printenv', 'LEAN_PATH'], cwd=cwd)
|
||||||
|
return cwd, p
|
||||||
|
|
||||||
|
if __name__ == '__main__':
|
||||||
|
project_path, lean_path = get_project_and_lean_path()
|
||||||
|
print(f"$PWD: {project_path}")
|
||||||
|
print(f"$LEAN_PATH: {lean_path}")
|
||||||
|
server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)
|
||||||
|
units, invocations = server.compile_unit("Example")
|
||||||
|
for i, u in enumerate(units):
|
||||||
|
print(f"==== #{i} ====")
|
||||||
|
print(u)
|
||||||
|
print("==== Invocations ====")
|
||||||
|
for i in invocations:
|
||||||
|
print(f"{i.before}\n{i.tactic}\n{i.after}\n")
|
||||||
|
|
@ -0,0 +1 @@
|
||||||
|
from pantograph.server import Server
|
||||||
|
|
@ -0,0 +1,13 @@
|
||||||
|
from dataclasses import dataclass
|
||||||
|
|
||||||
|
@dataclass(frozen=True)
|
||||||
|
class TacticInvocation:
|
||||||
|
before: str
|
||||||
|
after: str
|
||||||
|
tactic: str
|
||||||
|
|
||||||
|
@staticmethod
|
||||||
|
def parse(payload: dict):
|
||||||
|
return TacticInvocation(before=payload["goalBefore"],
|
||||||
|
after=payload["goalAfter"],
|
||||||
|
tactic=payload["tactic"])
|
||||||
|
|
@ -2,7 +2,7 @@
|
||||||
Data structuers for expressions and goals
|
Data structuers for expressions and goals
|
||||||
"""
|
"""
|
||||||
from dataclasses import dataclass
|
from dataclasses import dataclass
|
||||||
from typing import Optional, Self, Union
|
from typing import Optional, Union
|
||||||
|
|
||||||
Expr = str
|
Expr = str
|
||||||
|
|
||||||
|
|
@ -16,7 +16,7 @@ class Variable:
|
||||||
name: Optional[str] = None
|
name: Optional[str] = None
|
||||||
|
|
||||||
@staticmethod
|
@staticmethod
|
||||||
def parse(payload: dict) -> Self:
|
def parse(payload: dict):
|
||||||
name = payload.get("userName")
|
name = payload.get("userName")
|
||||||
t = parse_expr(payload["type"])
|
t = parse_expr(payload["type"])
|
||||||
v = payload.get("value")
|
v = payload.get("value")
|
||||||
|
|
@ -39,11 +39,11 @@ class Goal:
|
||||||
is_conversion: bool = False
|
is_conversion: bool = False
|
||||||
|
|
||||||
@staticmethod
|
@staticmethod
|
||||||
def sentence(target: Expr) -> Self:
|
def sentence(target: Expr):
|
||||||
return Goal(variables=[], target=target)
|
return Goal(variables=[], target=target)
|
||||||
|
|
||||||
@staticmethod
|
@staticmethod
|
||||||
def parse(payload: dict) -> Self:
|
def parse(payload: dict):
|
||||||
name = payload.get("userName")
|
name = payload.get("userName")
|
||||||
variables = [Variable.parse(v) for v in payload["vars"]]
|
variables = [Variable.parse(v) for v in payload["vars"]]
|
||||||
target = parse_expr(payload["target"])
|
target = parse_expr(payload["target"])
|
||||||
|
|
@ -73,7 +73,7 @@ class GoalState:
|
||||||
return not self.goals
|
return not self.goals
|
||||||
|
|
||||||
@staticmethod
|
@staticmethod
|
||||||
def parse(payload: dict, _sentinel: list[int]) -> Self:
|
def parse(payload: dict, _sentinel: list[int]):
|
||||||
state_id = payload["nextStateId"]
|
state_id = payload["nextStateId"]
|
||||||
goals = [Goal.parse(g) for g in payload["goals"]]
|
goals = [Goal.parse(g) for g in payload["goals"]]
|
||||||
return GoalState(state_id, goals, _sentinel)
|
return GoalState(state_id, goals, _sentinel)
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,231 @@
|
||||||
|
from pantograph.server import Server, ServerError
|
||||||
|
from pantograph.expr import Variable, Goal, TacticCalc
|
||||||
|
import unittest
|
||||||
|
import sglang as sgl
|
||||||
|
|
||||||
|
LEAN4_INTRO = '''/-- A sequence `u` of real numbers converges to `l` if `∀ ε > 0, ∃ N, ∀ n ≥ N, |u_n - l| ≤ ε`.
|
||||||
|
This condition will be spelled `seq_limit u l`. -/
|
||||||
|
def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
|
||||||
|
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε
|
||||||
|
|
||||||
|
/- In the above definition, note that the `n`-th term of the sequence `u` is denoted
|
||||||
|
simply by `u n`.
|
||||||
|
|
||||||
|
Similarly, in the next definition, `f x` is what we would write `f(x)` on paper.
|
||||||
|
Also note that implication is denoted by a single arrow (we'll explain why later). -/
|
||||||
|
|
||||||
|
/-- A function`f : ℝ → ℝ` is continuous at `x₀` if
|
||||||
|
`∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ ⇒ |f(x) - f(x₀)| ≤ ε`.
|
||||||
|
This condition will be spelled `continuous_at f x₀`.-/
|
||||||
|
def continuous_at (f : ℝ → ℝ) (x₀ : ℝ) : Prop :=
|
||||||
|
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε
|
||||||
|
|
||||||
|
/-- Now we claim that if `f` is continuous at `x₀` then it is sequentially continuous
|
||||||
|
at `x₀`: for any sequence `u` converging to `x₀`, the sequence `f ∘ u` converges
|
||||||
|
to `f x₀`. -/
|
||||||
|
example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ) (hu : seq_limit u x₀) (hf : continuous_at f x₀) :
|
||||||
|
seq_limit (f ∘ u) (f x₀) := by { -- This `by` keyword marks the beginning of the proof
|
||||||
|
-- Put your text cursor here and watch the Lean InfoView panel to the right.
|
||||||
|
-- Then move your cursor from line to line in the proof while monitoring the Infoview.
|
||||||
|
|
||||||
|
-- Our goal is to prove that, for any positive `ε`, there exists a natural
|
||||||
|
-- number `N` such that, for any natural number `n` at least `N`,
|
||||||
|
-- `|f(u_n) - f(x₀)|` is at most `ε`.
|
||||||
|
unfold seq_limit
|
||||||
|
-- Fix a positive number `ε`.
|
||||||
|
intros ε hε
|
||||||
|
-- By assumption on `f` applied to this positive `ε`, we get a positive `δ`
|
||||||
|
-- such that, for all real number `x`, if `|x - x₀| ≤ δ` then `|f(x) - f(x₀)| ≤ ε` (1).
|
||||||
|
obtain ⟨δ, δ_pos, Hf⟩ : ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε := hf ε hε
|
||||||
|
-- The assumption on `u` applied to this `δ` gives a natural number `N` such that
|
||||||
|
-- for every natural number `n`, if `n ≥ N` then `|u_n - x₀| ≤ δ` (2).
|
||||||
|
obtain ⟨N, Hu⟩ : ∃ N, ∀ n ≥ N, |u n - x₀| ≤ δ := hu δ δ_pos
|
||||||
|
-- Let's prove `N` is suitable.
|
||||||
|
use N
|
||||||
|
-- Fix `n` which is at least `N`. Let's prove `|f(u_n) - f(x₀)| ≤ ε`.
|
||||||
|
intros n hn
|
||||||
|
-- Thanks to (1) applied to `u_n`, it suffices to prove that `|u_n - x₀| ≤ δ`.
|
||||||
|
apply Hf
|
||||||
|
-- This follows from property (2) and our assumption on `n`.
|
||||||
|
exact Hu n hn
|
||||||
|
-- This finishes the proof!
|
||||||
|
}
|
||||||
|
|
||||||
|
/-
|
||||||
|
Now that this proof is over, you can use the file explorer to the
|
||||||
|
left of this panel to open the file `Exercises > 01Rewriting.lean`.
|
||||||
|
-/'''
|
||||||
|
|
||||||
|
LEAN4_REWRITE = '''Rewrite tactic tutorial:
|
||||||
|
example (a b c : Nat) : a + b + c = a + c + b := by
|
||||||
|
rw [Nat.add_assoc, Nat.add_comm b, ← Nat.add_assoc]
|
||||||
|
|
||||||
|
example (a b c : Nat) : a + b + c = a + c + b := by
|
||||||
|
rw [Nat.add_assoc, Nat.add_assoc, Nat.add_comm b]
|
||||||
|
|
||||||
|
example (a b c : Nat) : a + b + c = a + c + b := by
|
||||||
|
rw [Nat.add_assoc, Nat.add_assoc, Nat.add_comm _ b]
|
||||||
|
|
||||||
|
example (f : Nat → Nat) (a : Nat) (h : a + 0 = 0) : f a = f 0 := by
|
||||||
|
rw [Nat.add_zero] at h
|
||||||
|
rw [h]
|
||||||
|
|
||||||
|
def Tuple (α : Type) (n : Nat) :=
|
||||||
|
{ as : List α // as.length = n }
|
||||||
|
|
||||||
|
example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := by
|
||||||
|
rw [h] at t
|
||||||
|
exact t
|
||||||
|
'''
|
||||||
|
|
||||||
|
@sgl.function
|
||||||
|
def multi_turn_question(s, question_1, question_2):
|
||||||
|
s += sgl.system("You are a helpful assistant.")
|
||||||
|
s += sgl.user(question_1)
|
||||||
|
s += sgl.assistant(sgl.gen("answer_1", max_tokens=256))
|
||||||
|
s += sgl.user(question_2)
|
||||||
|
s += sgl.assistant(sgl.gen("answer_2", max_tokens=256))
|
||||||
|
|
||||||
|
|
||||||
|
@sgl.function
|
||||||
|
def select_tactic(s, server, state, goal_id, feedback_turns = 5):
|
||||||
|
|
||||||
|
s += sgl.system("You are an expert in Lean. Choose the next one tactic to run given the current proof state and goals.")
|
||||||
|
s += sgl.user(LEAN4_REWRITE)
|
||||||
|
s += sgl.user("The current proof state: GoalState(state_id=0, goals=[Goal(variables=[], target='∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b', name=None, is_conversion=False)])")
|
||||||
|
s += sgl.assistant("```intros a b h```")
|
||||||
|
s += sgl.user("The current proof state: GoalState(state_id=1, goals=[Goal(variables=[Variable(t='Nat', v=None, name='a'), Variable(t='Nat', v=None, name='b'), Variable(t='b = 2', v=None, name='h')], target='1 + a + 1 = a + b', name=None, is_conversion=False)])")
|
||||||
|
s += sgl.assistant('TacticCalc("1 + a + 1 = a + 1 + 1")')
|
||||||
|
s += sgl.user("The current proof state: " + str(state))
|
||||||
|
for i in range(feedback_turns):
|
||||||
|
with s.copy() as tmp:
|
||||||
|
tmp += sgl.assistant(sgl.gen("tactic", max_tokens=64))
|
||||||
|
print("==tmp===")
|
||||||
|
print(tmp["tactic"])
|
||||||
|
tactic = extract_code_from_llm_output(tmp["tactic"])
|
||||||
|
s += sgl.assistant("```"+tactic+"```")
|
||||||
|
success, new_state = apply_tactic(server, state, goal_id, tactic)
|
||||||
|
if not success:
|
||||||
|
with s.user():
|
||||||
|
s += "This answer got Lean compile error:\n" + str(new_state) + "\n"
|
||||||
|
s += "Please try again by taking the Lean compiler feedback."
|
||||||
|
|
||||||
|
else:
|
||||||
|
return new_state
|
||||||
|
|
||||||
|
def apply_tactic(server, state, goal_id, tactic):
|
||||||
|
try:
|
||||||
|
new_state = server.goal_tactic(state, goal_id=goal_id, tactic=tactic)
|
||||||
|
except ServerError as e:
|
||||||
|
return False, e
|
||||||
|
return True, new_state
|
||||||
|
|
||||||
|
def extract_code_from_llm_output(reply):
|
||||||
|
i = reply.find("```lean")
|
||||||
|
if i != -1:
|
||||||
|
reply = reply[i + 7:]
|
||||||
|
i = reply.find("```")
|
||||||
|
reply = reply[:i]
|
||||||
|
return reply
|
||||||
|
i = reply.find("```")
|
||||||
|
if i != -1:
|
||||||
|
reply = reply[i + 3:]
|
||||||
|
i = reply.find("```")
|
||||||
|
reply = reply[:i]
|
||||||
|
return reply
|
||||||
|
return reply
|
||||||
|
|
||||||
|
class TestServerSGL(unittest.TestCase):
|
||||||
|
|
||||||
|
def test_conv_calc_sgl(self):
|
||||||
|
n_trails = 5
|
||||||
|
sgl.set_default_backend(sgl.OpenAI("gpt-4"))
|
||||||
|
|
||||||
|
server = Server()
|
||||||
|
state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
|
||||||
|
print("==========state0============")
|
||||||
|
print(state0)
|
||||||
|
variables = [
|
||||||
|
Variable(name="a", t="Nat"),
|
||||||
|
Variable(name="b", t="Nat"),
|
||||||
|
Variable(name="h", t="b = 2"),
|
||||||
|
]
|
||||||
|
|
||||||
|
state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a b h")
|
||||||
|
print("==========state1============")
|
||||||
|
print(state1)
|
||||||
|
state2 = server.goal_tactic(state1, goal_id=0, tactic=TacticCalc("1 + a + 1 = a + 1 + 1"))
|
||||||
|
print("==========state2============")
|
||||||
|
print(state2)
|
||||||
|
self.assertEqual(state2.goals, [
|
||||||
|
Goal(
|
||||||
|
variables,
|
||||||
|
target="1 + a + 1 = a + 1 + 1",
|
||||||
|
name='calc',
|
||||||
|
),
|
||||||
|
Goal(
|
||||||
|
variables,
|
||||||
|
target="a + 1 + 1 = a + b",
|
||||||
|
),
|
||||||
|
])
|
||||||
|
state3 = None
|
||||||
|
for i in range(n_trails):
|
||||||
|
print(f"===============trail {str(i)}============")
|
||||||
|
try:
|
||||||
|
state = select_tactic.run(server, state2, goal_id = 1)
|
||||||
|
state3 = state.ret_value
|
||||||
|
for m in state.messages():
|
||||||
|
print(m["role"], ":", m["content"])
|
||||||
|
|
||||||
|
print("\n-- new state --\n", state3)
|
||||||
|
break
|
||||||
|
|
||||||
|
except ServerError as e:
|
||||||
|
print(f"server error: {e}")
|
||||||
|
continue
|
||||||
|
state3 = server.goal_tactic(state2, goal_id=1, tactic=TacticCalc("_ = a + 2"))
|
||||||
|
|
||||||
|
|
||||||
|
print("==========state3============")
|
||||||
|
print(state3)
|
||||||
|
state4 = None
|
||||||
|
for i in range(n_trails):
|
||||||
|
print(f"===============trail {str(i)}============")
|
||||||
|
try:
|
||||||
|
state = select_tactic.run(server, state3, goal_id = 0)
|
||||||
|
state4 = state.ret_value
|
||||||
|
for m in state.messages():
|
||||||
|
print(m["role"], ":", m["content"])
|
||||||
|
|
||||||
|
print("\n-- new state --\n", state4)
|
||||||
|
break
|
||||||
|
|
||||||
|
except ServerError as e:
|
||||||
|
print(f"server error: {e}")
|
||||||
|
continue
|
||||||
|
|
||||||
|
state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
|
||||||
|
print("==========state4============")
|
||||||
|
print(state4)
|
||||||
|
self.assertTrue(state4.is_solved)
|
||||||
|
|
||||||
|
|
||||||
|
def test_sglang_openai(self):
|
||||||
|
sgl.set_default_backend(sgl.OpenAI("gpt-4"))
|
||||||
|
|
||||||
|
print('\n----- Test sglang ---')
|
||||||
|
state = multi_turn_question.run(
|
||||||
|
question_1="What is the capital of the United States?",
|
||||||
|
question_2="List two local attractions.",
|
||||||
|
)
|
||||||
|
|
||||||
|
for m in state.messages():
|
||||||
|
print(m["role"], ":", m["content"])
|
||||||
|
|
||||||
|
print("\n-- answer_1 --\n", state["answer_1"])
|
||||||
|
|
||||||
|
|
||||||
|
if __name__ == '__main__':
|
||||||
|
|
||||||
|
unittest.main()
|
||||||
|
|
||||||
|
|
@ -5,6 +5,7 @@ interface.
|
||||||
import json, pexpect, pathlib, unittest, os
|
import json, pexpect, pathlib, unittest, os
|
||||||
from pantograph.expr import parse_expr, Expr, Variable, Goal, GoalState, \
|
from pantograph.expr import parse_expr, Expr, Variable, Goal, GoalState, \
|
||||||
Tactic, TacticHave, TacticCalc
|
Tactic, TacticHave, TacticCalc
|
||||||
|
from pantograph.compiler import TacticInvocation
|
||||||
|
|
||||||
def _get_proc_cwd():
|
def _get_proc_cwd():
|
||||||
return pathlib.Path(__file__).parent
|
return pathlib.Path(__file__).parent
|
||||||
|
|
@ -145,6 +146,24 @@ class Server:
|
||||||
raise ServerError(result["parseError"])
|
raise ServerError(result["parseError"])
|
||||||
return GoalState.parse(result, self.to_remove_goal_states)
|
return GoalState.parse(result, self.to_remove_goal_states)
|
||||||
|
|
||||||
|
def compile_unit(self, module: str) -> tuple[list[str], list[TacticInvocation]]:
|
||||||
|
file_path = self.project_path / (module.replace('.', '/') + '.lean')
|
||||||
|
result = self.run('compile.unit', {
|
||||||
|
'module': module,
|
||||||
|
'compilationUnits': True,
|
||||||
|
'invocations': True
|
||||||
|
})
|
||||||
|
if "error" in result:
|
||||||
|
raise ServerError(result["desc"])
|
||||||
|
|
||||||
|
with open(file_path, 'rb') as f:
|
||||||
|
content = f.read()
|
||||||
|
units = [content[begin:end].decode('utf-8') for begin,end in result['units']]
|
||||||
|
|
||||||
|
invocations = [TacticInvocation.parse(i) for i in result['invocations']]
|
||||||
|
return units, invocations
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
def get_version():
|
def get_version():
|
||||||
import subprocess
|
import subprocess
|
||||||
|
|
|
||||||
File diff suppressed because it is too large
Load Diff
|
|
@ -7,13 +7,16 @@ license = "GPL-3"
|
||||||
readme = "README.md"
|
readme = "README.md"
|
||||||
|
|
||||||
[tool.poetry.dependencies]
|
[tool.poetry.dependencies]
|
||||||
python = "^3.11"
|
python = "^3.10"
|
||||||
pexpect = "^4.9.0"
|
pexpect = "^4.9.0"
|
||||||
|
|
||||||
[tool.poetry.build]
|
[tool.poetry.build]
|
||||||
generate-setup-file = false
|
generate-setup-file = false
|
||||||
script = "build.py"
|
script = "build.py"
|
||||||
|
|
||||||
|
[tool.poetry.group.dev.dependencies]
|
||||||
|
notebook = "^7.2.1"
|
||||||
|
|
||||||
[build-system]
|
[build-system]
|
||||||
requires = ["poetry-core"]
|
requires = ["poetry-core"]
|
||||||
build-backend = "poetry.core.masonry.api"
|
build-backend = "poetry.core.masonry.api"
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue