Merge pull request #1 from lenianiva/dev

feat: Expression typing, garbage collection, library loading

examples/Example/.gitignore

@@ -0,0 +1,3 @@
+/build
+/lakefile.olean
+/lake-packages/*

examples/Example/Example.lean

@@ -0,0 +1,5 @@
+import Aesop
+
+-- Ensure that Aesop is running
+example : α → α :=
+  by aesop

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"}

examples/Example/lakefile.lean

@@ -0,0 +1,10 @@
+import Lake
+open Lake DSL
+
+require aesop from git
+  "https://github.com/leanprover-community/aesop.git" @ "v4.8.0-rc1"
+
+package Example
+
+@[default_target]
+lean_lib Example

examples/Example/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.8.0-rc1

examples/README.md

@@ -0,0 +1,15 @@
+# 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 from the
+project root:
+``` sh
+poetry run examples/aesop.py
+```
+

examples/aesop.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)
+    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

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:

pantograph/server.py

@@ -2,8 +2,8 @@
 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 Variable, Goal, GoalState, \
+from pantograph.expr import parse_expr, Expr, Variable, Goal, GoalState, \
     Tactic, TacticHave, TacticCalc
 
 def _get_proc_cwd():
@@ -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
@@ -36,35 +39,63 @@ 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()
+        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)
 
     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:
+        except pexpect.exceptions.TIMEOUT as exc:
-            raise pexpect.exceptions.TIMEOUT
+            raise exc
 
-    def reset(self):
+    def gc(self):
-        return self.run("reset", {})
+        """
+        Garbage collect deleted goal states.
+
+        Must be called periodically.
+        """
+        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:
+        """
+        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:
             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 +114,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 +124,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 +134,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():
@@ -117,11 +148,17 @@ 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()
+        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")
+        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 +169,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")

src

@@ -1 +1 @@
-Subproject commit f20ee8dc87ae3fa9c0f13040e1b4f097f1a40503
+Subproject commit 0aec757601a2aea9f9efabae7eda4300832f0021