Merge pull request #50 from lenianiva/misc/version
chore: Update to 0.2.23
This commit is contained in:
Leni Aniva
GitHub
commit
4badb8adab
|
|
@ -20,7 +20,8 @@ poetry install
|
|||
|
||||
Build the documentations by
|
||||
```sh
|
||||
jupyter-book build docs
|
||||
poetry install --only doc
|
||||
poetry run jupyter-book build docs
|
||||
```
|
||||
Then serve
|
||||
```sh
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
Data
|
||||
=============
|
||||
|
||||
.. automodule:: pantograph.compiler
|
||||
.. automodule:: pantograph.data
|
||||
:members:
|
||||
|
|
|
|||
|
|
@ -53,7 +53,7 @@
|
|||
"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\")"
|
||||
"units = server.tactic_invocations(project_path / \"Example.lean\")"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -61,7 +61,7 @@
|
|||
"id": "c3c1be91-27a5-4481-b09d-a32dbb94b058",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"The function returns a tuple `([str], [TacticInvocation])`. The former element is a list of strings containing each compilation unit, comment data included."
|
||||
"The function returns a list of `CompilationUnit` objects, corresponding to each compilation unit in the input Lean file. For performance reasons only the text boundaries are loaded into `CompilationUnit`s."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -74,13 +74,13 @@
|
|||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"==== #0 ====\n",
|
||||
"#0: [14,85]\n",
|
||||
"/-- Ensure that Aesop is running -/\n",
|
||||
"example : α → α :=\n",
|
||||
" by aesop\n",
|
||||
"\n",
|
||||
"\n",
|
||||
"==== #1 ====\n",
|
||||
"#1: [85,254]\n",
|
||||
"example : ∀ (p q: Prop), p ∨ q → q ∨ p := by\n",
|
||||
" intro p q h\n",
|
||||
" -- Here are some comments\n",
|
||||
|
|
@ -94,9 +94,12 @@
|
|||
}
|
||||
],
|
||||
"source": [
|
||||
"for i, u in enumerate(units):\n",
|
||||
" print(f\"==== #{i} ====\")\n",
|
||||
" print(u)"
|
||||
"with open(project_path / \"Example.lean\", 'rb') as f:\n",
|
||||
" content = f.read()\n",
|
||||
" for i, unit in enumerate(units):\n",
|
||||
" print(f\"#{i}: [{unit.i_begin},{unit.i_end}]\")\n",
|
||||
" unit_text = content[unit.i_begin:unit.i_end].decode('utf-8')\n",
|
||||
" print(unit_text)"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -104,7 +107,7 @@
|
|||
"id": "52e650fc-4a87-445f-8aa8-707ed9e36c03",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"The latter is a list of `TacticInvocation`, which contains the `.before` (corresponding to the state before the tactic), `.after` (corresponding to the state after the tactic), and `.tactic` (tactic executed) fields. "
|
||||
"Each `CompilationUnit` includes a list of `TacticInvocation`s, which contains the `.before` (corresponding to the state before the tactic), `.after` (corresponding to the state after the tactic), and `.tactic` (tactic executed) fields. "
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -122,13 +125,33 @@
|
|||
"⊢ α → α\n",
|
||||
"[Tactic]\n",
|
||||
"aesop (using [])\n",
|
||||
"[Afte]\n",
|
||||
"\n",
|
||||
"[After]\n",
|
||||
"\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"for i in units[0].invocations:\n",
|
||||
" print(f\"[Before]\\n{i.before}\")\n",
|
||||
" print(f\"[Tactic]\\n{i.tactic} (using {i.used_constants})\")\n",
|
||||
" print(f\"[After]\\n{i.after}\")"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 5,
|
||||
"id": "51f5398b-5416-4dc1-81cd-6d2514758232",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"[Before]\n",
|
||||
"⊢ ∀ (p q : Prop), p ∨ q → q ∨ p\n",
|
||||
"[Tactic]\n",
|
||||
"intro p q h (using [])\n",
|
||||
"[Afte]\n",
|
||||
"[After]\n",
|
||||
"p q : Prop\n",
|
||||
"h : p ∨ q\n",
|
||||
"⊢ q ∨ p\n",
|
||||
|
|
@ -138,7 +161,7 @@
|
|||
"⊢ q ∨ p\n",
|
||||
"[Tactic]\n",
|
||||
"cases h (using ['Eq.refl', 'Or'])\n",
|
||||
"[Afte]\n",
|
||||
"[After]\n",
|
||||
"case inl\n",
|
||||
"p q : Prop\n",
|
||||
"h✝ : p\n",
|
||||
|
|
@ -151,7 +174,7 @@
|
|||
"⊢ q ∨ p\n",
|
||||
"[Tactic]\n",
|
||||
"apply Or.inr (using ['Or.inr'])\n",
|
||||
"[Afte]\n",
|
||||
"[After]\n",
|
||||
"case inl.h\n",
|
||||
"p q : Prop\n",
|
||||
"h✝ : p\n",
|
||||
|
|
@ -163,7 +186,7 @@
|
|||
"⊢ p\n",
|
||||
"[Tactic]\n",
|
||||
"assumption (using [])\n",
|
||||
"[Afte]\n",
|
||||
"[After]\n",
|
||||
"\n",
|
||||
"[Before]\n",
|
||||
"case inr\n",
|
||||
|
|
@ -172,7 +195,7 @@
|
|||
"⊢ q ∨ p\n",
|
||||
"[Tactic]\n",
|
||||
"apply Or.inl (using ['Or.inl'])\n",
|
||||
"[Afte]\n",
|
||||
"[After]\n",
|
||||
"case inr.h\n",
|
||||
"p q : Prop\n",
|
||||
"h✝ : q\n",
|
||||
|
|
@ -184,25 +207,17 @@
|
|||
"⊢ q\n",
|
||||
"[Tactic]\n",
|
||||
"assumption (using [])\n",
|
||||
"[Afte]\n",
|
||||
"[After]\n",
|
||||
"\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"for i in invocations:\n",
|
||||
"for i in units[1].invocations:\n",
|
||||
" print(f\"[Before]\\n{i.before}\")\n",
|
||||
" print(f\"[Tactic]\\n{i.tactic} (using {i.used_constants})\")\n",
|
||||
" print(f\"[Afte]\\n{i.after}\")"
|
||||
" print(f\"[After]\\n{i.after}\")"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "51f5398b-5416-4dc1-81cd-6d2514758232",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": []
|
||||
}
|
||||
],
|
||||
"metadata": {
|
||||
|
|
@ -221,7 +236,7 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.12.6"
|
||||
"version": "3.12.7"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@
|
|||
"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",
|
||||
"can replace an expression with `sorry`, and the `sorry` will become a goal. Any type errors will also become goals. In order to detect whether type errors have occurred, the user can look at the messages from each compilation unit.\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",
|
||||
|
|
@ -120,8 +120,8 @@
|
|||
"\"\"\"\n",
|
||||
"\n",
|
||||
"server = Server()\n",
|
||||
"state0, = server.load_sorry(sketch)\n",
|
||||
"print(state0)"
|
||||
"unit, = server.load_sorry(sketch)\n",
|
||||
"print(unit.goal_state)"
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -157,7 +157,7 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.12.6"
|
||||
"version": "3.12.7"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
|
|
|
|||
|
|
@ -214,7 +214,9 @@
|
|||
"\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`"
|
||||
"`TacticCalc` instance and feed it into `server.goal_tactic`.\n",
|
||||
"\n",
|
||||
"Technically speaking `have` and `let` are not tactics in Lean, so their execution requires special attention."
|
||||
]
|
||||
},
|
||||
{
|
||||
|
|
@ -307,7 +309,7 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.12.6"
|
||||
"version": "3.12.7"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
|
|
|
|||
|
|
@ -23,6 +23,38 @@ Almost all of Pantograph's business logic is written in Lean, and Pantograph
|
|||
achieves tighter coupling between the data extraction and proof search
|
||||
components.
|
||||
|
||||
## Caveats and Limitations
|
||||
|
||||
Pantograph does not exactly mimic Lean LSP's behaviour. That would not grant the
|
||||
flexibility it offers. To support tree search means Pantograph has to act
|
||||
differently from Lean in some times, but never at the sacrifice of soundness.
|
||||
|
||||
- When Lean LSP says "don't know how to synthesize placeholder", this indicates
|
||||
the human operator needs to manually move the cursor to the placeholder and
|
||||
type in the correct expression. This error therefore should not halt the proof
|
||||
process, and the placeholder should be turned into a goal.
|
||||
- When Lean LSP says "unresolved goals", that means a proof cannot finish where
|
||||
it is supposed to finish at the end of a `by` block. Pantograph will raise the
|
||||
error in this case, since it indicates the termination of a proof search branch.
|
||||
- `pick_goal` or `swap` will not work since they run contrary to tree search
|
||||
paradigms. However, if there are tactics which perform non-trivial operations
|
||||
to multiple goals at the same time, this constrain could potentially be
|
||||
relaxed at a cost of great bookkeeping overhead to the user.
|
||||
|
||||
Pantograph cannot perform things that are inherently constrained by Lean. These
|
||||
include:
|
||||
|
||||
- If a tactic loses track of metavariables, it will not be caught until the end
|
||||
of the proof search. This is a bug in the tactic itself.
|
||||
- Timeouts for executing tactics is not available. Maybe this will change in the
|
||||
future.
|
||||
- Interceptions of parsing errors generally cannot be turned into goals (e.g.
|
||||
`def mystery : Nat := :=`) due to Lean's parsing system.
|
||||
|
||||
Each Pantograph version is anchored to a Lean version specified in
|
||||
`src/lean-toolchain`. Features can be backported to older Lean versions upon
|
||||
request.
|
||||
|
||||
## Referencing
|
||||
|
||||
[Paper Link](https://arxiv.org/abs/2410.16429)
|
||||
|
|
|
|||
|
|
@ -1,448 +0,0 @@
|
|||
{
|
||||
"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 (e.g. Mathlib).\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": 1,
|
||||
"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": 2,
|
||||
"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": 3,
|
||||
"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": 3,
|
||||
"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": 4,
|
||||
"id": "bfbd5512-fcb0-428d-8131-4da4005e743c",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"GoalState(state_id=1, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p✝')], target='p✝ → p✝', name=None, is_conversion=False)], _sentinel=[])"
|
||||
]
|
||||
},
|
||||
"execution_count": 4,
|
||||
"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": 5,
|
||||
"id": "2d18d6dc-7936-4bb6-b47d-f781dd8ddacd",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"'p✝ : Prop\\n⊢ p✝ → p✝'"
|
||||
]
|
||||
},
|
||||
"execution_count": 5,
|
||||
"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": 6,
|
||||
"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": 7,
|
||||
"id": "9d18045a-9734-415c-8f40-7aadb6cb18f4",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"GoalState(state_id=3, goals=[], _sentinel=[])"
|
||||
]
|
||||
},
|
||||
"execution_count": 7,
|
||||
"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": 8,
|
||||
"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": 9,
|
||||
"id": "ecf5d9d3-e53e-4f67-969e-d38e3d97c65e",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example\n",
|
||||
"$LEAN_PATH: b'././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/build/lib:/home/aniva/.elan/toolchains/leanprover--lean4---v4.12/lib/lean\\n'\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"import subprocess, os\n",
|
||||
"from pathlib import Path\n",
|
||||
"project_path = Path(os.getcwd()).resolve() / 'Example'\n",
|
||||
"print(f\"$PWD: {project_path}\")\n",
|
||||
"server = Server(imports=['Example'], project_path=project_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": 10,
|
||||
"id": "bf485778-baa9-4c1c-80fa-960f9cf9bc8a",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"data": {
|
||||
"text/plain": [
|
||||
"True"
|
||||
]
|
||||
},
|
||||
"execution_count": 10,
|
||||
"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 Lean file via `Server.tactic_invocations`. Feeding in the absolute path is preferred."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 11,
|
||||
"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",
|
||||
"==== 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.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": "markdown",
|
||||
"id": "8762b719-d13b-4714-84ff-48c44b18f364",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"### Loading a theorem for the agent to prove\n",
|
||||
"\n",
|
||||
"For this to work, write `sorry` in the place where you would like your agent to do work, for example\n",
|
||||
"```lean\n",
|
||||
"example : (p q: Prop): Or p q -> Or q p := sorry\n",
|
||||
"```\n",
|
||||
"Then use the `Server.load_sorry`. As long as you only have one statement in `command`, it will give you exactly one goal state. A command with no `sorry`s results in no goal states.\n",
|
||||
"\n",
|
||||
"Note: Since a syntactically incorrect command will not generate `sorry`s, they will be sliently ignored by the frontend. Check if this is the case if the function returns no goals."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 12,
|
||||
"id": "3c515d2b-6910-499e-953b-bc69dc0e0a57",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"GoalState(state_id=2, goals=[Goal(variables=[Variable(t='Prop', v=None, name='p'), Variable(t='Prop', v=None, name='q')], target='p ∨ q → q ∨ p', name=None, is_conversion=False)], _sentinel=[0])\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"state0, = server.load_sorry(\"example (p q: Prop): Or p q -> Or q p := sorry\")\n",
|
||||
"print(state0)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "50b90547-fcbf-419f-866e-a6ebcc925c5f",
|
||||
"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
|
||||
}
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
#!/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.tactic_invocations(project_path / "Example.lean")
|
||||
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")
|
||||
|
|
@ -32,5 +32,5 @@ theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by
|
|||
|
||||
if __name__ == '__main__':
|
||||
server = Server()
|
||||
state0, = server.load_sorry(sketch)
|
||||
print(state0)
|
||||
unit, = server.load_sorry(sketch)
|
||||
print(unit.goal_state)
|
||||
|
|
|
|||
|
|
@ -201,7 +201,7 @@ def step_prove(
|
|||
print(colored("Lean code:", "light_grey", attrs=["bold"]), lean_code)
|
||||
|
||||
try:
|
||||
states = server.load_sorry(lean_code)
|
||||
units = server.load_sorry(lean_code)
|
||||
except ServerError as e:
|
||||
msg = f"Encountered exception: {e}"
|
||||
print(colored(msg, "red"))
|
||||
|
|
@ -210,18 +210,18 @@ def step_prove(
|
|||
error=msg,
|
||||
)
|
||||
|
||||
if len(states) != 1:
|
||||
if len(units) != 1:
|
||||
print(colored("Model must output one compilation unit", "red"))
|
||||
return SketchParseFailure(
|
||||
sketch=fl_sketch,
|
||||
error="Model must output one compilation unit",
|
||||
)
|
||||
|
||||
state = states[0]
|
||||
state = units[0].goal_state
|
||||
|
||||
if isinstance(state, list) and len(state) > 0:
|
||||
if state is None:
|
||||
# This means `state` contains error messages
|
||||
msg = "\n".join(state)
|
||||
msg = "\n".join(units[0].messages)
|
||||
print(colored("Sketch failed:", "red"), msg)
|
||||
return SketchParseFailure(
|
||||
sketch=fl_sketch,
|
||||
|
|
@ -273,7 +273,7 @@ def single_proof_search_dsp_lean(
|
|||
try:
|
||||
server = server_func()
|
||||
except Exception as e:
|
||||
print(colored("Failed to create server: {e}", "red"))
|
||||
print(colored(f"Failed to create server: {e}", "red"))
|
||||
return DatumResult(
|
||||
name=str(datum),
|
||||
error=str(e),
|
||||
|
|
|
|||
|
|
@ -27,13 +27,14 @@ def try_test_data(server, agent, entry: dict, max_steps: int, max_trials_per_goa
|
|||
agent.informal_stmt = entry["informal_stmt"]
|
||||
agent.informal_proof = entry["informal_proof"]
|
||||
|
||||
goal_states = server.load_sorry(command)
|
||||
units = server.load_sorry(command)
|
||||
|
||||
if len(goal_states) != 1:
|
||||
if len(units) != 1:
|
||||
return None
|
||||
|
||||
goal_state, = goal_states
|
||||
if isinstance(goal_state, list):
|
||||
unit, = units
|
||||
goal_state = unit.goal_state
|
||||
if goal_state is None:
|
||||
return None
|
||||
try:
|
||||
return agent.search(
|
||||
|
|
|
|||
|
|
@ -1,21 +0,0 @@
|
|||
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
|
||||
used_constants: list[str]
|
||||
|
||||
@staticmethod
|
||||
def parse(payload: dict):
|
||||
return TacticInvocation(
|
||||
before=payload["goalBefore"],
|
||||
after=payload["goalAfter"],
|
||||
tactic=payload["tactic"],
|
||||
used_constants=payload.get('usedConstants', []),
|
||||
)
|
||||
|
|
@ -0,0 +1,71 @@
|
|||
from typing import Optional, Tuple
|
||||
from dataclasses import dataclass, field
|
||||
from pantograph.expr import GoalState
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class TacticInvocation:
|
||||
"""
|
||||
One tactic invocation with the before/after goals extracted from Lean source
|
||||
code.
|
||||
"""
|
||||
before: str
|
||||
after: str
|
||||
tactic: str
|
||||
used_constants: list[str]
|
||||
|
||||
@staticmethod
|
||||
def parse(payload: dict):
|
||||
return TacticInvocation(
|
||||
before=payload["goalBefore"],
|
||||
after=payload["goalAfter"],
|
||||
tactic=payload["tactic"],
|
||||
used_constants=payload.get('usedConstants', []),
|
||||
)
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class CompilationUnit:
|
||||
|
||||
# Byte boundaries [begin, end[ of each compilation unit.
|
||||
i_begin: int
|
||||
i_end: int
|
||||
|
||||
messages: list[str] = field(default_factory=list)
|
||||
|
||||
invocations: Optional[list[TacticInvocation]] = None
|
||||
# If `goal_state` is none, maybe error has occurred. See `messages`
|
||||
goal_state: Optional[GoalState] = None
|
||||
goal_src_boundaries: Optional[list[Tuple[int, int]]] = None
|
||||
|
||||
new_constants: Optional[list[str]] = None
|
||||
|
||||
@staticmethod
|
||||
def parse(payload: dict, goal_state_sentinel=None):
|
||||
i_begin = payload["boundary"][0]
|
||||
i_end = payload["boundary"][1]
|
||||
messages = payload["messages"]
|
||||
|
||||
if (invocation_payload := payload.get("invocations")) is not None:
|
||||
invocations = [
|
||||
TacticInvocation.parse(i) for i in invocation_payload
|
||||
]
|
||||
else:
|
||||
invocations = None
|
||||
|
||||
if (state_id := payload.get("goalStateId")) is not None:
|
||||
goal_state = GoalState.parse_inner(int(state_id), payload["goals"], goal_state_sentinel)
|
||||
goal_src_boundaries = payload["goalSrcBoundaries"]
|
||||
else:
|
||||
goal_state = None
|
||||
goal_src_boundaries = None
|
||||
|
||||
new_constants = payload.get("newConstants")
|
||||
|
||||
return CompilationUnit(
|
||||
i_begin,
|
||||
i_end,
|
||||
messages,
|
||||
invocations,
|
||||
goal_state,
|
||||
goal_src_boundaries,
|
||||
new_constants
|
||||
)
|
||||
|
|
@ -93,6 +93,7 @@ class GoalState:
|
|||
|
||||
@staticmethod
|
||||
def parse_inner(state_id: int, goals: list, _sentinel: list[int]):
|
||||
assert _sentinel is not None
|
||||
goal_names = { g["name"]: i for i, g in enumerate(goals) }
|
||||
goals = [Goal.parse(g, goal_names) for g in goals]
|
||||
return GoalState(state_id, goals, _sentinel)
|
||||
|
|
|
|||
|
|
@ -17,7 +17,7 @@ from pantograph.expr import (
|
|||
TacticCalc,
|
||||
TacticExpr,
|
||||
)
|
||||
from pantograph.compiler import TacticInvocation
|
||||
from pantograph.data import CompilationUnit
|
||||
|
||||
def _get_proc_cwd():
|
||||
return Path(__file__).parent
|
||||
|
|
@ -173,7 +173,11 @@ class Server:
|
|||
if "error" in result:
|
||||
print(f"Cannot start goal: {expr}")
|
||||
raise ServerError(result["desc"])
|
||||
return GoalState(state_id=result["stateId"], goals=[Goal.sentence(expr)], _sentinel=self.to_remove_goal_states)
|
||||
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:
|
||||
"""
|
||||
|
|
@ -231,7 +235,7 @@ class Server:
|
|||
raise ServerError(result["parseError"])
|
||||
return GoalState.parse(result, self.to_remove_goal_states)
|
||||
|
||||
def tactic_invocations(self, file_name: Union[str, Path]) -> tuple[list[str], list[TacticInvocation]]:
|
||||
def tactic_invocations(self, file_name: Union[str, Path]) -> list[CompilationUnit]:
|
||||
"""
|
||||
Collect tactic invocation points in file, and return them.
|
||||
"""
|
||||
|
|
@ -239,49 +243,91 @@ class Server:
|
|||
'fileName': str(file_name),
|
||||
'invocations': True,
|
||||
"sorrys": False,
|
||||
"newConstants": False,
|
||||
})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
|
||||
with open(file_name, 'rb') as f:
|
||||
content = f.read()
|
||||
units = [
|
||||
content[unit["boundary"][0]:unit["boundary"][1]].decode('utf-8')
|
||||
for unit in result['units']
|
||||
]
|
||||
invocations = [
|
||||
invocation
|
||||
for unit in result['units']
|
||||
for invocation in [TacticInvocation.parse(i) for i in unit['invocations']]
|
||||
]
|
||||
return units, invocations
|
||||
units = [CompilationUnit.parse(payload) for payload in result['units']]
|
||||
return units
|
||||
|
||||
def load_sorry(self, command: str) -> list[GoalState | list[str]]:
|
||||
def load_sorry(self, content: str) -> list[CompilationUnit]:
|
||||
"""
|
||||
Executes the compiler on a Lean file. For each compilation unit, either
|
||||
return the gathered `sorry` s, or a list of messages indicating error.
|
||||
"""
|
||||
result = self.run('frontend.process', {
|
||||
'file': command,
|
||||
'file': content,
|
||||
'invocations': False,
|
||||
"sorrys": True,
|
||||
"newConstants": False,
|
||||
})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
|
||||
def parse_unit(unit: dict):
|
||||
state_id = unit.get("goalStateId")
|
||||
if state_id is None:
|
||||
# NOTE: `state_id` maybe 0.
|
||||
# Maybe error has occurred
|
||||
return unit["messages"]
|
||||
state = GoalState.parse_inner(state_id, unit["goals"], self.to_remove_goal_states)
|
||||
return state
|
||||
states = [
|
||||
parse_unit(unit) for unit in result['units']
|
||||
units = [
|
||||
CompilationUnit.parse(payload, goal_state_sentinel=self.to_remove_goal_states)
|
||||
for payload in result['units']
|
||||
]
|
||||
return states
|
||||
return units
|
||||
|
||||
def env_add(self, name: str, t: Expr, v: Expr, is_theorem: bool = True):
|
||||
result = self.run('env.add', {
|
||||
"name": name,
|
||||
"type": t,
|
||||
"value": v,
|
||||
"isTheorem": is_theorem,
|
||||
})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
def env_inspect(
|
||||
self,
|
||||
name: str,
|
||||
print_value: bool = False,
|
||||
print_dependency: bool = False) -> dict:
|
||||
result = self.run('env.inspect', {
|
||||
"name": name,
|
||||
"value": print_value,
|
||||
"dependency": print_dependency,
|
||||
})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
return result
|
||||
|
||||
def env_save(self, path: str):
|
||||
result = self.run('env.save', {
|
||||
"path": path,
|
||||
})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
def env_load(self, path: str):
|
||||
result = self.run('env.load', {
|
||||
"path": path,
|
||||
})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
|
||||
def goal_save(self, goal_state: GoalState, path: str):
|
||||
result = self.run('goal.save', {
|
||||
"id": goal_state.state_id,
|
||||
"path": path,
|
||||
})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
def goal_load(self, path: str) -> GoalState:
|
||||
result = self.run('goal.load', {
|
||||
"path": path,
|
||||
})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
state_id = result['id']
|
||||
result = self.run('goal.print', {
|
||||
'stateId': state_id,
|
||||
'goals': True,
|
||||
})
|
||||
if "error" in result:
|
||||
raise ServerError(result["desc"])
|
||||
return GoalState.parse_inner(state_id, result['goals'], self.to_remove_goal_states)
|
||||
|
||||
|
||||
def get_version():
|
||||
|
|
@ -295,7 +341,7 @@ def get_version():
|
|||
class TestServer(unittest.TestCase):
|
||||
|
||||
def test_version(self):
|
||||
self.assertEqual(get_version(), "0.2.19")
|
||||
self.assertEqual(get_version(), "0.2.23")
|
||||
|
||||
def test_expr_type(self):
|
||||
server = Server()
|
||||
|
|
@ -445,9 +491,9 @@ class TestServer(unittest.TestCase):
|
|||
|
||||
def test_load_sorry(self):
|
||||
server = Server()
|
||||
state0, = server.load_sorry("example (p: Prop): p → p := sorry")
|
||||
if isinstance(state0, list):
|
||||
print(state0)
|
||||
unit, = server.load_sorry("example (p: Prop): p → p := sorry")
|
||||
self.assertIsNotNone(unit.goal_state, f"{unit.messages}")
|
||||
state0 = unit.goal_state
|
||||
self.assertEqual(state0.goals, [
|
||||
Goal(
|
||||
[Variable(name="p", t="Prop")],
|
||||
|
|
@ -458,6 +504,33 @@ class TestServer(unittest.TestCase):
|
|||
state2 = server.goal_tactic(state1, goal_id=0, tactic="exact h")
|
||||
self.assertTrue(state2.is_solved)
|
||||
|
||||
def test_env_add_inspect(self):
|
||||
server = Server()
|
||||
server.env_add(
|
||||
name="mystery",
|
||||
t="forall (n: Nat), Nat",
|
||||
v="fun (n: Nat) => n + 1",
|
||||
is_theorem=False,
|
||||
)
|
||||
inspect_result = server.env_inspect(name="mystery")
|
||||
self.assertEqual(inspect_result['type'], {'pp': 'Nat → Nat', 'dependentMVars': []})
|
||||
|
||||
def test_goal_state_pickling(self):
|
||||
import tempfile
|
||||
server = Server()
|
||||
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
|
||||
with tempfile.TemporaryDirectory() as td:
|
||||
path = td + "/goal-state.pickle"
|
||||
server.goal_save(state0, path)
|
||||
state0b = server.goal_load(path)
|
||||
self.assertEqual(state0b.goals, [
|
||||
Goal(
|
||||
variables=[
|
||||
],
|
||||
target="∀ (p q : Prop), p ∨ q → q ∨ p",
|
||||
)
|
||||
])
|
||||
|
||||
|
||||
if __name__ == '__main__':
|
||||
unittest.main()
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
[tool.poetry]
|
||||
name = "pantograph"
|
||||
version = "0.2.19"
|
||||
version = "0.2.23"
|
||||
description = "A machine-to-machine interaction system for Lean"
|
||||
authors = ["Leni Aniva <v@leni.sh>"]
|
||||
license = "GPL-3"
|
||||
|
|
|
|||
2
src
2
src
|
|
@ -1 +1 @@
|
|||
Subproject commit 4f6ccd3e82dd41402b7244484a1b0312d9e27018
|
||||
Subproject commit 3744cfaa9608cd43e00078283339662b3720949b
|
||||
Loading…
Reference in New Issue