doc: Update jupyter notebook

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
 ```

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": []

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:

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()