From fceb0c1a206e858b829cd8ac72593fa6d3e168c5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 17 May 2024 20:45:29 -0700
Subject: [PATCH] example: Calling aesop (partial)

---
 examples/Example/.gitignore         |  3 +++
 examples/Example/Example.lean       |  1 +
 examples/Example/lake-manifest.json | 23 +++++++++++++++++++++++
 examples/Example/lakefile.lean      | 11 +++++++++++
 examples/Example/lean-toolchain     |  1 +
 examples/README.md                  | 14 ++++++++++++++
 examples/aesop.py                   | 14 ++++++++++++++
 7 files changed, 67 insertions(+)
 create mode 100644 examples/Example/.gitignore
 create mode 100644 examples/Example/Example.lean
 create mode 100644 examples/Example/lake-manifest.json
 create mode 100644 examples/Example/lakefile.lean
 create mode 100644 examples/Example/lean-toolchain
 create mode 100644 examples/README.md
 create mode 100755 examples/aesop.py

diff --git a/examples/Example/.gitignore b/examples/Example/.gitignore
new file mode 100644
index 0000000..1824d0c
--- /dev/null
+++ b/examples/Example/.gitignore
@@ -0,0 +1,3 @@
+/build
+/lakefile.olean
+/lake-packages/*
diff --git a/examples/Example/Example.lean b/examples/Example/Example.lean
new file mode 100644
index 0000000..eef5356
--- /dev/null
+++ b/examples/Example/Example.lean
@@ -0,0 +1 @@
+import Aesop
diff --git a/examples/Example/lake-manifest.json b/examples/Example/lake-manifest.json
new file mode 100644
index 0000000..06e1c0e
--- /dev/null
+++ b/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"}
diff --git a/examples/Example/lakefile.lean b/examples/Example/lakefile.lean
new file mode 100644
index 0000000..0429d0d
--- /dev/null
+++ b/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
diff --git a/examples/Example/lean-toolchain b/examples/Example/lean-toolchain
new file mode 100644
index 0000000..d8a6d7e
--- /dev/null
+++ b/examples/Example/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.8.0-rc1
diff --git a/examples/README.md b/examples/README.md
new file mode 100644
index 0000000..8924626
--- /dev/null
+++ b/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
+```
+
diff --git a/examples/aesop.py b/examples/aesop.py
new file mode 100755
index 0000000..dd5ba84
--- /dev/null
+++ b/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)