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