diff --git a/lake-manifest.json b/lake-manifest.json index 09bf9cfb3bc8b..cc9da57b5fd74 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,13 +1,13 @@ {"version": 7, "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/fgdorais/std4", + [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "89eab993f49a933f981ce078a17118c1f94a3247", + "rev": "dbb4045860667f0d09669dbfb524b6e7b0ca3aca", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "nat-add", + "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/quote4", diff --git a/lakefile.lean b/lakefile.lean index 935be5ec153bc..b9e06d5208004 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -26,7 +26,7 @@ package mathlib 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/fgdorais/std4" @ "nat-add" +require std from git "https://github.com/leanprover/std4" @ "main" require Qq from git "https://github.com/leanprover-community/quote4" @ "master" require aesop from git "https://github.com/leanprover-community/aesop" @ "master" require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.23"