diff --git a/examples/Example/lake-manifest.json b/examples/Example/lake-manifest.json
index 06e1c0e..2199727 100644
--- a/examples/Example/lake-manifest.json
+++ b/examples/Example/lake-manifest.json
@@ -1,11 +1,12 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "3025cb124492b423070f20cf0a70636f757d117f",
-   "name": "std",
+   "scope": "",
+   "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -13,11 +14,12 @@
   {"url": "https://github.com/leanprover-community/aesop.git",
    "type": "git",
    "subDir": null,
-   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
+   "scope": "",
+   "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.8.0-rc1",
+   "inputRev": "v4.10.0-rc1",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.toml"}],
  "name": "Example",
  "lakeDir": ".lake"}
diff --git a/examples/Example/lakefile.lean b/examples/Example/lakefile.lean
index 52623f0..8759d91 100644
--- a/examples/Example/lakefile.lean
+++ b/examples/Example/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 open Lake DSL
 
 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
 
diff --git a/examples/Example/lean-toolchain b/examples/Example/lean-toolchain
index d8a6d7e..d69d1ed 100644
--- a/examples/Example/lean-toolchain
+++ b/examples/Example/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc1
+leanprover/lean4:v4.10.0-rc1
diff --git a/examples/README.md b/examples/README.md
index 68286fb..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
 ```
@@ -19,5 +21,8 @@ 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`!
+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/`!
 
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/examples/data.py b/examples/data.py
index bb1365b..f1d8978 100755
--- a/examples/data.py
+++ b/examples/data.py
@@ -14,7 +14,7 @@ if __name__ == '__main__':
     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")
+    units, invocations = server.tactic_invocations(project_path / "Example.lean")
     for i, u in enumerate(units):
         print(f"==== #{i} ====")
         print(u)
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 28268bc..7631c0e 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -2,13 +2,15 @@
 Class which manages a Pantograph instance. All calls to the kernel uses this
 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, \
     Tactic, TacticHave, TacticCalc
 from pantograph.compiler import TacticInvocation
 
 def _get_proc_cwd():
-    return pathlib.Path(__file__).parent
+    return Path(__file__).parent
 def _get_proc_path():
     return _get_proc_cwd() / "pantograph-repl"
 
@@ -22,7 +24,7 @@ class Server:
                  project_path=None,
                  lean_path=None,
                  # Options for executing the REPL.
-                 # Set `{ "automaticMode" : True }` to get a gym-like experience
+                 # Set `{ "automaticMode" : False }` to handle resumption by yourself.
                  options={},
                  core_options=[],
                  timeout=20,
@@ -64,7 +66,7 @@ class Server:
         )
         self.proc.setecho(False) # Do not send any command before this.
         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:
             self.run("options.set", self.options)
@@ -146,23 +148,39 @@ class Server:
             raise ServerError(result["parseError"])
         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
+    def tactic_invocations(self, file_name: Union[str, Path]) -> tuple[list[str], list[TacticInvocation]]:
+        """
+        Collect tactic invocation points in file, and return them.
+        """
+        result = self.run('frontend.process', {
+            'fileName': str(file_name),
+            'invocations': True,
+            "sorrys": False,
         })
         if "error" in result:
             raise ServerError(result["desc"])
 
-        with open(file_path, 'rb') as f:
+        with open(file_name, '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 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():
@@ -176,7 +194,7 @@ def get_version():
 class TestServer(unittest.TestCase):
 
     def test_version(self):
-        self.assertEqual(get_version(), "0.2.17")
+        self.assertEqual(get_version(), "0.2.19")
 
     def test_expr_type(self):
         server = Server()
@@ -209,7 +227,7 @@ class TestServer(unittest.TestCase):
         self.assertEqual(len(server.to_remove_goal_states), 0)
 
     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")
         self.assertEqual(len(server.to_remove_goal_states), 0)
         self.assertEqual(state0.state_id, 0)
@@ -261,7 +279,7 @@ class TestServer(unittest.TestCase):
 
 
     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")
 
         variables = [
@@ -293,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()
diff --git a/src b/src
index 9b3eef3..bec84f8 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit 9b3eef35ec40a09bba7140ecfc04dafddbd92c27
+Subproject commit bec84f857bd4f80064213fa5646bef4699191290