From 7c3b64562bdfd7a0d9cd796983291bb2a79fe9c9 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 17 May 2024 19:52:00 -0700
Subject: [PATCH 01/18] feat: Goal state garbage collection

---
 pantograph/expr.py   |  9 +++++++--
 pantograph/server.py | 39 +++++++++++++++++++++++++++++++++------
 2 files changed, 40 insertions(+), 8 deletions(-)

diff --git a/pantograph/expr.py b/pantograph/expr.py
index 4ae0367..dee9711 100644
--- a/pantograph/expr.py
+++ b/pantograph/expr.py
@@ -60,6 +60,11 @@ class GoalState:
     state_id: int
     goals: list[Goal]
 
+    _sentinel: list[int]
+
+    def __del__(self):
+        self._sentinel.append(self.state_id)
+
     @property
     def is_solved(self) -> bool:
         """
@@ -68,10 +73,10 @@ class GoalState:
         return not self.goals
 
     @staticmethod
-    def parse(payload: dict) -> Self:
+    def parse(payload: dict, _sentinel: list[int]) -> Self:
         state_id = payload["nextStateId"]
         goals = [Goal.parse(g) for g in payload["goals"]]
-        return GoalState(state_id, goals)
+        return GoalState(state_id, goals, _sentinel)
 
 @dataclass(frozen=True)
 class TacticHave:
diff --git a/pantograph/server.py b/pantograph/server.py
index 52a7661..19f087f 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -36,6 +36,9 @@ class Server:
         self.proc = None
         self.restart()
 
+        # List of goal states that should be garbage collected
+        self.to_remove_goal_states = []
+
     def restart(self):
         if self.proc is not None:
             self.proc.close()
@@ -48,14 +51,26 @@ class Server:
         self.proc.setecho(False)
 
     def run(self, cmd, payload):
+        """
+        Runs a raw JSON command. Preferably use one of the commands below.
+        """
         s = json.dumps(payload)
         self.proc.sendline(f"{cmd} {s}")
         try:
             self.proc.expect("{.*}\r\n", timeout=self.timeout)
             output = self.proc.match.group()
             return json.loads(output)
-        except pexpect.exceptions.TIMEOUT:
-            raise pexpect.exceptions.TIMEOUT
+        except pexpect.exceptions.TIMEOUT as exc:
+            raise exc
+
+    def gc(self):
+        """
+        Garbage collect deleted goal states.
+
+        Must be called periodically.
+        """
+        self.run('goal.delete', {'stateIds': self.to_remove_goal_states})
+        self.to_remove_goal_states.clear()
 
     def reset(self):
         return self.run("reset", {})
@@ -64,7 +79,7 @@ class Server:
         result = self.run('goal.start', {"expr": str(expr)})
         if "error" in result:
             raise ServerError(result["desc"])
-        return GoalState(state_id = result["stateId"], goals = [Goal.sentence(expr)])
+        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:
         args = {"stateId": state.state_id, "goalId": goal_id}
@@ -83,7 +98,7 @@ class Server:
             raise ServerError(result["tacticErrors"])
         if "parseError" in result:
             raise ServerError(result["parseError"])
-        return GoalState.parse(result)
+        return GoalState.parse(result, self.to_remove_goal_states)
 
     def goal_conv_begin(self, state: GoalState, goal_id: int) -> GoalState:
         result = self.run('goal.tactic', {"stateId": state.state_id, "goalId": goal_id, "conv": True})
@@ -93,7 +108,7 @@ class Server:
             raise ServerError(result["tacticErrors"])
         if "parseError" in result:
             raise ServerError(result["parseError"])
-        return GoalState.parse(result)
+        return GoalState.parse(result, self.to_remove_goal_states)
 
     def goal_conv_end(self, state: GoalState) -> GoalState:
         result = self.run('goal.tactic', {"stateId": state.state_id, "goalId": 0, "conv": False})
@@ -103,7 +118,7 @@ class Server:
             raise ServerError(result["tacticErrors"])
         if "parseError" in result:
             raise ServerError(result["parseError"])
-        return GoalState.parse(result)
+        return GoalState.parse(result, self.to_remove_goal_states)
 
 
 def get_version():
@@ -122,6 +137,7 @@ class TestServer(unittest.TestCase):
     def test_goal_start(self):
         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)
         state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a")
         self.assertEqual(state1.state_id, 1)
@@ -132,6 +148,17 @@ class TestServer(unittest.TestCase):
         )])
         self.assertEqual(str(state1.goals[0]),"a : Prop\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a")
 
+        del state0
+        self.assertEqual(len(server.to_remove_goal_states), 1)
+        server.gc()
+        self.assertEqual(len(server.to_remove_goal_states), 0)
+
+        state0b = server.goal_start("forall (p: Prop), p -> p")
+        del state0b
+        self.assertEqual(len(server.to_remove_goal_states), 1)
+        server.gc()
+        self.assertEqual(len(server.to_remove_goal_states), 0)
+
     def test_conv_calc(self):
         server = Server()
         state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")

From 553d4fb0e0684761cbedcf3be01be1434d1323ba Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 17 May 2024 19:58:16 -0700
Subject: [PATCH 02/18] feat: Typing of an expression

---
 pantograph/server.py | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/pantograph/server.py b/pantograph/server.py
index 19f087f..3281bd7 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -3,7 +3,7 @@ Class which manages a Pantograph instance. All calls to the kernel uses this
 interface.
 """
 import json, pexpect, pathlib, unittest
-from pantograph.expr import Variable, Goal, GoalState, \
+from pantograph.expr import parse_expr, Expr, Variable, Goal, GoalState, \
     Tactic, TacticHave, TacticCalc
 
 def _get_proc_cwd():
@@ -75,6 +75,16 @@ class Server:
     def reset(self):
         return self.run("reset", {})
 
+    def expr_type(self, expr: str) -> Expr:
+        """
+        Evaluate the type of a given expression. This gives an error if the
+        input `expr` is ill-formed.
+        """
+        result = self.run('expr.echo', {"expr": expr})
+        if "error" in result:
+            raise ServerError(result["desc"])
+        return parse_expr(result["type"])
+
     def goal_start(self, expr: str) -> GoalState:
         result = self.run('goal.start', {"expr": str(expr)})
         if "error" in result:
@@ -134,6 +144,11 @@ class TestServer(unittest.TestCase):
     def test_version(self):
         self.assertEqual(get_version(), "0.2.14")
 
+    def test_expr_type(self):
+        server = Server()
+        t = server.expr_type("forall (n m: Nat), n + m = m + n")
+        self.assertEqual(t, "Prop")
+
     def test_goal_start(self):
         server = Server()
         state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")

From 82eb649a517a21bb0f1cf3453b85920b13744010 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 17 May 2024 20:35:19 -0700
Subject: [PATCH 03/18] chore: Version bump of Pantograph

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

diff --git a/pantograph/server.py b/pantograph/server.py
index 3281bd7..3d30630 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -142,7 +142,7 @@ def get_version():
 class TestServer(unittest.TestCase):
 
     def test_version(self):
-        self.assertEqual(get_version(), "0.2.14")
+        self.assertEqual(get_version(), "0.2.15")
 
     def test_expr_type(self):
         server = Server()
diff --git a/src b/src
index f20ee8d..0aec757 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit f20ee8dc87ae3fa9c0f13040e1b4f097f1a40503
+Subproject commit 0aec757601a2aea9f9efabae7eda4300832f0021

From fceb0c1a206e858b829cd8ac72593fa6d3e168c5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 17 May 2024 20:45:29 -0700
Subject: [PATCH 04/18] example: Calling aesop (partial)

---
 examples/Example/.gitignore         |  3 +++
 examples/Example/Example.lean       |  1 +
 examples/Example/lake-manifest.json | 23 +++++++++++++++++++++++
 examples/Example/lakefile.lean      | 11 +++++++++++
 examples/Example/lean-toolchain     |  1 +
 examples/README.md                  | 14 ++++++++++++++
 examples/aesop.py                   | 14 ++++++++++++++
 7 files changed, 67 insertions(+)
 create mode 100644 examples/Example/.gitignore
 create mode 100644 examples/Example/Example.lean
 create mode 100644 examples/Example/lake-manifest.json
 create mode 100644 examples/Example/lakefile.lean
 create mode 100644 examples/Example/lean-toolchain
 create mode 100644 examples/README.md
 create mode 100755 examples/aesop.py

diff --git a/examples/Example/.gitignore b/examples/Example/.gitignore
new file mode 100644
index 0000000..1824d0c
--- /dev/null
+++ b/examples/Example/.gitignore
@@ -0,0 +1,3 @@
+/build
+/lakefile.olean
+/lake-packages/*
diff --git a/examples/Example/Example.lean b/examples/Example/Example.lean
new file mode 100644
index 0000000..eef5356
--- /dev/null
+++ b/examples/Example/Example.lean
@@ -0,0 +1 @@
+import Aesop
diff --git a/examples/Example/lake-manifest.json b/examples/Example/lake-manifest.json
new file mode 100644
index 0000000..06e1c0e
--- /dev/null
+++ b/examples/Example/lake-manifest.json
@@ -0,0 +1,23 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "3025cb124492b423070f20cf0a70636f757d117f",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.8.0-rc1",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "Example",
+ "lakeDir": ".lake"}
diff --git a/examples/Example/lakefile.lean b/examples/Example/lakefile.lean
new file mode 100644
index 0000000..0429d0d
--- /dev/null
+++ b/examples/Example/lakefile.lean
@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+require aesop from git
+  "https://github.com/leanprover-community/aesop.git" @ "v4.8.0-rc1"
+
+package «Example» where
+  -- add package configuration options here
+
+lean_lib «Example» where
+  -- add library configuration options here
diff --git a/examples/Example/lean-toolchain b/examples/Example/lean-toolchain
new file mode 100644
index 0000000..d8a6d7e
--- /dev/null
+++ b/examples/Example/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.8.0-rc1
diff --git a/examples/README.md b/examples/README.md
new file mode 100644
index 0000000..8924626
--- /dev/null
+++ b/examples/README.md
@@ -0,0 +1,14 @@
+# Usage Example
+
+This example showcases how to bind library dependencies and execute the `Aesop`
+tactic in Lean. First build the example project:
+``` sh
+pushd Example
+lake build
+popd
+```
+This would generate compiled `.olean` files. Then run the example
+``` sh
+python3 aesop.py
+```
+
diff --git a/examples/aesop.py b/examples/aesop.py
new file mode 100755
index 0000000..dd5ba84
--- /dev/null
+++ b/examples/aesop.py
@@ -0,0 +1,14 @@
+#!/usr/bin/env python3
+
+import subprocess
+from pathlib import Path
+from pantograph.server import Server
+
+def get_lean_path():
+    cwd = Path(__file__).parent.resolve() / 'Example'
+    p = subprocess.check_output(['lake', 'env', 'printenv', 'LEAN_PATH'], cwd=cwd)
+    return p
+
+if __name__ == '__main__':
+    lean_path = get_lean_path()
+    print(lean_path)

From aa315ad31e381886d2606de6a3a7dc5774d8445f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 17 May 2024 20:53:34 -0700
Subject: [PATCH 05/18] example: Calling aesop

---
 examples/Example/Example.lean  |  4 ++++
 examples/Example/lakefile.lean |  7 +++----
 examples/aesop.py              | 13 +++++++++----
 pantograph/server.py           | 14 +++++++++++---
 4 files changed, 27 insertions(+), 11 deletions(-)

diff --git a/examples/Example/Example.lean b/examples/Example/Example.lean
index eef5356..1a5e245 100644
--- a/examples/Example/Example.lean
+++ b/examples/Example/Example.lean
@@ -1 +1,5 @@
 import Aesop
+
+-- Ensure that Aesop is running
+example : α → α :=
+  by aesop
diff --git a/examples/Example/lakefile.lean b/examples/Example/lakefile.lean
index 0429d0d..52623f0 100644
--- a/examples/Example/lakefile.lean
+++ b/examples/Example/lakefile.lean
@@ -4,8 +4,7 @@ open Lake DSL
 require aesop from git
   "https://github.com/leanprover-community/aesop.git" @ "v4.8.0-rc1"
 
-package «Example» where
-  -- add package configuration options here
+package Example
 
-lean_lib «Example» where
-  -- add library configuration options here
+@[default_target]
+lean_lib Example
diff --git a/examples/aesop.py b/examples/aesop.py
index dd5ba84..3f074b8 100755
--- a/examples/aesop.py
+++ b/examples/aesop.py
@@ -4,11 +4,16 @@ import subprocess
 from pathlib import Path
 from pantograph.server import Server
 
-def get_lean_path():
+def get_project_and_lean_path():
     cwd = Path(__file__).parent.resolve() / 'Example'
     p = subprocess.check_output(['lake', 'env', 'printenv', 'LEAN_PATH'], cwd=cwd)
-    return p
+    return cwd, p
 
 if __name__ == '__main__':
-    lean_path = get_lean_path()
-    print(lean_path)
+    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)
+    state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
+    state1 = server.goal_tactic(state0, goal_id=0, tactic="aesop")
+    assert state1.is_solved
diff --git a/pantograph/server.py b/pantograph/server.py
index 3d30630..80e95f9 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -2,7 +2,7 @@
 Class which manages a Pantograph instance. All calls to the kernel uses this
 interface.
 """
-import json, pexpect, pathlib, unittest
+import json, pexpect, pathlib, unittest, os
 from pantograph.expr import parse_expr, Expr, Variable, Goal, GoalState, \
     Tactic, TacticHave, TacticCalc
 
@@ -18,6 +18,8 @@ class Server:
 
     def __init__(self,
                  imports=["Init"],
+                 project_path=None,
+                 lean_path=None,
                  options=[],
                  timeout=20,
                  maxread=1000000):
@@ -27,8 +29,9 @@ class Server:
         """
         self.timeout = timeout
         self.imports = imports
+        self.project_path = project_path if project_path else _get_proc_cwd()
+        self.lean_path = lean_path
         self.maxread = maxread
-        self.proc_cwd = _get_proc_cwd()
         self.proc_path = _get_proc_path()
 
         self.options = options
@@ -42,11 +45,16 @@ class Server:
     def restart(self):
         if self.proc is not None:
             self.proc.close()
+        env = os.environ
+        if self.lean_path:
+            env = env | {'LEAN_PATH': self.lean_path}
+
         self.proc = pexpect.spawn(
             f"{self.proc_path} {self.args}",
             encoding="utf-8",
             maxread=self.maxread,
-            cwd=self.proc_cwd,
+            cwd=self.project_path,
+            env=env,
         )
         self.proc.setecho(False)
 

From 926aaa436400c0b429f231987b0b8e9231914d41 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 17 May 2024 20:56:01 -0700
Subject: [PATCH 06/18] doc: Running example from project root

---
 examples/README.md | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/examples/README.md b/examples/README.md
index 8924626..8ccd495 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -7,8 +7,9 @@ pushd Example
 lake build
 popd
 ```
-This would generate compiled `.olean` files. Then run the example
+This would generate compiled `.olean` files. Then run the example from the
+project root:
 ``` sh
-python3 aesop.py
+poetry run examples/aesop.py
 ```
 

From cf85bb6901c310cbc6c59eaa3bcb4c78b5fd1709 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 17 May 2024 23:05:32 -0700
Subject: [PATCH 07/18] feat: GC only if there's something to gc

---
 pantograph/server.py | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/pantograph/server.py b/pantograph/server.py
index 80e95f9..63037c7 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -77,11 +77,9 @@ class Server:
 
         Must be called periodically.
         """
-        self.run('goal.delete', {'stateIds': self.to_remove_goal_states})
-        self.to_remove_goal_states.clear()
-
-    def reset(self):
-        return self.run("reset", {})
+        if self.to_remove_goal_states:
+            self.run('goal.delete', {'stateIds': self.to_remove_goal_states})
+            self.to_remove_goal_states.clear()
 
     def expr_type(self, expr: str) -> Expr:
         """

From 9993019b69b314deb28f2c8e60bcc6f6a369db68 Mon Sep 17 00:00:00 2001
From: ChuyueSun <chuyue99@gmail.com>
Date: Sun, 19 May 2024 18:59:03 -0700
Subject: [PATCH 08/18] update readme

---
 README.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/README.md b/README.md
index d44c1c2..f66d9f2 100644
--- a/README.md
+++ b/README.md
@@ -3,6 +3,10 @@
 Python interface to the Pantograph library
 
 ## Getting started
+Update submodule
+``` bash
+git submodule update --init
+```
 
 Execute
 ```bash

From fa7c4a89d34a864bc159240a3b53afca26eb1f62 Mon Sep 17 00:00:00 2001
From: ChuyueSun <chuyue99@gmail.com>
Date: Sun, 19 May 2024 19:16:05 -0700
Subject: [PATCH 09/18] add test_sglang

---
 test_sglang.py | 57 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 test_sglang.py

diff --git a/test_sglang.py b/test_sglang.py
new file mode 100644
index 0000000..34b8148
--- /dev/null
+++ b/test_sglang.py
@@ -0,0 +1,57 @@
+# copy pasted from https://docs.vllm.ai/en/latest/getting_started/quickstart.html
+
+# do export VLLM_USE_MODELSCOPE=True
+import argparse
+from typing import Dict, List
+import os
+import sglang as sgl
+from sglang import OpenAI, assistant, gen, set_default_backend, system, user
+
+
+def test_pytorch():
+    print('\n----- Test PyTorch ---')
+    # Print the PyTorch version and CUDA version
+    print(f"PyTorch version: {torch.__version__}")
+    print(f"CUDA version: {torch.version.cuda}")
+    
+    # Perform a matrix multiplication on CUDA and print the result
+    result = torch.randn(2, 4).cuda() @ torch.randn(4, 1).cuda()
+    print(f"Matrix multiplication result: {result}")
+    
+    # Check CUDA availability and device details
+    print(f'Number of CUDA devices: {torch.cuda.device_count()}')
+    if torch.cuda.device_count() > 0:
+        print(f'Device name: {torch.cuda.get_device_name(0)}')
+    else:
+        print("No CUDA devices available.")
+
+@sgl.function
+def multi_turn_question(s, question_1, question_2):
+    s += sgl.system("You are a helpful assistant.")
+    s += sgl.user(question_1)
+    s += sgl.assistant(sgl.gen("answer_1", max_tokens=256))
+    s += sgl.user(question_2)
+    s += sgl.assistant(sgl.gen("answer_2", max_tokens=256))
+
+
+
+def test_sglang():
+    print('\n----- Test sglang ---')
+    state = multi_turn_question.run(
+        question_1="What is the capital of the United States?",
+        question_2="List two local attractions.",
+    )
+
+    for m in state.messages():
+        print(m["role"], ":", m["content"])
+
+    print("\n-- answer_1 --\n", state["answer_1"])
+
+
+if __name__ == "__main__":
+    import time
+    start_time = time.time()
+    sgl.set_default_backend(sgl.OpenAI("gpt-4"))
+
+    test_sglang()
+    print(f"Time taken: {time.time() - start_time:.2f} seconds, or {(time.time() - start_time) / 60:.2f} minutes, or {(time.time() - start_time) / 3600:.2f} hours.\a")
\ No newline at end of file

From 9ef093c9e2c0b657803d14de82b5cec08b401223 Mon Sep 17 00:00:00 2001
From: ChuyueSun <chuyue99@gmail.com>
Date: Sun, 19 May 2024 19:17:05 -0700
Subject: [PATCH 10/18] update

---
 test_sglang.py | 19 +------------------
 1 file changed, 1 insertion(+), 18 deletions(-)

diff --git a/test_sglang.py b/test_sglang.py
index 34b8148..6b68cc8 100644
--- a/test_sglang.py
+++ b/test_sglang.py
@@ -1,6 +1,5 @@
-# copy pasted from https://docs.vllm.ai/en/latest/getting_started/quickstart.html
 
-# do export VLLM_USE_MODELSCOPE=True
+
 import argparse
 from typing import Dict, List
 import os
@@ -8,22 +7,6 @@ import sglang as sgl
 from sglang import OpenAI, assistant, gen, set_default_backend, system, user
 
 
-def test_pytorch():
-    print('\n----- Test PyTorch ---')
-    # Print the PyTorch version and CUDA version
-    print(f"PyTorch version: {torch.__version__}")
-    print(f"CUDA version: {torch.version.cuda}")
-    
-    # Perform a matrix multiplication on CUDA and print the result
-    result = torch.randn(2, 4).cuda() @ torch.randn(4, 1).cuda()
-    print(f"Matrix multiplication result: {result}")
-    
-    # Check CUDA availability and device details
-    print(f'Number of CUDA devices: {torch.cuda.device_count()}')
-    if torch.cuda.device_count() > 0:
-        print(f'Device name: {torch.cuda.get_device_name(0)}')
-    else:
-        print("No CUDA devices available.")
 
 @sgl.function
 def multi_turn_question(s, question_1, question_2):

From 095180589b8972fae85a0744d18a31311ab08aa0 Mon Sep 17 00:00:00 2001
From: ChuyueSun <chuyue99@gmail.com>
Date: Mon, 20 May 2024 00:02:33 -0700
Subject: [PATCH 11/18] add conv_sgl tests

---
 .gitignore           |   1 +
 .gitmodules          |   1 +
 pantograph/server.py | 155 ++++++++++++++++++++++++++++++++++++++++++-
 3 files changed, 156 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 4bd6cec..670b156 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,6 +7,7 @@
 
 # Output
 /dist
+/venv
 
 pantograph/pantograph
 pantograph/lean-toolchain
diff --git a/.gitmodules b/.gitmodules
index caa4dcb..6b49ada 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +1,4 @@
 [submodule "src"]
 	path = src
 	url = https://git.leni.sh/aniva/Pantograph.git
+	
\ No newline at end of file
diff --git a/pantograph/server.py b/pantograph/server.py
index 52a7661..86c11ad 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -6,6 +6,41 @@ import json, pexpect, pathlib, unittest
 from pantograph.expr import Variable, Goal, GoalState, \
     Tactic, TacticHave, TacticCalc
 
+
+import argparse
+from typing import Dict, List
+import os
+import sglang as sgl
+
+
+
+
+@sgl.function
+def multi_turn_question(s, question_1, question_2):
+    s += sgl.system("You are a helpful assistant.")
+    s += sgl.user(question_1)
+    s += sgl.assistant(sgl.gen("answer_1", max_tokens=256))
+    s += sgl.user(question_2)
+    s += sgl.assistant(sgl.gen("answer_2", max_tokens=256))
+
+
+@sgl.function
+def select_tactic(s, state):
+    s += sgl.system("You are an expert in Lean. Choose the next one tactic to run given the current proof state and goals.")
+    s += sgl.user("The current proof state: GoalState(state_id=0, goals=[Goal(variables=[], target='∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b', name=None, is_conversion=False)])")
+    s += sgl.assistant("```intros a b h```")
+    s += sgl.user("The current proof state: GoalState(state_id=1, goals=[Goal(variables=[Variable(t='Nat', v=None, name='a'), Variable(t='Nat', v=None, name='b'), Variable(t='b = 2', v=None, name='h')], target='1 + a + 1 = a + b', name=None, is_conversion=False)])")
+    s += sgl.assistant('TacticCalc("1 + a + 1 = a + 1 + 1")')
+    s += sgl.user("The current proof state: " + str(state))
+    with s.copy() as tmp:
+        tmp += sgl.assistant(sgl.gen("tactic", max_tokens=64))
+        print("==tmp===")
+        print(tmp["tactic"])
+        tactic = extract_code_from_llm_output(tmp["tactic"])
+    s += sgl.assistant("```"+tactic+"```")
+
+
+
 def _get_proc_cwd():
     return pathlib.Path(__file__).parent
 def _get_proc_path():
@@ -112,7 +147,21 @@ def get_version():
                           stdout=subprocess.PIPE,
                           cwd=_get_proc_cwd()) as p:
         return p.communicate()[0].decode('utf-8').strip()
-
+    
+def extract_code_from_llm_output(reply):
+    i = reply.find("```lean")
+    if i != -1:
+        reply = reply[i + 7:]
+        i = reply.find("```")
+        reply = reply[:i]
+        return reply
+    i = reply.find("```")
+    if i != -1:
+        reply = reply[i + 3:]
+        i = reply.find("```")
+        reply = reply[:i]
+        return reply
+    return reply
 
 class TestServer(unittest.TestCase):
 
@@ -132,6 +181,75 @@ class TestServer(unittest.TestCase):
         )])
         self.assertEqual(str(state1.goals[0]),"a : Prop\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a")
 
+    def test_conv_calc_sgl(self):
+        sgl.set_default_backend(sgl.OpenAI("gpt-4"))
+
+        server = Server()
+        state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
+        print("==========state0============")
+        print(state0)
+        variables = [
+            Variable(name="a", t="Nat"),
+            Variable(name="b", t="Nat"),
+            Variable(name="h", t="b = 2"),
+        ]
+
+        state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a b h")
+        print("==========state1============")
+        print(state1)
+        state2 = server.goal_tactic(state1, goal_id=0, tactic=TacticCalc("1 + a + 1 = a + 1 + 1"))
+        print("==========state2============")
+        print(state2)
+        self.assertEqual(state2.goals, [
+            Goal(
+                variables,
+                target="1 + a + 1 = a + 1 + 1",
+                name='calc',
+            ),
+            Goal(
+                variables,
+                target="a + 1 + 1 = a + b",
+            ),
+        ])
+        state = select_tactic.run(str(state2))
+        for m in state.messages():
+            print(m["role"], ":", m["content"])
+
+        print("\n-- tactic --\n", state.stream_executor.variables)
+        print(state.stream_executor.arguments)
+
+
+        # print("==========state2============")
+        # print(state2)
+        # state_c1 = server.goal_conv_begin(state2, goal_id=0)
+        # print("==========state c1============")
+        # print(state_c1)
+        # state_c2 = server.goal_tactic(state_c1, goal_id=0, tactic="rhs")
+        # print("==========state c2============")
+        # print(state_c2)
+        # state_c3 = server.goal_tactic(state_c2, goal_id=0, tactic="rw [Nat.add_comm]")
+        # print("==========state c3============")
+        # print(state_c3)
+        # state_c4 = server.goal_conv_end(state_c3)
+        # print("==========state c4============")
+        # print(state_c4)
+
+        # state_c5 = server.goal_tactic(state_c4, goal_id=0, tactic="rfl")
+        # print("==========state c5============")
+        # print(state_c5)
+        # self.assertTrue(state_c5.is_solved)
+
+        # print()
+
+        # state3 = server.goal_tactic(state2, goal_id=1, tactic=TacticCalc("_ = a + 2"))
+        # print("==========state3============")
+        # print(state3)
+        # state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
+        # print("==========state4============")
+        # print(state4)        
+        # self.assertTrue(state4.is_solved)
+
+
     def test_conv_calc(self):
         server = Server()
         state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
@@ -154,17 +272,52 @@ class TestServer(unittest.TestCase):
                 target="a + 1 + 1 = a + b",
             ),
         ])
+        print("==========state2============")
+        print(state2)
         state_c1 = server.goal_conv_begin(state2, goal_id=0)
+        print("==========state c1============")
+        print(state_c1)
         state_c2 = server.goal_tactic(state_c1, goal_id=0, tactic="rhs")
+        print("==========state c2============")
+        print(state_c2)
         state_c3 = server.goal_tactic(state_c2, goal_id=0, tactic="rw [Nat.add_comm]")
+        print("==========state c3============")
+        print(state_c3)
         state_c4 = server.goal_conv_end(state_c3)
+        print("==========state c4============")
+        print(state_c4)
+
         state_c5 = server.goal_tactic(state_c4, goal_id=0, tactic="rfl")
+        print("==========state c5============")
+        print(state_c5)
         self.assertTrue(state_c5.is_solved)
+        
+        print()
 
         state3 = server.goal_tactic(state2, goal_id=1, tactic=TacticCalc("_ = a + 2"))
+        print("==========state3============")
+        print(state3)
         state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
+        print("==========state4============")
+        print(state4)        
         self.assertTrue(state4.is_solved)
 
+    def test_sglang_openai(self):
+        sgl.set_default_backend(sgl.OpenAI("gpt-4"))
 
+        print('\n----- Test sglang ---')
+        state = multi_turn_question.run(
+            question_1="What is the capital of the United States?",
+            question_2="List two local attractions.",
+        )
+
+        for m in state.messages():
+            print(m["role"], ":", m["content"])
+
+        print("\n-- answer_1 --\n", state["answer_1"])
+
+   
 if __name__ == '__main__':
+
     unittest.main()
+

From 67b3ec969bd7c9982fe58f38f3c5e16a3191ea23 Mon Sep 17 00:00:00 2001
From: ChuyueSun <chuyue99@gmail.com>
Date: Mon, 20 May 2024 00:26:52 -0700
Subject: [PATCH 12/18] apply sgl tactic

---
 pantograph/server.py | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/pantograph/server.py b/pantograph/server.py
index 86c11ad..633913e 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -38,6 +38,7 @@ def select_tactic(s, state):
         print(tmp["tactic"])
         tactic = extract_code_from_llm_output(tmp["tactic"])
     s += sgl.assistant("```"+tactic+"```")
+    return tactic
 
 
 
@@ -212,11 +213,19 @@ class TestServer(unittest.TestCase):
             ),
         ])
         state = select_tactic.run(str(state2))
+        tactic = state.ret_value
         for m in state.messages():
             print(m["role"], ":", m["content"])
 
         print("\n-- tactic --\n", state.stream_executor.variables)
-        print(state.stream_executor.arguments)
+        
+        state3 = server.goal_tactic(state2, goal_id=1, tactic=tactic)
+        print("==========state3============")
+        print(state3)
+        # state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
+        # print("==========state4============")
+        # print(state4)        
+        # self.assertTrue(state4.is_solved)
 
 
         # print("==========state2============")
@@ -241,13 +250,6 @@ class TestServer(unittest.TestCase):
 
         # print()
 
-        # state3 = server.goal_tactic(state2, goal_id=1, tactic=TacticCalc("_ = a + 2"))
-        # print("==========state3============")
-        # print(state3)
-        # state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
-        # print("==========state4============")
-        # print(state4)        
-        # self.assertTrue(state4.is_solved)
 
 
     def test_conv_calc(self):

From 46459763bebae7ebedfb71543a4879722952585e Mon Sep 17 00:00:00 2001
From: ChuyueSun <chuyue99@gmail.com>
Date: Mon, 20 May 2024 18:06:15 -0700
Subject: [PATCH 13/18] refactor

---
 pantograph/gen_tactic.py | 140 ++++++++++++++++++++++++++++++++++
 pantograph/server.py     | 159 +--------------------------------------
 2 files changed, 142 insertions(+), 157 deletions(-)
 create mode 100644 pantograph/gen_tactic.py

diff --git a/pantograph/gen_tactic.py b/pantograph/gen_tactic.py
new file mode 100644
index 0000000..68c7ccb
--- /dev/null
+++ b/pantograph/gen_tactic.py
@@ -0,0 +1,140 @@
+from pantograph.server import Server
+from pantograph.expr import Variable, Goal, TacticCalc
+import  unittest
+import sglang as sgl
+
+
+
+
+@sgl.function
+def multi_turn_question(s, question_1, question_2):
+    s += sgl.system("You are a helpful assistant.")
+    s += sgl.user(question_1)
+    s += sgl.assistant(sgl.gen("answer_1", max_tokens=256))
+    s += sgl.user(question_2)
+    s += sgl.assistant(sgl.gen("answer_2", max_tokens=256))
+
+
+@sgl.function
+def select_tactic(s, state):
+    s += sgl.system("You are an expert in Lean. Choose the next one tactic to run given the current proof state and goals.")
+    s += sgl.user("The current proof state: GoalState(state_id=0, goals=[Goal(variables=[], target='∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b', name=None, is_conversion=False)])")
+    s += sgl.assistant("```intros a b h```")
+    s += sgl.user("The current proof state: GoalState(state_id=1, goals=[Goal(variables=[Variable(t='Nat', v=None, name='a'), Variable(t='Nat', v=None, name='b'), Variable(t='b = 2', v=None, name='h')], target='1 + a + 1 = a + b', name=None, is_conversion=False)])")
+    s += sgl.assistant('TacticCalc("1 + a + 1 = a + 1 + 1")')
+    s += sgl.user("The current proof state: " + str(state))
+    with s.copy() as tmp:
+        tmp += sgl.assistant(sgl.gen("tactic", max_tokens=64))
+        print("==tmp===")
+        print(tmp["tactic"])
+        tactic = extract_code_from_llm_output(tmp["tactic"])
+    s += sgl.assistant("```"+tactic+"```")
+    return tactic
+
+
+    
+def extract_code_from_llm_output(reply):
+    i = reply.find("```lean")
+    if i != -1:
+        reply = reply[i + 7:]
+        i = reply.find("```")
+        reply = reply[:i]
+        return reply
+    i = reply.find("```")
+    if i != -1:
+        reply = reply[i + 3:]
+        i = reply.find("```")
+        reply = reply[:i]
+        return reply
+    return reply
+
+class TestServerSGL(unittest.TestCase):
+
+    def test_conv_calc_sgl(self):
+        sgl.set_default_backend(sgl.OpenAI("gpt-4"))
+
+        server = Server()
+        state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
+        print("==========state0============")
+        print(state0)
+        variables = [
+            Variable(name="a", t="Nat"),
+            Variable(name="b", t="Nat"),
+            Variable(name="h", t="b = 2"),
+        ]
+
+        state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a b h")
+        print("==========state1============")
+        print(state1)
+        state2 = server.goal_tactic(state1, goal_id=0, tactic=TacticCalc("1 + a + 1 = a + 1 + 1"))
+        print("==========state2============")
+        print(state2)
+        self.assertEqual(state2.goals, [
+            Goal(
+                variables,
+                target="1 + a + 1 = a + 1 + 1",
+                name='calc',
+            ),
+            Goal(
+                variables,
+                target="a + 1 + 1 = a + b",
+            ),
+        ])
+        state = select_tactic.run(str(state2))
+        tactic = state.ret_value
+        for m in state.messages():
+            print(m["role"], ":", m["content"])
+
+        print("\n-- tactic --\n", tactic)
+        
+        state3 = server.goal_tactic(state2, goal_id=1, tactic=tactic)
+        print("==========state3============")
+        print(state3)
+        # state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
+        # print("==========state4============")
+        # print(state4)        
+        # self.assertTrue(state4.is_solved)
+
+
+        # print("==========state2============")
+        # print(state2)
+        # state_c1 = server.goal_conv_begin(state2, goal_id=0)
+        # print("==========state c1============")
+        # print(state_c1)
+        # state_c2 = server.goal_tactic(state_c1, goal_id=0, tactic="rhs")
+        # print("==========state c2============")
+        # print(state_c2)
+        # state_c3 = server.goal_tactic(state_c2, goal_id=0, tactic="rw [Nat.add_comm]")
+        # print("==========state c3============")
+        # print(state_c3)
+        # state_c4 = server.goal_conv_end(state_c3)
+        # print("==========state c4============")
+        # print(state_c4)
+
+        # state_c5 = server.goal_tactic(state_c4, goal_id=0, tactic="rfl")
+        # print("==========state c5============")
+        # print(state_c5)
+        # self.assertTrue(state_c5.is_solved)
+
+        # print()
+
+
+    def test_sglang_openai(self):
+        sgl.set_default_backend(sgl.OpenAI("gpt-4"))
+
+        print('\n----- Test sglang ---')
+        state = multi_turn_question.run(
+            question_1="What is the capital of the United States?",
+            question_2="List two local attractions.",
+        )
+
+        for m in state.messages():
+            print(m["role"], ":", m["content"])
+
+        print("\n-- answer_1 --\n", state["answer_1"])
+
+   
+if __name__ == '__main__':
+
+    unittest.main()
+
diff --git a/pantograph/server.py b/pantograph/server.py
index 633913e..f652fbb 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -6,42 +6,6 @@ import json, pexpect, pathlib, unittest
 from pantograph.expr import Variable, Goal, GoalState, \
     Tactic, TacticHave, TacticCalc
 
-
-import argparse
-from typing import Dict, List
-import os
-import sglang as sgl
-
-
-
-
-@sgl.function
-def multi_turn_question(s, question_1, question_2):
-    s += sgl.system("You are a helpful assistant.")
-    s += sgl.user(question_1)
-    s += sgl.assistant(sgl.gen("answer_1", max_tokens=256))
-    s += sgl.user(question_2)
-    s += sgl.assistant(sgl.gen("answer_2", max_tokens=256))
-
-
-@sgl.function
-def select_tactic(s, state):
-    s += sgl.system("You are an expert in Lean. Choose the next one tactic to run given the current proof state and goals.")
-    s += sgl.user("The current proof state: GoalState(state_id=0, goals=[Goal(variables=[], target='∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b', name=None, is_conversion=False)])")
-    s += sgl.assistant("```intros a b h```")
-    s += sgl.user("The current proof state: GoalState(state_id=1, goals=[Goal(variables=[Variable(t='Nat', v=None, name='a'), Variable(t='Nat', v=None, name='b'), Variable(t='b = 2', v=None, name='h')], target='1 + a + 1 = a + b', name=None, is_conversion=False)])")
-    s += sgl.assistant('TacticCalc("1 + a + 1 = a + 1 + 1")')
-    s += sgl.user("The current proof state: " + str(state))
-    with s.copy() as tmp:
-        tmp += sgl.assistant(sgl.gen("tactic", max_tokens=64))
-        print("==tmp===")
-        print(tmp["tactic"])
-        tactic = extract_code_from_llm_output(tmp["tactic"])
-    s += sgl.assistant("```"+tactic+"```")
-    return tactic
-
-
-
 def _get_proc_cwd():
     return pathlib.Path(__file__).parent
 def _get_proc_path():
@@ -148,21 +112,7 @@ def get_version():
                           stdout=subprocess.PIPE,
                           cwd=_get_proc_cwd()) as p:
         return p.communicate()[0].decode('utf-8').strip()
-    
-def extract_code_from_llm_output(reply):
-    i = reply.find("```lean")
-    if i != -1:
-        reply = reply[i + 7:]
-        i = reply.find("```")
-        reply = reply[:i]
-        return reply
-    i = reply.find("```")
-    if i != -1:
-        reply = reply[i + 3:]
-        i = reply.find("```")
-        reply = reply[:i]
-        return reply
-    return reply
+
 
 class TestServer(unittest.TestCase):
 
@@ -182,76 +132,6 @@ class TestServer(unittest.TestCase):
         )])
         self.assertEqual(str(state1.goals[0]),"a : Prop\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a")
 
-    def test_conv_calc_sgl(self):
-        sgl.set_default_backend(sgl.OpenAI("gpt-4"))
-
-        server = Server()
-        state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
-        print("==========state0============")
-        print(state0)
-        variables = [
-            Variable(name="a", t="Nat"),
-            Variable(name="b", t="Nat"),
-            Variable(name="h", t="b = 2"),
-        ]
-
-        state1 = server.goal_tactic(state0, goal_id=0, tactic="intro a b h")
-        print("==========state1============")
-        print(state1)
-        state2 = server.goal_tactic(state1, goal_id=0, tactic=TacticCalc("1 + a + 1 = a + 1 + 1"))
-        print("==========state2============")
-        print(state2)
-        self.assertEqual(state2.goals, [
-            Goal(
-                variables,
-                target="1 + a + 1 = a + 1 + 1",
-                name='calc',
-            ),
-            Goal(
-                variables,
-                target="a + 1 + 1 = a + b",
-            ),
-        ])
-        state = select_tactic.run(str(state2))
-        tactic = state.ret_value
-        for m in state.messages():
-            print(m["role"], ":", m["content"])
-
-        print("\n-- tactic --\n", state.stream_executor.variables)
-        
-        state3 = server.goal_tactic(state2, goal_id=1, tactic=tactic)
-        print("==========state3============")
-        print(state3)
-        # state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
-        # print("==========state4============")
-        # print(state4)        
-        # self.assertTrue(state4.is_solved)
-
-
-        # print("==========state2============")
-        # print(state2)
-        # state_c1 = server.goal_conv_begin(state2, goal_id=0)
-        # print("==========state c1============")
-        # print(state_c1)
-        # state_c2 = server.goal_tactic(state_c1, goal_id=0, tactic="rhs")
-        # print("==========state c2============")
-        # print(state_c2)
-        # state_c3 = server.goal_tactic(state_c2, goal_id=0, tactic="rw [Nat.add_comm]")
-        # print("==========state c3============")
-        # print(state_c3)
-        # state_c4 = server.goal_conv_end(state_c3)
-        # print("==========state c4============")
-        # print(state_c4)
-
-        # state_c5 = server.goal_tactic(state_c4, goal_id=0, tactic="rfl")
-        # print("==========state c5============")
-        # print(state_c5)
-        # self.assertTrue(state_c5.is_solved)
-
-        # print()
-
-
-
     def test_conv_calc(self):
         server = Server()
         state0 = server.goal_start("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b")
@@ -274,52 +154,17 @@ class TestServer(unittest.TestCase):
                 target="a + 1 + 1 = a + b",
             ),
         ])
-        print("==========state2============")
-        print(state2)
         state_c1 = server.goal_conv_begin(state2, goal_id=0)
-        print("==========state c1============")
-        print(state_c1)
         state_c2 = server.goal_tactic(state_c1, goal_id=0, tactic="rhs")
-        print("==========state c2============")
-        print(state_c2)
         state_c3 = server.goal_tactic(state_c2, goal_id=0, tactic="rw [Nat.add_comm]")
-        print("==========state c3============")
-        print(state_c3)
         state_c4 = server.goal_conv_end(state_c3)
-        print("==========state c4============")
-        print(state_c4)
-
         state_c5 = server.goal_tactic(state_c4, goal_id=0, tactic="rfl")
-        print("==========state c5============")
-        print(state_c5)
         self.assertTrue(state_c5.is_solved)
-        
-        print()
 
         state3 = server.goal_tactic(state2, goal_id=1, tactic=TacticCalc("_ = a + 2"))
-        print("==========state3============")
-        print(state3)
         state4 = server.goal_tactic(state3, goal_id=0, tactic="rw [Nat.add_assoc]")
-        print("==========state4============")
-        print(state4)        
         self.assertTrue(state4.is_solved)
 
-    def test_sglang_openai(self):
-        sgl.set_default_backend(sgl.OpenAI("gpt-4"))
 
-        print('\n----- Test sglang ---')
-        state = multi_turn_question.run(
-            question_1="What is the capital of the United States?",
-            question_2="List two local attractions.",
-        )
-
-        for m in state.messages():
-            print(m["role"], ":", m["content"])
-
-        print("\n-- answer_1 --\n", state["answer_1"])
-
-   
 if __name__ == '__main__':
-
-    unittest.main()
-
+    unittest.main()
\ No newline at end of file

From 8c2f27681ca696125a78aa5954a6cfc2807a472e Mon Sep 17 00:00:00 2001
From: ChuyueSun <chuyue99@gmail.com>
Date: Mon, 20 May 2024 18:06:59 -0700
Subject: [PATCH 14/18] remove unused

---
 test_sglang.py | 40 ----------------------------------------
 1 file changed, 40 deletions(-)
 delete mode 100644 test_sglang.py

diff --git a/test_sglang.py b/test_sglang.py
deleted file mode 100644
index 6b68cc8..0000000
--- a/test_sglang.py
+++ /dev/null
@@ -1,40 +0,0 @@
-
-
-import argparse
-from typing import Dict, List
-import os
-import sglang as sgl
-from sglang import OpenAI, assistant, gen, set_default_backend, system, user
-
-
-
-@sgl.function
-def multi_turn_question(s, question_1, question_2):
-    s += sgl.system("You are a helpful assistant.")
-    s += sgl.user(question_1)
-    s += sgl.assistant(sgl.gen("answer_1", max_tokens=256))
-    s += sgl.user(question_2)
-    s += sgl.assistant(sgl.gen("answer_2", max_tokens=256))
-
-
-
-def test_sglang():
-    print('\n----- Test sglang ---')
-    state = multi_turn_question.run(
-        question_1="What is the capital of the United States?",
-        question_2="List two local attractions.",
-    )
-
-    for m in state.messages():
-        print(m["role"], ":", m["content"])
-
-    print("\n-- answer_1 --\n", state["answer_1"])
-
-
-if __name__ == "__main__":
-    import time
-    start_time = time.time()
-    sgl.set_default_backend(sgl.OpenAI("gpt-4"))
-
-    test_sglang()
-    print(f"Time taken: {time.time() - start_time:.2f} seconds, or {(time.time() - start_time) / 60:.2f} minutes, or {(time.time() - start_time) / 3600:.2f} hours.\a")
\ No newline at end of file

From d973c9e300177c3fa122815da9f88dc38d2f3f0b Mon Sep 17 00:00:00 2001
From: ChuyueSun <chuyue99@gmail.com>
Date: Tue, 21 May 2024 22:15:45 -0700
Subject: [PATCH 15/18] support py3.10

---
 pantograph/expr.py | 10 +++++-----
 poetry.lock        | 18 +++++++-----------
 2 files changed, 12 insertions(+), 16 deletions(-)

diff --git a/pantograph/expr.py b/pantograph/expr.py
index dee9711..6c54241 100644
--- a/pantograph/expr.py
+++ b/pantograph/expr.py
@@ -2,7 +2,7 @@
 Data structuers for expressions and goals
 """
 from dataclasses import dataclass
-from typing import Optional, Self, Union
+from typing import Optional, Union
 
 Expr = str
 
@@ -16,7 +16,7 @@ class Variable:
     name: Optional[str] = None
 
     @staticmethod
-    def parse(payload: dict) -> Self:
+    def parse(payload: dict):
         name = payload.get("userName")
         t = parse_expr(payload["type"])
         v = payload.get("value")
@@ -39,11 +39,11 @@ class Goal:
     is_conversion: bool = False
 
     @staticmethod
-    def sentence(target: Expr) -> Self:
+    def sentence(target: Expr):
         return Goal(variables=[], target=target)
 
     @staticmethod
-    def parse(payload: dict) -> Self:
+    def parse(payload: dict):
         name = payload.get("userName")
         variables = [Variable.parse(v) for v in payload["vars"]]
         target = parse_expr(payload["target"])
@@ -73,7 +73,7 @@ class GoalState:
         return not self.goals
 
     @staticmethod
-    def parse(payload: dict, _sentinel: list[int]) -> Self:
+    def parse(payload: dict, _sentinel: list[int]):
         state_id = payload["nextStateId"]
         goals = [Goal.parse(g) for g in payload["goals"]]
         return GoalState(state_id, goals, _sentinel)
diff --git a/poetry.lock b/poetry.lock
index 261ace1..be1c94f 100644
--- a/poetry.lock
+++ b/poetry.lock
@@ -1,15 +1,10 @@
-# This file is automatically @generated by Poetry 1.8.2 and should not be changed by hand.
-
 [[package]]
 name = "pexpect"
 version = "4.9.0"
 description = "Pexpect allows easy control of interactive console applications."
+category = "main"
 optional = false
 python-versions = "*"
-files = [
-    {file = "pexpect-4.9.0-py2.py3-none-any.whl", hash = "sha256:7236d1e080e4936be2dc3e326cec0af72acf9212a7e1d060210e70a47e253523"},
-    {file = "pexpect-4.9.0.tar.gz", hash = "sha256:ee7d41123f3c9911050ea2c2dac107568dc43b2d3b0c7557a33212c398ead30f"},
-]
 
 [package.dependencies]
 ptyprocess = ">=0.5"
@@ -18,14 +13,15 @@ ptyprocess = ">=0.5"
 name = "ptyprocess"
 version = "0.7.0"
 description = "Run a subprocess in a pseudo terminal"
+category = "main"
 optional = false
 python-versions = "*"
-files = [
-    {file = "ptyprocess-0.7.0-py2.py3-none-any.whl", hash = "sha256:4b41f3967fce3af57cc7e94b888626c18bf37a083e3651ca8feeb66d492fef35"},
-    {file = "ptyprocess-0.7.0.tar.gz", hash = "sha256:5c5d0a3b48ceee0b48485e0c26037c0acd7d29765ca3fbb5cb3831d347423220"},
-]
 
 [metadata]
-lock-version = "2.0"
+lock-version = "1.1"
 python-versions = "^3.11"
 content-hash = "aaae6d4832f97d9ad1b145776be94a2c44a7e77068bb1b3a05241a81dde23909"
+
+[metadata.files]
+pexpect = []
+ptyprocess = []

From 1e5a9c0fb4f0c382a550739b5acc44a3623b7929 Mon Sep 17 00:00:00 2001
From: Chuyue Sun <chuyue99@gmail.com>
Date: Fri, 24 May 2024 21:34:55 -0700
Subject: [PATCH 16/18] change pyproject toml to python3.10

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

diff --git a/pyproject.toml b/pyproject.toml
index 1450528..83ba788 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -7,7 +7,7 @@ license = "GPL-3"
 readme = "README.md"
 
 [tool.poetry.dependencies]
-python = "^3.11"
+python = "^3.10"
 pexpect = "^4.9.0"
 
 [tool.poetry.build]

From 516a93851ac3231448af552f508f333dd80c457b Mon Sep 17 00:00:00 2001
From: Chuyue Sun <chuyue99@gmail.com>
Date: Fri, 24 May 2024 22:42:32 -0700
Subject: [PATCH 17/18] update readme

---
 README.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/README.md b/README.md
index f66d9f2..5d02305 100644
--- a/README.md
+++ b/README.md
@@ -7,6 +7,10 @@ Update submodule
 ``` bash
 git submodule update --init
 ```
+Install dependencies
+```bash
+poetry install
+```
 
 Execute
 ```bash

From 775e30a80fdecda72bb716f61c56f0abd8623665 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 28 May 2024 20:35:47 -0700
Subject: [PATCH 18/18] feat: Extraction of tactic invocations

---
 examples/Example/Example.lean |  8 ++++++++
 examples/compile-tactics.py   | 19 +++++++++++++++++++
 pantograph/server.py          | 10 +++++++++-
 poetry.lock                   | 22 +++++++++++++---------
 src                           |  2 +-
 5 files changed, 50 insertions(+), 11 deletions(-)
 create mode 100755 examples/compile-tactics.py

diff --git a/examples/Example/Example.lean b/examples/Example/Example.lean
index 1a5e245..40cb3dc 100644
--- a/examples/Example/Example.lean
+++ b/examples/Example/Example.lean
@@ -3,3 +3,11 @@ import Aesop
 -- Ensure that Aesop is running
 example : α → α :=
   by aesop
+
+example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
+  intro p q h
+  cases h
+  . apply Or.inr
+    assumption
+  . apply Or.inl
+    assumption
diff --git a/examples/compile-tactics.py b/examples/compile-tactics.py
new file mode 100755
index 0000000..d4845da
--- /dev/null
+++ b/examples/compile-tactics.py
@@ -0,0 +1,19 @@
+#!/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)
+    data = server.compile_tactics("Example")
+    for (before, tactic, after) in data:
+        print(f"{before}\n{tactic}\n{after}\n\n")
diff --git a/pantograph/server.py b/pantograph/server.py
index 4701e1f..af8c7e3 100644
--- a/pantograph/server.py
+++ b/pantograph/server.py
@@ -137,6 +137,14 @@ class Server:
         return GoalState.parse(result, self.to_remove_goal_states)
 
 
+    def compile_tactics(self, module: str) -> list[tuple[str, str, str]]:
+        result = self.run('compile.tactics', {'module': module})
+        if "error" in result:
+            raise ServerError(result["desc"])
+        return [(i['goalBefore'], i['tactic'], i['goalAfter']) for i in result['invocations']]
+
+
+
 def get_version():
     import subprocess
     with subprocess.Popen([_get_proc_path(), "--version"],
@@ -215,4 +223,4 @@ class TestServer(unittest.TestCase):
 
 
 if __name__ == '__main__':
-    unittest.main()
\ No newline at end of file
+    unittest.main()
diff --git a/poetry.lock b/poetry.lock
index be1c94f..0d47380 100644
--- a/poetry.lock
+++ b/poetry.lock
@@ -1,10 +1,15 @@
+# This file is automatically @generated by Poetry 1.8.2 and should not be changed by hand.
+
 [[package]]
 name = "pexpect"
 version = "4.9.0"
 description = "Pexpect allows easy control of interactive console applications."
-category = "main"
 optional = false
 python-versions = "*"
+files = [
+    {file = "pexpect-4.9.0-py2.py3-none-any.whl", hash = "sha256:7236d1e080e4936be2dc3e326cec0af72acf9212a7e1d060210e70a47e253523"},
+    {file = "pexpect-4.9.0.tar.gz", hash = "sha256:ee7d41123f3c9911050ea2c2dac107568dc43b2d3b0c7557a33212c398ead30f"},
+]
 
 [package.dependencies]
 ptyprocess = ">=0.5"
@@ -13,15 +18,14 @@ ptyprocess = ">=0.5"
 name = "ptyprocess"
 version = "0.7.0"
 description = "Run a subprocess in a pseudo terminal"
-category = "main"
 optional = false
 python-versions = "*"
+files = [
+    {file = "ptyprocess-0.7.0-py2.py3-none-any.whl", hash = "sha256:4b41f3967fce3af57cc7e94b888626c18bf37a083e3651ca8feeb66d492fef35"},
+    {file = "ptyprocess-0.7.0.tar.gz", hash = "sha256:5c5d0a3b48ceee0b48485e0c26037c0acd7d29765ca3fbb5cb3831d347423220"},
+]
 
 [metadata]
-lock-version = "1.1"
-python-versions = "^3.11"
-content-hash = "aaae6d4832f97d9ad1b145776be94a2c44a7e77068bb1b3a05241a81dde23909"
-
-[metadata.files]
-pexpect = []
-ptyprocess = []
+lock-version = "2.0"
+python-versions = "^3.10"
+content-hash = "54cb66612c110a515f024e54d2b2a0af54ffcbe06602ad7f4ea6a446699d419a"
diff --git a/src b/src
index 0aec757..b9b16ba 160000
--- a/src
+++ b/src
@@ -1 +1 @@
-Subproject commit 0aec757601a2aea9f9efabae7eda4300832f0021
+Subproject commit b9b16ba0e9d99279837527bcb40176277d11e725