example: Calling aesop (partial)

examples/Example/.gitignore

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

examples/Example/Example.lean

@@ -0,0 +1 @@
+import 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,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

examples/Example/lean-toolchain

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

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
+```
+

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)