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

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"
       }

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 @ {

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"}

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 {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:4.1.0
+leanprover/lean4:4.7.0-rc2