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 1/7] 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 2/7] 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 3/7] 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 4/7] 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 5/7] 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 6/7] 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 7/7] 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:
         """