From d3c14f321fe73ef002cadd5c5321c5ff443c5d4a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 01:30:52 -0800
Subject: [PATCH 01/13] chore: Update to 0.2.22

---
 pantograph/server.py | 4 +++-
 pyproject.toml       | 2 +-
 src                  | 2 +-
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/pantograph/server.py b/pantograph/server.py
index db71c84..3e9943d 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -239,6 +239,7 @@ class Server:
             'fileName': str(file_name),
             'invocations': True,
             "sorrys": False,
+            "newConstants": False,
         })
         if "error" in result:
             raise ServerError(result["desc"])
@@ -265,6 +266,7 @@ class Server:
             'file': command,
             'invocations': False,
             "sorrys": True,
+            "newConstants": False,
         })
         if "error" in result:
             raise ServerError(result["desc"])
@@ -295,7 +297,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.22")
 
     def test_expr_type(self):
         server = Server()
diff --git a/pyproject.toml b/pyproject.toml
index ef55b3c..7736e99 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "pantograph"
-version = "0.2.19"
+version = "0.2.22"
 description = "A machine-to-machine interaction system for Lean"
 authors = ["Leni Aniva <v@leni.sh>"]
 license = "GPL-3"
diff --git a/src b/src
index 4f6ccd3..5d76626 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit 4f6ccd3e82dd41402b7244484a1b0312d9e27018
+Subproject commit 5d76626912795579832f2bb43748e137bb6d0595

From 47b2fbe38d777045e9472697d46419edd1a574d4 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 16:25:45 -0800
Subject: [PATCH 02/13] refactor: Into CompilationUnit objects

---
 pantograph/compiler.py | 21 -------------
 pantograph/data.py     | 69 ++++++++++++++++++++++++++++++++++++++++++
 pantograph/expr.py     |  1 +
 pantograph/server.py   | 50 +++++++++++-------------------
 4 files changed, 88 insertions(+), 53 deletions(-)
 delete mode 100644 pantograph/compiler.py
 create mode 100644 pantograph/data.py

diff --git a/pantograph/compiler.py b/pantograph/compiler.py
deleted file mode 100644
index 38469bf..0000000
--- a/pantograph/compiler.py
+++ /dev/null
@@ -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', []),
-        )
diff --git a/pantograph/data.py b/pantograph/data.py
new file mode 100644
index 0000000..d2c0ae0
--- /dev/null
+++ b/pantograph/data.py
@@ -0,0 +1,69 @@
+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:
+
+    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
+        )
diff --git a/pantograph/expr.py b/pantograph/expr.py
index 5c8bbc2..f616354 100644
--- a/pantograph/expr.py
+++ b/pantograph/expr.py
@@ -98,6 +98,7 @@ class GoalState:
         return GoalState(state_id, goals, _sentinel)
     @staticmethod
     def parse(payload: dict, _sentinel: list[int]):
+        assert _sentinel is not None
         return GoalState.parse_inner(payload["nextStateId"], payload["goals"], _sentinel)
 
     def __str__(self):
diff --git a/pantograph/server.py b/pantograph/server.py
index 3e9943d..bed7682 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -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.
         """
@@ -244,26 +248,16 @@ class Server:
         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,
@@ -271,19 +265,11 @@ class Server:
         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 get_version():
@@ -447,9 +433,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")],

From 359b5f8d47298a920dd7105470636b38bc896497 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 16:32:12 -0800
Subject: [PATCH 03/13] feat: env.{add, inspect}

---
 pantograph/server.py | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/pantograph/server.py b/pantograph/server.py
index bed7682..703b9c1 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -271,6 +271,29 @@ class Server:
         ]
         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 get_version():
     import subprocess
@@ -446,6 +469,17 @@ 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': []})
+
 
 if __name__ == '__main__':
     unittest.main()

From fb8652d13230ba4556d4f53138bb36309cf6397d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 16:36:55 -0800
Subject: [PATCH 04/13] feat: Env/Goal pickling

---
 pantograph/server.py | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/pantograph/server.py b/pantograph/server.py
index 703b9c1..284694e 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -294,6 +294,36 @@ class Server:
             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) -> int:
+        # FIXME: Load the entire state
+        result = self.run('goal.load', {
+            "path": path,
+        })
+        if "error" in result:
+            raise ServerError(result["desc"])
+        state_id = result['id']
+        return state_id
+
 
 def get_version():
     import subprocess

From f1e3ec82f03c622b812627c37d2eb746ff951f22 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 16:54:50 -0800
Subject: [PATCH 05/13] fix: Goal state pickling/unpickling

---
 pantograph/server.py | 13 +++++++++----
 src                  |  2 +-
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/pantograph/server.py b/pantograph/server.py
index 284694e..3e26edd 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -314,15 +314,20 @@ class Server:
         })
         if "error" in result:
             raise ServerError(result["desc"])
-    def goal_load(self, path: str) -> int:
-        # FIXME: Load the entire state
+    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']
-        return state_id
+        result = self.run('goal.print', {
+            'stateId': state_id,
+            'goals': True,
+        })
+        if "error" in result:
+            raise ServerError(result["desc"])
+        return GoalState.parse(result, self.to_remove_goal_states)
 
 
 def get_version():
@@ -336,7 +341,7 @@ def get_version():
 class TestServer(unittest.TestCase):
 
     def test_version(self):
-        self.assertEqual(get_version(), "0.2.22")
+        self.assertEqual(get_version(), "0.2.23")
 
     def test_expr_type(self):
         server = Server()
diff --git a/src b/src
index 5d76626..3744cfa 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit 5d76626912795579832f2bb43748e137bb6d0595
+Subproject commit 3744cfaa9608cd43e00078283339662b3720949b

From 8e373eb3b215bb02046c3f5bb4671578f807f70a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 17:00:25 -0800
Subject: [PATCH 06/13] fix: Goal state pickling

---
 pantograph/expr.py   |  2 +-
 pantograph/server.py | 18 +++++++++++++++++-
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/pantograph/expr.py b/pantograph/expr.py
index f616354..be648c8 100644
--- a/pantograph/expr.py
+++ b/pantograph/expr.py
@@ -93,12 +93,12 @@ 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)
     @staticmethod
     def parse(payload: dict, _sentinel: list[int]):
-        assert _sentinel is not None
         return GoalState.parse_inner(payload["nextStateId"], payload["goals"], _sentinel)
 
     def __str__(self):
diff --git a/pantograph/server.py b/pantograph/server.py
index 3e26edd..645897e 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -327,7 +327,7 @@ class Server:
         })
         if "error" in result:
             raise ServerError(result["desc"])
-        return GoalState.parse(result, self.to_remove_goal_states)
+        return GoalState.parse_inner(state_id, result['goals'], self.to_remove_goal_states)
 
 
 def get_version():
@@ -515,6 +515,22 @@ class TestServer(unittest.TestCase):
         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()

From 57001bb0a3040a3a12e1cc0741c5ecbd5fd46d7e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 17:07:35 -0800
Subject: [PATCH 07/13] doc: Update documentation

---
 docs/api-data.rst |  2 +-
 docs/goal.ipynb   |  6 ++++--
 docs/intro.md     | 32 ++++++++++++++++++++++++++++++++
 3 files changed, 37 insertions(+), 3 deletions(-)

diff --git a/docs/api-data.rst b/docs/api-data.rst
index e853b1d..bc65d4b 100644
--- a/docs/api-data.rst
+++ b/docs/api-data.rst
@@ -1,5 +1,5 @@
 Data
 =============
 
-.. automodule:: pantograph.compiler
+.. automodule:: pantograph.data
     :members:
diff --git a/docs/goal.ipynb b/docs/goal.ipynb
index b59748f..d6d7e78 100644
--- a/docs/goal.ipynb
+++ b/docs/goal.ipynb
@@ -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,
diff --git a/docs/intro.md b/docs/intro.md
index c7ef45a..74a18f2 100644
--- a/docs/intro.md
+++ b/docs/intro.md
@@ -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)

From 4c559294d34974fe13dac87975aa482ea4dbf6b7 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 17:07:50 -0800
Subject: [PATCH 08/13] chore: Update version

---
 pyproject.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pyproject.toml b/pyproject.toml
index 7736e99..8cc9bcc 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "pantograph"
-version = "0.2.22"
+version = "0.2.23"
 description = "A machine-to-machine interaction system for Lean"
 authors = ["Leni Aniva <v@leni.sh>"]
 license = "GPL-3"

From 04e40b6dfab76eac33fe331a2a5b13dc7d0b84b5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 17:14:44 -0800
Subject: [PATCH 09/13] doc: Update all examples to 0.2.23

---
 docs/data.ipynb    | 69 ++++++++++++++++++++++++++++------------------
 examples/data.py   | 23 ----------------
 examples/sketch.py |  4 +--
 pantograph/data.py |  2 ++
 4 files changed, 46 insertions(+), 52 deletions(-)
 delete mode 100755 examples/data.py

diff --git a/docs/data.ipynb b/docs/data.ipynb
index f3afbc0..0b04592 100644
--- a/docs/data.ipynb
+++ b/docs/data.ipynb
@@ -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,
diff --git a/examples/data.py b/examples/data.py
deleted file mode 100755
index f1d8978..0000000
--- a/examples/data.py
+++ /dev/null
@@ -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")
diff --git a/examples/sketch.py b/examples/sketch.py
index 0f9bb74..f8cad14 100644
--- a/examples/sketch.py
+++ b/examples/sketch.py
@@ -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)
diff --git a/pantograph/data.py b/pantograph/data.py
index d2c0ae0..5863aac 100644
--- a/pantograph/data.py
+++ b/pantograph/data.py
@@ -25,8 +25,10 @@ class TacticInvocation:
 @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

From ce7e27a0fd974f38d06894a99d1641d2c94af87d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 17:20:25 -0800
Subject: [PATCH 10/13] doc: Add doc building instructions

---
 README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index cad254e..6c290c7 100644
--- a/README.md
+++ b/README.md
@@ -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

From 56fc11f83148c8cdf03d6a10910407594d5062bd Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 17:32:07 -0800
Subject: [PATCH 11/13] fix: Experiments with new `load_sorry`

---
 experiments/dsp/main.py     | 10 +++++-----
 experiments/minif2f/main.py |  9 +++++----
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/experiments/dsp/main.py b/experiments/dsp/main.py
index 8437b85..133e766 100644
--- a/experiments/dsp/main.py
+++ b/experiments/dsp/main.py
@@ -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,
diff --git a/experiments/minif2f/main.py b/experiments/minif2f/main.py
index a2726f2..9e03d85 100755
--- a/experiments/minif2f/main.py
+++ b/experiments/minif2f/main.py
@@ -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(

From 2aa5fb2a3d4489642ad263756891906f227514f2 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 20:46:39 -0800
Subject: [PATCH 12/13] doc: Update `load_sorry` documentation

---
 docs/drafting.ipynb |   8 +-
 examples/all.ipynb  | 448 --------------------------------------------
 2 files changed, 4 insertions(+), 452 deletions(-)
 delete mode 100644 examples/all.ipynb

diff --git a/docs/drafting.ipynb b/docs/drafting.ipynb
index f5dfd5a..59011cf 100644
--- a/docs/drafting.ipynb
+++ b/docs/drafting.ipynb
@@ -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,
diff --git a/examples/all.ipynb b/examples/all.ipynb
deleted file mode 100644
index 121cd5a..0000000
--- a/examples/all.ipynb
+++ /dev/null
@@ -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
-}

From ffacb67a03cca4e0ba6f3639ead16db9091bddba Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 21:30:40 -0800
Subject: [PATCH 13/13] fix: DSP output

---
 experiments/dsp/main.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/experiments/dsp/main.py b/experiments/dsp/main.py
index 133e766..3372e00 100644
--- a/experiments/dsp/main.py
+++ b/experiments/dsp/main.py
@@ -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),