From d99104cf0ec7bc3611c4c0fa9f9748b7e7b570ff Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Sep 2024 19:28:35 -0700 Subject: [PATCH] doc: Update jupyter notebook --- examples/README.md | 4 ++- examples/all.ipynb | 85 ++++++++++++++++++++++++++++++-------------- pantograph/expr.py | 8 +++-- pantograph/server.py | 27 ++++++++++++++ 4 files changed, 94 insertions(+), 30 deletions(-) diff --git a/examples/README.md b/examples/README.md index 5991455..41e702e 100644 --- a/examples/README.md +++ b/examples/README.md @@ -1,6 +1,8 @@ # 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 poetry run jupyter notebook ``` diff --git a/examples/all.ipynb b/examples/all.ipynb index 6e201a7..21e668e 100644 --- a/examples/all.ipynb +++ b/examples/all.ipynb @@ -7,14 +7,14 @@ "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", + "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": 2, + "execution_count": 1, "id": "101f4591-ec31-4000-96a6-ac3fc3dd0fa2", "metadata": {}, "outputs": [], @@ -34,7 +34,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 2, "id": "4affc375-360b-40cf-8d22-4fdcc12dba0d", "metadata": {}, "outputs": [], @@ -52,7 +52,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 3, "id": "29f7ae15-7f69-4740-a6fa-71fbb1ccabd8", "metadata": {}, "outputs": [ @@ -62,7 +62,7 @@ "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": {}, "output_type": "execute_result" } @@ -81,17 +81,17 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 4, "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])" + "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": {}, "output_type": "execute_result" } @@ -111,7 +111,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 5, "id": "2d18d6dc-7936-4bb6-b47d-f781dd8ddacd", "metadata": {}, "outputs": [ @@ -121,7 +121,7 @@ "'p✝ : Prop\\n⊢ p✝ → p✝'" ] }, - "execution_count": 9, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -140,7 +140,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 6, "id": "a0fdd3b3-9b38-4602-84a3-89065822f6e8", "metadata": {}, "outputs": [ @@ -170,17 +170,17 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 7, "id": "9d18045a-9734-415c-8f40-7aadb6cb18f4", "metadata": {}, "outputs": [ { "data": { "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": {}, "output_type": "execute_result" } @@ -201,7 +201,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 8, "id": "ee98de99-3cfc-4449-8d62-00e8eaee03db", "metadata": {}, "outputs": [], @@ -223,7 +223,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 9, "id": "ecf5d9d3-e53e-4f67-969e-d38e3d97c65e", "metadata": {}, "outputs": [ @@ -231,8 +231,8 @@ "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" + "$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.10.0-rc1/lib/lean\\n'\n" ] } ], @@ -259,7 +259,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 10, "id": "bf485778-baa9-4c1c-80fa-960f9cf9bc8a", "metadata": {}, "outputs": [ @@ -269,7 +269,7 @@ "True" ] }, - "execution_count": 20, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } @@ -287,12 +287,12 @@ "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`." + "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": 21, + "execution_count": 11, "id": "8ff6007b-50df-4449-9a86-6d3eb0bc0caa", "metadata": {}, "outputs": [ @@ -316,8 +316,6 @@ " . apply Or.inl\n", " assumption\n", "\n", - "==== #2 ====\n", - "\n", "==== Invocations ====\n", "α : Sort ?u.7\n", "⊢ α → α\n", @@ -378,7 +376,7 @@ } ], "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", " print(f\"==== #{i} ====\")\n", " print(u)\n", @@ -387,10 +385,45 @@ " 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": "cb5bbbcc-01dc-4a35-81ba-e155cedb9a91", + "id": "50b90547-fcbf-419f-866e-a6ebcc925c5f", "metadata": {}, "outputs": [], "source": [] diff --git a/pantograph/expr.py b/pantograph/expr.py index 6c54241..0b36c01 100644 --- a/pantograph/expr.py +++ b/pantograph/expr.py @@ -73,10 +73,12 @@ class GoalState: return not self.goals @staticmethod - def parse(payload: dict, _sentinel: list[int]): - state_id = payload["nextStateId"] - goals = [Goal.parse(g) for g in payload["goals"]] + def parse_inner(state_id: int, goals: list, _sentinel: list[int]): + goals = [Goal.parse(g) for g in goals] 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) class TacticHave: diff --git a/pantograph/server.py b/pantograph/server.py index 8595635..7631c0e 100644 --- a/pantograph/server.py +++ b/pantograph/server.py @@ -167,6 +167,20 @@ class Server: invocations = [TacticInvocation.parse(i) for i in result['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(): @@ -297,6 +311,19 @@ class TestServer(unittest.TestCase): state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]") 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__': unittest.main()