bump to nightly-2023-08-04-05

mathlib commit leanprover-community/mathlib3@48a058d
leanprover-community · Aug 4, 2023 · a23eed5 · a23eed5
1 parent 5ed98c8
commit a23eed5
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "fe512bc399dc93d128cdd53e5f7416ca2df635c7",
+    "rev": "b9d415a5426dcc76b63de1848817dc098dd8b991",
     "name": "lean3port",
-    "inputRev?": "fe512bc399dc93d128cdd53e5f7416ca2df635c7"}},
+    "inputRev?": "b9d415a5426dcc76b63de1848817dc098dd8b991"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "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-08-04-03"
+def tag : String := "nightly-2023-08-04-05"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"fe512bc399dc93d128cdd53e5f7416ca2df635c7"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"b9d415a5426dcc76b63de1848817dc098dd8b991"
 
 @[default_target]
 lean_lib Mathbin where