aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

Merge pull request #13 from lenianiva/frontend/collect-holes 

feat: Collect sorrys command in the server
This commit is contained in:
Leni Aniva 2024-09-13 18:22:51 -07:00 committed by GitHub
parent 180f1b1313 2f70e6d918
commit 8d43507901
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
9 changed files with 129 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
examples/Example/lake-manifest.json
View File

@ -1,11 +1,12 @@
{"version": 7, {"version": "1.1.0",
"packagesDir": ".lake/packages", "packagesDir": ".lake/packages",
"packages": "packages":
[{"url": "https://github.com/leanprover/std4", [{"url": "https://github.com/leanprover-community/batteries",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"rev": "3025cb124492b423070f20cf0a70636f757d117f", "scope": "",
"name": "std", "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98",
"name": "batteries",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "main", "inputRev": "main",
"inherited": true, "inherited": true,
@ -13,11 +14,12 @@
{"url": "https://github.com/leanprover-community/aesop.git", {"url": "https://github.com/leanprover-community/aesop.git",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0", "scope": "",
"rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
"name": "aesop", "name": "aesop",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "v4.8.0-rc1", "inputRev": "v4.10.0-rc1",
"inherited": false, "inherited": false,
"configFile": "lakefile.lean"}], "configFile": "lakefile.toml"}],
"name": "Example", "name": "Example",
"lakeDir": ".lake"} "lakeDir": ".lake"}

2
examples/Example/lakefile.lean
View File

@ -2,7 +2,7 @@ import Lake
open Lake DSL open Lake DSL
require aesop from git require aesop from git
"https://github.com/leanprover-community/aesop.git" @ "v4.8.0-rc1" "https://github.com/leanprover-community/aesop.git" @ "v4.10.0-rc1"
package Example package Example

2
examples/Example/lean-toolchain
View File

@ -1 +1 @@
leanprover/lean4:v4.8.0-rc1 leanprover/lean4:v4.10.0-rc1

9
examples/README.md
View File

@ -1,6 +1,8 @@
# Examples # Examples
For a quick introduction of the API, fire up Jupyter and open `all.ipynb`. For a quick introduction of the API, fire up Jupyter and open `all.ipynb`. (Did
you remember to `poetry install`?)
``` sh ``` sh
poetry run jupyter notebook poetry run jupyter notebook
``` ```
@ -19,5 +21,8 @@ poetry run examples/aesop.py
poetry run examples/data.py poetry run examples/data.py
``` ```
Warning: If you make modifications to any Lean files, you must re-run `lake build`! Warning: If you make modifications to any Lean files, you must re-run `lake
build`! Moreover, the version of the Lean used in the example folder (including
dependencies in `lakefile.lean` and `lean-toolchain`) **must match exactly**
with the version in `src/`!

85
examples/all.ipynb
View File

@ -7,14 +7,14 @@
"source": [ "source": [
"# Pantograph Example\n", "# Pantograph Example\n",
"\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", "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", "\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\"]`." "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", "cell_type": "code",
"execution_count": 2, "execution_count": 1,
"id": "101f4591-ec31-4000-96a6-ac3fc3dd0fa2", "id": "101f4591-ec31-4000-96a6-ac3fc3dd0fa2",
"metadata": {}, "metadata": {},
"outputs": [], "outputs": [],
@ -34,7 +34,7 @@
}, },
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 3, "execution_count": 2,
"id": "4affc375-360b-40cf-8d22-4fdcc12dba0d", "id": "4affc375-360b-40cf-8d22-4fdcc12dba0d",
"metadata": {}, "metadata": {},
"outputs": [], "outputs": [],
@ -52,7 +52,7 @@
}, },
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 6, "execution_count": 3,
"id": "29f7ae15-7f69-4740-a6fa-71fbb1ccabd8", "id": "29f7ae15-7f69-4740-a6fa-71fbb1ccabd8",
"metadata": {}, "metadata": {},
"outputs": [ "outputs": [
@ -62,7 +62,7 @@
"GoalState(state_id=0, goals=[Goal(variables=[], target='forall (p : Prop), p -> p', name=None, is_conversion=False)], _sentinel=[])" "GoalState(state_id=0, goals=[Goal(variables=[], target='forall (p : Prop), p -> p', name=None, is_conversion=False)], _sentinel=[])"
] ]
}, },
"execution_count": 6, "execution_count": 3,
"metadata": {}, "metadata": {},
"output_type": "execute_result" "output_type": "execute_result"
} }
@ -81,17 +81,17 @@
}, },
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 8, "execution_count": 4,
"id": "bfbd5512-fcb0-428d-8131-4da4005e743c", "id": "bfbd5512-fcb0-428d-8131-4da4005e743c",
"metadata": {}, "metadata": {},
"outputs": [ "outputs": [
{ {
"data": { "data": {
"text/plain": [ "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])" "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": 8, "execution_count": 4,
"metadata": {}, "metadata": {},
"output_type": "execute_result" "output_type": "execute_result"
} }
@ -111,7 +111,7 @@
}, },
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 9, "execution_count": 5,
"id": "2d18d6dc-7936-4bb6-b47d-f781dd8ddacd", "id": "2d18d6dc-7936-4bb6-b47d-f781dd8ddacd",
"metadata": {}, "metadata": {},
"outputs": [ "outputs": [
@ -121,7 +121,7 @@
"'p✝ : Prop\\n⊢ p✝ → p✝'" "'p✝ : Prop\\n⊢ p✝ → p✝'"
] ]
}, },
"execution_count": 9, "execution_count": 5,
"metadata": {}, "metadata": {},
"output_type": "execute_result" "output_type": "execute_result"
} }
@ -140,7 +140,7 @@
}, },
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 12, "execution_count": 6,
"id": "a0fdd3b3-9b38-4602-84a3-89065822f6e8", "id": "a0fdd3b3-9b38-4602-84a3-89065822f6e8",
"metadata": {}, "metadata": {},
"outputs": [ "outputs": [
@ -170,17 +170,17 @@
}, },
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 15, "execution_count": 7,
"id": "9d18045a-9734-415c-8f40-7aadb6cb18f4", "id": "9d18045a-9734-415c-8f40-7aadb6cb18f4",
"metadata": {}, "metadata": {},
"outputs": [ "outputs": [
{ {
"data": { "data": {
"text/plain": [ "text/plain": [
"GoalState(state_id=7, goals=[], _sentinel=[1, 3, 4, 5])" "GoalState(state_id=3, goals=[], _sentinel=[])"
] ]
}, },
"execution_count": 15, "execution_count": 7,
"metadata": {}, "metadata": {},
"output_type": "execute_result" "output_type": "execute_result"
} }
@ -201,7 +201,7 @@
}, },
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 16, "execution_count": 8,
"id": "ee98de99-3cfc-4449-8d62-00e8eaee03db", "id": "ee98de99-3cfc-4449-8d62-00e8eaee03db",
"metadata": {}, "metadata": {},
"outputs": [], "outputs": [],
@ -223,7 +223,7 @@
}, },
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 19, "execution_count": 9,
"id": "ecf5d9d3-e53e-4f67-969e-d38e3d97c65e", "id": "ecf5d9d3-e53e-4f67-969e-d38e3d97c65e",
"metadata": {}, "metadata": {},
"outputs": [ "outputs": [
@ -231,8 +231,8 @@
"name": "stdout", "name": "stdout",
"output_type": "stream", "output_type": "stream",
"text": [ "text": [
"$PWD: /Users/aniva/Projects/atp/PyPantograph/examples/Example\n", "$PWD: /home/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" "$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.10.0-rc1/lib/lean\\n'\n"
] ]
} }
], ],
@ -259,7 +259,7 @@
}, },
{ {
"cell_type": "code", "cell_type": "code",
"execution_count": 20, "execution_count": 10,
"id": "bf485778-baa9-4c1c-80fa-960f9cf9bc8a", "id": "bf485778-baa9-4c1c-80fa-960f9cf9bc8a",
"metadata": {}, "metadata": {},
"outputs": [ "outputs": [
@ -269,7 +269,7 @@
"True" "True"
] ]
}, },
"execution_count": 20, "execution_count": 10,
"metadata": {}, "metadata": {},
"output_type": "execute_result" "output_type": "execute_result"
} }
@ -287,12 +287,12 @@
"source": [ "source": [
"## Reading Symbols\n", "## Reading Symbols\n",
"\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`." "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", "cell_type": "code",
"execution_count": 21, "execution_count": 11,
"id": "8ff6007b-50df-4449-9a86-6d3eb0bc0caa", "id": "8ff6007b-50df-4449-9a86-6d3eb0bc0caa",
"metadata": {}, "metadata": {},
"outputs": [ "outputs": [
@ -316,8 +316,6 @@
" . apply Or.inl\n", " . apply Or.inl\n",
" assumption\n", " assumption\n",
"\n", "\n",
"==== #2 ====\n",
"\n",
"==== Invocations ====\n", "==== Invocations ====\n",
"α : Sort ?u.7\n", "α : Sort ?u.7\n",
"⊢ α → α\n", "⊢ α → α\n",
@ -378,7 +376,7 @@
} }
], ],
"source": [ "source": [
"units, invocations = server.compile_unit(\"Example\")\n", "units, invocations = server.tactic_invocations(project_path / \"Example.lean\")\n",
"for i, u in enumerate(units):\n", "for i, u in enumerate(units):\n",
" print(f\"==== #{i} ====\")\n", " print(f\"==== #{i} ====\")\n",
" print(u)\n", " print(u)\n",
@ -387,10 +385,45 @@
" print(f\"{i.before}\\n{i.tactic}\\n{i.after}\\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", "cell_type": "code",
"execution_count": null, "execution_count": null,
"id": "cb5bbbcc-01dc-4a35-81ba-e155cedb9a91", "id": "50b90547-fcbf-419f-866e-a6ebcc925c5f",
"metadata": {}, "metadata": {},
"outputs": [], "outputs": [],
"source": [] "source": []

2
examples/data.py
View File

@ -14,7 +14,7 @@ if __name__ == '__main__':
print(f"$PWD: {project_path}") print(f"$PWD: {project_path}")
print(f"$LEAN_PATH: {lean_path}") print(f"$LEAN_PATH: {lean_path}")
server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path) server = Server(imports=['Example'], project_path=project_path, lean_path=lean_path)
units, invocations = server.compile_unit("Example") units, invocations = server.tactic_invocations(project_path / "Example.lean")
for i, u in enumerate(units): for i, u in enumerate(units):
print(f"==== #{i} ====") print(f"==== #{i} ====")
print(u) print(u)

8
pantograph/expr.py
View File

@ -73,10 +73,12 @@ class GoalState:
return not self.goals return not self.goals
@staticmethod @staticmethod
def parse(payload: dict, _sentinel: list[int]): def parse_inner(state_id: int, goals: list, _sentinel: list[int]):
state_id = payload["nextStateId"] goals = [Goal.parse(g) for g in goals]
goals = [Goal.parse(g) for g in payload["goals"]]
return GoalState(state_id, goals, _sentinel) return GoalState(state_id, goals, _sentinel)
@staticmethod
def parse(payload: dict, _sentinel: list[int]):
return GoalState.parse_inner(payload["nextStateId"], payload["goals"], _sentinel)
@dataclass(frozen=True) @dataclass(frozen=True)
class TacticHave: class TacticHave:

59
pantograph/server.py
View File

@ -2,13 +2,15 @@
Class which manages a Pantograph instance. All calls to the kernel uses this Class which manages a Pantograph instance. All calls to the kernel uses this
interface. interface.
""" """
import json, pexpect, pathlib, unittest, os import json, pexpect, unittest, os
from typing import Union
from pathlib import Path
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 from pantograph.compiler import TacticInvocation
def _get_proc_cwd(): def _get_proc_cwd():
return pathlib.Path(__file__).parent return Path(__file__).parent
def _get_proc_path(): def _get_proc_path():
return _get_proc_cwd() / "pantograph-repl" return _get_proc_cwd() / "pantograph-repl"
@ -22,7 +24,7 @@ class Server:
project_path=None, project_path=None,
lean_path=None, lean_path=None,
# Options for executing the REPL. # Options for executing the REPL.
# Set `{ "automaticMode" : True }` to get a gym-like experience # Set `{ "automaticMode" : False }` to handle resumption by yourself.
options={}, options={},
core_options=[], core_options=[],
timeout=20, timeout=20,
@ -64,7 +66,7 @@ class Server:
) )
self.proc.setecho(False) # Do not send any command before this. self.proc.setecho(False) # Do not send any command before this.
ready = self.proc.readline() # Reads the "ready." ready = self.proc.readline() # Reads the "ready."
assert ready == "ready.\r\n" assert ready == "ready.\r\n", f"Server failed to emit ready signal: {ready}; Maybe the project needs to be rebuilt"
if self.options: if self.options:
self.run("options.set", self.options) self.run("options.set", self.options)
@ -146,23 +148,39 @@ 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]]: def tactic_invocations(self, file_name: Union[str, Path]) -> tuple[list[str], list[TacticInvocation]]:
file_path = self.project_path / (module.replace('.', '/') + '.lean') """
result = self.run('compile.unit', { Collect tactic invocation points in file, and return them.
'module': module, """
'compilationUnits': True, result = self.run('frontend.process', {
'invocations': True 'fileName': str(file_name),
'invocations': True,
"sorrys": False,
}) })
if "error" in result: if "error" in result:
raise ServerError(result["desc"]) raise ServerError(result["desc"])
with open(file_path, 'rb') as f: with open(file_name, 'rb') as f:
content = f.read() content = f.read()
units = [content[begin:end].decode('utf-8') for begin,end in result['units']] units = [content[begin:end].decode('utf-8') for begin,end in result['units']]
invocations = [TacticInvocation.parse(i) for i in result['invocations']] invocations = [TacticInvocation.parse(i) for i in result['invocations']]
return units, invocations return units, invocations
def load_sorry(self, command: str) -> list[GoalState]:
result = self.run('frontend.process', {
'file': command,
'invocations': False,
"sorrys": True,
})
if "error" in result:
raise ServerError(result["desc"])
states = [
GoalState.parse_inner(state_id, goals, self.to_remove_goal_states)
for (state_id, goals) in result['goalStates']
]
return states
def get_version(): def get_version():
@ -176,7 +194,7 @@ def get_version():
class TestServer(unittest.TestCase): class TestServer(unittest.TestCase):
def test_version(self): def test_version(self):
self.assertEqual(get_version(), "0.2.17") self.assertEqual(get_version(), "0.2.19")
def test_expr_type(self): def test_expr_type(self):
server = Server() server = Server()
@ -209,7 +227,7 @@ class TestServer(unittest.TestCase):
self.assertEqual(len(server.to_remove_goal_states), 0) self.assertEqual(len(server.to_remove_goal_states), 0)
def test_automatic_mode(self): def test_automatic_mode(self):
server = Server(options={"automaticMode": True}) server = Server()
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p") state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
self.assertEqual(len(server.to_remove_goal_states), 0) self.assertEqual(len(server.to_remove_goal_states), 0)
self.assertEqual(state0.state_id, 0) self.assertEqual(state0.state_id, 0)
@ -261,7 +279,7 @@ class TestServer(unittest.TestCase):
def test_conv_calc(self): def test_conv_calc(self):
server = Server() server = Server(options={"automaticMode": False})
state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b") state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
variables = [ variables = [
@ -293,6 +311,19 @@ class TestServer(unittest.TestCase):
state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]") state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
self.assertTrue(state4.is_solved) self.assertTrue(state4.is_solved)
def test_load_sorry(self):
server = Server()
state0, = server.load_sorry("example (p: Prop): p → p := sorry")
self.assertEqual(state0.goals, [
Goal(
[Variable(name="p", t="Prop")],
target="p → p",
),
])
state1 = server.goal_tactic(state0, goal_id=0, tactic="intro h")
state2 = server.goal_tactic(state1, goal_id=0, tactic="exact h")
self.assertTrue(state2.is_solved)
if __name__ == '__main__': if __name__ == '__main__':
unittest.main() unittest.main()

2
src

@ -1 +1 @@
Subproject commit 9b3eef35ec40a09bba7140ecfc04dafddbd92c27 Subproject commit bec84f857bd4f80064213fa5646bef4699191290