fix: adapt test suite to new Lake, mathlib not compatible yet though

leanprover · Jul 3, 2022 · 4b5e606 · 4b5e606
1 parent a5bd0de
commit 4b5e606
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 7 deletions.
diff --git a/test/dep/lakefile.lean b/test/dep/lakefile.lean
@@ -1,10 +1,8 @@
 import Lake
 open Lake DSL
 
-package dep {
-  defaultFacet := PackageFacet.oleans
-  dependencies := #[{
-    name := `mathlib
-    src := Source.git "https://github.com/leanprover-community/mathlib4.git" "84ca33e940678954dc146f732f447ddc8984cf39"
-  }]
-}
+package dep
+
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
+
+lean_lib dep
diff --git a/test/dep/lean_packages/manifest.json b/test/dep/lean_packages/manifest.json
@@ -0,0 +1,5 @@
+{"version": 1,
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4.git",
+   "rev": "ecd37441047e490ff2ad339e16f45bb8b58591bd",
+   "name": "mathlib"}]}