bump to nightly-2023-05-25-03

mathlib commit leanprover-community/mathlib@8d33f09
leanprover-community · May 25, 2023 · cab2c30 · cab2c30
1 parent 8b2ed6c
commit cab2c30
Show file tree

Hide file tree

Showing 6 changed files with 411 additions and 69 deletions.
diff --git a/Mathbin/Algebra/Category/Module/Limits.lean b/Mathbin/Algebra/Category/Module/Limits.lean
diff --git a/Mathbin/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean b/Mathbin/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean
diff --git a/Mathbin/Analysis/Calculus/Fderiv/Star.lean b/Mathbin/Analysis/Calculus/Fderiv/Star.lean
diff --git a/Mathbin/RingTheory/Ideal/QuotientOperations.lean b/Mathbin/RingTheory/Ideal/QuotientOperations.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "eda396f443b385d7252cd3f4fa5784dd77309a3c",
+    "rev": "ae4dda5884ae13dc7caeff0ab7f677559ac5e352",
     "name": "lean3port",
-    "inputRev?": "eda396f443b385d7252cd3f4fa5784dd77309a3c"}},
+    "inputRev?": "ae4dda5884ae13dc7caeff0ab7f677559ac5e352"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "009b0477e0161944b3592293b39c80c15ae7a75a",
+    "rev": "52d71ad9606cf755e2437cfedfbcc89ce8f2b86a",
     "name": "mathlib",
-    "inputRev?": "009b0477e0161944b3592293b39c80c15ae7a75a"}},
+    "inputRev?": "52d71ad9606cf755e2437cfedfbcc89ce8f2b86a"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

diff --git a/lakefile.lean b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-05-25-01"
+def tag : String := "nightly-2023-05-25-03"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"eda396f443b385d7252cd3f4fa5784dd77309a3c"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"ae4dda5884ae13dc7caeff0ab7f677559ac5e352"
 
 @[default_target]
 lean_lib Mathbin where