Merge pull request #51 from semorrison/pin_mathlib

chore: pin a Mathlib commit for tests
leanprover · Aug 23, 2023 · 991d129 · 991d129
2 parents 685a4f1 + cc5ef2e
commit 991d129
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 3 deletions.
diff --git a/README.md b/README.md
@@ -81,6 +81,13 @@ For more information about Alectryon make sure to take a look at their repositor
 
 # Development
 
+## Updating
+
+When updating the `lean-toolchain`, please also:
+* update `test/dep/lean-toolchain` to match,
+* change the Mathlib commit in `test/dep.lakefile.lean` to a commit of Mathlib using the same toolchain,
+* run `lake update` in `test/dep/` to update the `lake-manifest.json`.
+
 ## Experimental Features
 
 ### Additional Type Hover Metadata

diff --git a/test/dep/lake-manifest.json b/test/dep/lake-manifest.json
@@ -4,9 +4,9 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "9543173939e94784b16060bcd932c99387e30bb7",
+    "rev": "3d5d1404a27f4b285302a1589e1da2672590da34",
     "name": "mathlib",
-    "inputRev?": "master"}},
+    "inputRev?": "3d5d1404a27f4b285302a1589e1da2672590da34"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

diff --git a/test/dep/lakefile.lean b/test/dep/lakefile.lean
@@ -3,7 +3,7 @@ open Lake DSL
 
 package dep
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "master"
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "3d5d1404a27f4b285302a1589e1da2672590da34"
 
 @[default_target]
 lean_lib dep
diff --git a/test/dep/lean-toolchain b/test/dep/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-04-07