bump to nightly-2023-06-21-23

mathlib commit leanprover-community/mathlib@f2ad364

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "addfe04203cfbe001020dc906ad69812e3e3228d",
+    "rev": "a1fd69c0ae3540f5b683423747edeb32e9046aaa",
     "name": "lean3port",
-    "inputRev?": "addfe04203cfbe001020dc906ad69812e3e3228d"}},
+    "inputRev?": "a1fd69c0ae3540f5b683423747edeb32e9046aaa"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "ee000bf3b049cd25914bfa67960159c9c51d2827",
+    "rev": "28cbaf7d43de64040cdeb1a4b1b5622c4c3049d2",
     "name": "mathlib",
-    "inputRev?": "ee000bf3b049cd25914bfa67960159c9c51d2827"}},
+    "inputRev?": "28cbaf7d43de64040cdeb1a4b1b5622c4c3049d2"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

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-06-21-21"
+def tag : String := "nightly-2023-06-21-23"
 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"@"addfe04203cfbe001020dc906ad69812e3e3228d"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"a1fd69c0ae3540f5b683423747edeb32e9046aaa"
 
 @[default_target]
 lean_lib Mathbin where