diff --git a/lake-manifest.json b/lake-manifest.json index 99a5e90a2ebf0..9b84bc639a564 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -2,14 +2,6 @@ "packagesDir": "lake-packages", "packages": [{"git": - {"url": "https://github.com/leanprover/std4", - "subDir?": null, - "rev": "a71c160b1934814837d37f377efaf2964e55c433", - "opts": {}, - "name": "std", - "inputRev?": "main", - "inherited": false}}, - {"git": {"url": "https://github.com/leanprover-community/quote4", "subDir?": null, "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2", @@ -40,5 +32,13 @@ "opts": {}, "name": "proofwidgets", "inputRev?": "v0.0.21", + "inherited": false}}, + {"git": + {"url": "https://github.com/fgdorais/std4", + "subDir?": null, + "rev": "c00d3b184f5df002a18055120fa4032ecec4aad7", + "opts": {}, + "name": "std", + "inputRev?": "nat-sub", "inherited": false}}], "name": "mathlib"} diff --git a/lakefile.lean b/lakefile.lean index f1b8ef2bae0da..71113c45a6e93 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -46,7 +46,7 @@ lean_exe checkYaml where meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" -require std from git "https://github.com/leanprover/std4" @ "main" +require std from git "https://github.com/fgdorais/std4" @ "nat-sub" require Qq from git "https://github.com/leanprover-community/quote4" @ "master" require aesop from git "https://github.com/leanprover-community/aesop" @ "master" require Cli from git "https://github.com/leanprover/lean4-cli" @ "nightly"