example: Calling aesop

examples/Example/Example.lean

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

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
+package Example
-  -- add package configuration options here
 
-lean_lib «Example» where
+@[default_target]
-  -- add library configuration options here
+lean_lib Example

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()
+    project_path, lean_path = get_project_and_lean_path()
-    print(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/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)