From b7542b4749015d8ee6f43f656256d955e00bf94b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 15 Mar 2024 06:01:25 -0700
Subject: [PATCH] chore: Lean version bump to 4.7.0-rc2

Multithreading in ABI was not stabilized in 4.1.0
---
 Makefile           |  8 ++++----
 flake.lock         |  8 ++++----
 flake.nix          |  2 +-
 lake-manifest.json | 24 +++++++++++++-----------
 lakefile.lean      |  2 +-
 lean-toolchain     |  2 +-
 6 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/Makefile b/Makefile
index 39350b6..5d4ad6b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,8 @@
-LIB := build/lib/Pantograph.olean
-EXE := build/bin/pantograph
+LIB := ./.lake/build/lib/Pantograph.olean
+EXE := ./.lake/build/bin/pantograph
 SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain
 
-TEST_EXE := build/bin/test
+TEST_EXE := ./.lake/build/bin/test
 TEST_SOURCE := $(wildcard Test/*.lean)
 
 $(LIB) $(EXE): $(SOURCE)
@@ -12,7 +12,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE)
 	lake build test
 
 test: $(TEST_EXE)
-	lake env $(TEST_EXE)
+	$(TEST_EXE)
 
 clean:
 	lake clean
diff --git a/flake.lock b/flake.lock
index 67246b6..89f0e9d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -41,16 +41,16 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1695693562,
-        "narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=",
+        "lastModified": 1709691092,
+        "narHash": "sha256-jHY8BhDotfGcMS0Xzl5iawqCaug3dDEKuD5Y1WcM06I=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "a832f398b80a5ebb820d27b9e55ec949759043ff",
+        "rev": "6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "v4.1.0",
+        "ref": "v4.7.0-rc2",
         "repo": "lean4",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 9f586f6..54640d3 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean.url = "github:leanprover/lean4?ref=v4.1.0";
+    lean.url = "github:leanprover/lean4?ref=v4.7.0-rc2";
   };
 
   outputs = inputs @ {
diff --git a/lake-manifest.json b/lake-manifest.json
index 6c2efa0..6ebbbe5 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,12 +1,14 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/lurk-lab/LSpec.git",
-    "subDir?": null,
-    "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
-    "opts": {},
-    "name": "LSpec",
-    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
-    "inherited": false}}],
- "name": "pantograph"}
+ [{"url": "https://github.com/lurk-lab/LSpec.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "pantograph",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 89ad70f..d7bc630 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -15,7 +15,7 @@ lean_exe pantograph {
 }
 
 require LSpec from git
-  "https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
+  "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
 lean_lib Test {
 }
 lean_exe test {
diff --git a/lean-toolchain b/lean-toolchain
index a9bddf0..faa2254 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.1.0
+leanprover/lean4:4.7.0-rc2