diff --git a/lake-manifest.json b/lake-manifest.json index 29febd020e..d7cf8a3a18 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -10,9 +10,9 @@ {"git": {"url": "https://github.com/leanprover-community/lean3port.git", "subDir?": null, - "rev": "e10bf04eafb086f16da757e983917fce937e9f78", + "rev": "af3675b09c625aaf390b3874cbdac583a0186804", "name": "lean3port", - "inputRev?": "e10bf04eafb086f16da757e983917fce937e9f78"}}, + "inputRev?": "af3675b09c625aaf390b3874cbdac583a0186804"}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli.git", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 5240a7ba5e..d4080bfd98 100644 --- 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-07-22-23" +def tag : String := "nightly-2023-07-23-01" 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"@"e10bf04eafb086f16da757e983917fce937e9f78" +require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"af3675b09c625aaf390b3874cbdac583a0186804" @[default_target] lean_lib Mathbin where