From 28419a050f1697426e8668c48062b2430ba5da52 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 14 Jan 2025 18:08:04 -0800
Subject: [PATCH 1/9] chore: Update upstream to v0.2.25-pre

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

diff --git a/pantograph/server.py b/pantograph/server.py
index 1bca76c..029ba17 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -344,7 +344,7 @@ def get_version():
 class TestServer(unittest.TestCase):
 
     def test_version(self):
-        self.assertEqual(get_version(), "0.2.24")
+        self.assertEqual(get_version(), "0.2.25")
 
     def test_expr_type(self):
         server = Server()
diff --git a/pyproject.toml b/pyproject.toml
index 6a90700..06d7d99 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "pantograph"
-version = "0.2.24"
+version = "0.2.25"
 description = "A machine-to-machine interaction system for Lean"
 authors = ["Leni Aniva <v@leni.sh>"]
 license = "Apache-2.0"
diff --git a/src b/src
index ef4e5ec..c1f63af 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit ef4e5ecbf8057c6baf542391d4c40ec068810aa4
+Subproject commit c1f63af01920e5038298795e969c574994411329

From 1ed1f07ec69c5258ccd3551dee1eaf1498e02699 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 16 Jan 2025 09:33:20 -0800
Subject: [PATCH 2/9] fix: Type error as goals flag

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

diff --git a/pantograph/server.py b/pantograph/server.py
index 029ba17..3637e39 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -244,6 +244,7 @@ def tactic_invocations(self, file_name: Union[str, Path]) -> list[CompilationUni
             'invocations': True,
             "sorrys": False,
             "newConstants": False,
+            "typeErrorsAsGoals": False,
         })
         if "error" in result:
             raise ServerError(result["desc"])

From 7d385694b285a1c715b77e07992ca25e3aa52228 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 16 Jan 2025 11:30:41 -0800
Subject: [PATCH 3/9] feat: Support for draft tactic

---
 pantograph/expr.py   |  8 +++++++-
 pantograph/server.py | 23 +++++++++++++++++++++--
 src                  |  2 +-
 3 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/pantograph/expr.py b/pantograph/expr.py
index be648c8..5ad1a33 100644
--- a/pantograph/expr.py
+++ b/pantograph/expr.py
@@ -143,5 +143,11 @@ class TacticExpr:
     Assigns an expression to the current goal
     """
     expr: str
+@dataclass(frozen=True)
+class TacticDraft:
+    """
+    Assigns an expression to the current goal
+    """
+    expr: str
 
-Tactic: TypeAlias = str | TacticHave | TacticLet | TacticCalc | TacticExpr
+Tactic: TypeAlias = str | TacticHave | TacticLet | TacticCalc | TacticExpr | TacticDraft
diff --git a/pantograph/server.py b/pantograph/server.py
index 3637e39..77b87f3 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -16,6 +16,7 @@
     TacticLet,
     TacticCalc,
     TacticExpr,
+    TacticDraft,
 )
 from pantograph.data import CompilationUnit
 
@@ -194,10 +195,12 @@ def goal_tactic(self, state: GoalState, goal_id: int, tactic: Tactic) -> GoalSta
             args["let"] = tactic.branch
             if tactic.binder_name:
                 args["binderName"] = tactic.binder_name
-        elif isinstance(tactic, TacticExpr):
-            args["expr"] = tactic.expr
         elif isinstance(tactic, TacticCalc):
             args["calc"] = tactic.step
+        elif isinstance(tactic, TacticExpr):
+            args["expr"] = tactic.expr
+        elif isinstance(tactic, TacticDraft):
+            args["draft"] = tactic.expr
         else:
             raise RuntimeError(f"Invalid tactic type: {tactic}")
         result = self.run('goal.tactic', args)
@@ -508,6 +511,22 @@ def test_load_sorry(self):
         state2 = server.goal_tactic(state1, goal_id=0, tactic="exact h")
         self.assertTrue(state2.is_solved)
 
+        state1b = server.goal_tactic(state0, goal_id=0, tactic=TacticDraft("by\nhave h1 : Or p p := sorry\nsorry"))
+        self.assertEqual(state1b.goals, [
+            Goal(
+                [Variable(name="p", t="Prop")],
+                target="p ∨ p",
+            ),
+            Goal(
+                [
+                    Variable(name="p", t="Prop"),
+                    Variable(name="h1", t="p ∨ p"),
+                ],
+                target="p → p",
+            ),
+        ])
+
+
     def test_env_add_inspect(self):
         server = Server()
         server.env_add(
diff --git a/src b/src
index c1f63af..59935e3 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit c1f63af01920e5038298795e969c574994411329
+Subproject commit 59935e386bfdb7e2863a1a6d7a068db51a718465

From 3a4f2807c6575ab2773049c97f8e3af1e01e2db3 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 20 Jan 2025 12:03:21 -0800
Subject: [PATCH 4/9] chore: Update example

---
 examples/Example/lake-manifest.json | 22 +++++++++++-----------
 examples/Example/lakefile.lean      |  2 +-
 examples/sketch.py                  | 12 ++++++++++--
 3 files changed, 22 insertions(+), 14 deletions(-)

diff --git a/examples/Example/lake-manifest.json b/examples/Example/lake-manifest.json
index fe0adeb..1792824 100644
--- a/examples/Example/lake-manifest.json
+++ b/examples/Example/lake-manifest.json
@@ -1,25 +1,25 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover-community/aesop.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
-   "name": "batteries",
+   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop.git",
+   "inputRev": "v4.15.0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa",
-   "name": "aesop",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.12.0",
-   "inherited": false,
+   "inputRev": "v4.15.0",
+   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Example",
  "lakeDir": ".lake"}
diff --git a/examples/Example/lakefile.lean b/examples/Example/lakefile.lean
index a85cd79..40f8e92 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.12.0"
+  "https://github.com/leanprover-community/aesop.git" @ "v4.15.0"
 
 package Example
 
diff --git a/examples/sketch.py b/examples/sketch.py
index f8cad14..8ba19fc 100644
--- a/examples/sketch.py
+++ b/examples/sketch.py
@@ -1,9 +1,14 @@
 #!/usr/bin/env python3
 
 from pantograph.server import Server
+from pantograph.expr import TacticDraft
+
+root = """
+theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry
+"""
 
 sketch = """
-theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by
+by
    -- Consider some n and m in Nats.
    intros n m
    -- Perform induction on n.
@@ -32,5 +37,8 @@
 
 if __name__ == '__main__':
     server = Server()
-    unit, = server.load_sorry(sketch)
+    unit, = server.load_sorry(root)
     print(unit.goal_state)
+
+    sketch = server.goal_tactic(unit.goal_state, 0, TacticDraft(sketch))
+    print(sketch)

From 30689a7f3e78166c526c2f5498f8860a7d80c786 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 24 Jan 2025 15:03:47 -0800
Subject: [PATCH 5/9] feat: Add module read function

---
 pantograph/server.py | 11 +++++++++++
 src                  |  2 +-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/pantograph/server.py b/pantograph/server.py
index 77b87f3..9a298af 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -300,6 +300,17 @@ def env_inspect(
         if "error" in result:
             raise ServerError(result["desc"])
         return result
+    def env_module_read(self, module: str) -> dict:
+        """
+        Reads the content from one Lean module including what constants are in
+        it.
+        """
+        result = self.run('env.module_read', {
+            "module": module
+        })
+        if "error" in result:
+            raise ServerError(result["desc"])
+        return result
 
     def env_save(self, path: str):
         result = self.run('env.save', {
diff --git a/src b/src
index 59935e3..ed1d5d7 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit 59935e386bfdb7e2863a1a6d7a068db51a718465
+Subproject commit ed1d5d7b58a3d62250a769bb7703f7e11f65e931

From 3d45eebc81ed53cac10c6560ee144c4934f9875e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 26 Jan 2025 14:26:41 -0800
Subject: [PATCH 6/9] doc: Clean up old documentation

---
 README.md            | 12 +-----------
 pantograph/server.py | 35 +++++++++++++++++++++++++++++++++--
 2 files changed, 34 insertions(+), 13 deletions(-)

diff --git a/README.md b/README.md
index 6c290c7..5485820 100644
--- a/README.md
+++ b/README.md
@@ -31,17 +31,7 @@ python3 -m http.server -d .
 
 ## Examples
 
-For API interaction examples, see `examples/README.md`. The examples directory
-also contains a comprehensive Jupyter notebook.
-
-## Experiments
-
-In `experiments/`, there are some experiments:
-1. `minif2f` is an example of executing a `sglang` based prover on the miniF2F dataset
-2. `dsp` is an Lean implementation of Draft-Sketch-Prove
-
-The experiments should be run in `poetry shell`. The environment variable
-`OPENAI_API_KEY` must be set when running experiments calling the OpenAI API.
+For API interaction examples, see `examples/README.md`.
 
 ## Referencing
 
diff --git a/pantograph/server.py b/pantograph/server.py
index f35161f..fc65c68 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -44,7 +44,9 @@ class ServerError(Exception):
 
 class Server:
     """
-    Main interaction instance with Pantograph
+    Main interaction instance with Pantograph.
+
+    Asynchronous and synchronous versions are provided for each function.
     """
 
     def __init__(self,
@@ -354,6 +356,12 @@ async def load_sorry_async(self, content: str) -> List[CompilationUnit]:
     load_sorry = to_sync(load_sorry_async)
 
     async def env_add_async(self, name: str, t: Expr, v: Expr, is_theorem: bool = True):
+        """
+        Adds a definition to the environment.
+
+        NOTE: May have to accept additional parameters if the definition
+        contains universe mvars.
+        """
         result = await self.run_async('env.add', {
             "name": name,
             "type": t,
@@ -371,6 +379,9 @@ async def env_inspect_async(
             name: str,
             print_value: bool = False,
             print_dependency: bool = False) -> Dict:
+        """
+        Print the type and dependencies of a constant.
+        """
         result = await self.run_async('env.inspect', {
             "name": name,
             "value": print_value,
@@ -396,6 +407,9 @@ async def env_module_read_async(self, module: str) -> dict:
     env_module_read = to_sync(env_module_read_async)
 
     async def env_save_async(self, path: str):
+        """
+        Save the current environment to a file
+        """
         result = await self.run_async('env.save', {
             "path": path,
         })
@@ -404,6 +418,9 @@ async def env_save_async(self, path: str):
     env_save = to_sync(env_save_async)
 
     async def env_load_async(self, path: str):
+        """
+        Load the current environment from a file
+        """
         result = await self.run_async('env.load', {
             "path": path,
         })
@@ -413,6 +430,9 @@ async def env_load_async(self, path: str):
     env_load = to_sync(env_load_async)
 
     async def goal_save_async(self, goal_state: GoalState, path: str):
+        """
+        Save a goal state to a file
+        """
         result = await self.run_async('goal.save', {
             "id": goal_state.state_id,
             "path": path,
@@ -423,6 +443,11 @@ async def goal_save_async(self, goal_state: GoalState, path: str):
     goal_save = to_sync(goal_save_async)
 
     async def goal_load_async(self, path: str) -> GoalState:
+        """
+        Load a goal state from a file.
+
+        User is responsible for keeping track of the environment.
+        """
         result = await self.run_async('goal.load', {
             "path": path,
         })
@@ -440,7 +465,10 @@ async def goal_load_async(self, path: str) -> GoalState:
     goal_load = to_sync(goal_load_async)
 
 
-def get_version():
+def get_version() -> str:
+    """
+    Returns the current Pantograph version for diagnostics purposes.
+    """
     import subprocess
     with subprocess.Popen([_get_proc_path(), "--version"],
                           stdout=subprocess.PIPE,
@@ -451,6 +479,9 @@ def get_version():
 class TestServer(unittest.TestCase):
 
     def test_version(self):
+        """
+        NOTE: Update this after upstream updates.
+        """
         self.assertEqual(get_version(), "0.2.25")
 
     def test_server_init_del(self):

From 209368a8ed651a8c762c39879f458cc480b8f856 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 26 Jan 2025 22:11:07 -0800
Subject: [PATCH 7/9] chore: Update upstream

---
 src | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src b/src
index ed1d5d7..4d295bd 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit ed1d5d7b58a3d62250a769bb7703f7e11f65e931
+Subproject commit 4d295bd9ff04cbe27218f169ea0433eb2d4e8633

From e2aae43787a2f407b8f884fdd1b1ff1331c507b7 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 28 Jan 2025 17:44:34 -0800
Subject: [PATCH 8/9] chore: Update upstream

---
 src | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src b/src
index 4d295bd..4435a64 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit 4d295bd9ff04cbe27218f169ea0433eb2d4e8633
+Subproject commit 4435a6459cddc0661d39d2f370887eff007c94fd

From ec82b04e4a40b372e2d6c2135fab7efb17d428e5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 28 Jan 2025 17:45:37 -0800
Subject: [PATCH 9/9] doc: Update error signal in case of version mismatch

---
 pantograph/server.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pantograph/server.py b/pantograph/server.py
index fc65c68..0853049 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -161,7 +161,7 @@ async def restart_async(self):
         self.proc.setecho(False) # Do not send any command before this.
         try:
             ready = await self.proc.readline_async() # Reads the "ready."
-            assert ready.rstrip() == "ready.", f"Server failed to emit ready signal: {ready}; Maybe the project needs to be rebuilt"
+            assert ready.rstrip() == "ready.", f"Server failed to emit ready signal: {ready}; Project Lean version must match Pantograph's Lean version exactly or, it maybe needs to be rebuilt"
         except pexpect.exceptions.TIMEOUT as exc:
             raise RuntimeError("Server failed to emit ready signal in time") from exc