feat: Extraction of tactic invocations

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

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

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()
+    unittest.main()

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"

src

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