merge #9453

.github/workflows/bors.yml

@@ -161,6 +161,19 @@ jobs:
           lean --version
           lake --version
 
+      - name: build cache
+        run: |
+          lake build cache
+
+      - name: prune ProofWidgets .lake
+        run: |
+          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
+          # but also `.oleans`, which may have been built with the wrong toolchain.
+          # This removes them.
+          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
+          rm -rf .lake/packages/proofwidgets/.lake/build/lib
+          rm -rf .lake/packages/proofwidgets/.lake/build/ir
+
       - name: get cache
         run: |
           lake exe cache clean
@@ -194,6 +207,7 @@ jobs:
           lake exe cache put || (sleep 1; lake exe cache put) || true
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: check the cache
         run: |
@@ -221,6 +235,7 @@ jobs:
           lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
         run: |
@@ -229,6 +244,7 @@ jobs:
           lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: check declarations in db files
         run: |

.github/workflows/build.yml

@@ -168,6 +168,19 @@ jobs:
           lean --version
           lake --version
 
+      - name: build cache
+        run: |
+          lake build cache
+
+      - name: prune ProofWidgets .lake
+        run: |
+          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
+          # but also `.oleans`, which may have been built with the wrong toolchain.
+          # This removes them.
+          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
+          rm -rf .lake/packages/proofwidgets/.lake/build/lib
+          rm -rf .lake/packages/proofwidgets/.lake/build/ir
+
       - name: get cache
         run: |
           lake exe cache clean
@@ -201,6 +214,7 @@ jobs:
           lake exe cache put || (sleep 1; lake exe cache put) || true
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: check the cache
         run: |
@@ -228,6 +242,7 @@ jobs:
           lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
         run: |
@@ -236,6 +251,7 @@ jobs:
           lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: check declarations in db files
         run: |

.github/workflows/build.yml.in

@@ -147,6 +147,19 @@ jobs:
           lean --version
           lake --version
 
+      - name: build cache
+        run: |
+          lake build cache
+
+      - name: prune ProofWidgets .lake
+        run: |
+          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
+          # but also `.oleans`, which may have been built with the wrong toolchain.
+          # This removes them.
+          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
+          rm -rf .lake/packages/proofwidgets/.lake/build/lib
+          rm -rf .lake/packages/proofwidgets/.lake/build/ir
+
       - name: get cache
         run: |
           lake exe cache clean
@@ -180,6 +193,7 @@ jobs:
           lake exe cache put || (sleep 1; lake exe cache put) || true
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: check the cache
         run: |
@@ -207,6 +221,7 @@ jobs:
           lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
         run: |
@@ -215,6 +230,7 @@ jobs:
           lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: check declarations in db files
         run: |

.github/workflows/build_fork.yml

@@ -165,6 +165,19 @@ jobs:
           lean --version
           lake --version
 
+      - name: build cache
+        run: |
+          lake build cache
+
+      - name: prune ProofWidgets .lake
+        run: |
+          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
+          # but also `.oleans`, which may have been built with the wrong toolchain.
+          # This removes them.
+          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
+          rm -rf .lake/packages/proofwidgets/.lake/build/lib
+          rm -rf .lake/packages/proofwidgets/.lake/build/ir
+
       - name: get cache
         run: |
           lake exe cache clean
@@ -198,6 +211,7 @@ jobs:
           lake exe cache put || (sleep 1; lake exe cache put) || true
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: check the cache
         run: |
@@ -225,6 +239,7 @@ jobs:
           lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: build counterexamples
         run: |
@@ -233,6 +248,7 @@ jobs:
           lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: check declarations in db files
         run: |

Archive/Imo/Imo1981Q3.lean

@@ -207,5 +207,5 @@ theorem imo1981_q3 : IsGreatest (specifiedSet 1981) 3524578 := by
   apply this
   · decide
   · decide
-  · norm_num [ProblemPredicate_iff]; decide
+  · norm_num [problemPredicate_iff]; decide
 #align imo1981_q3 imo1981_q3

Cache/IO.lean

@@ -286,7 +286,7 @@ def allExist (paths : List (FilePath × Bool)) : IO Bool := do
   pure true
 
 /-- Compresses build files into the local cache and returns an array with the compressed files -/
-def packCache (hashMap : HashMap) (overwrite : Bool) (comment : Option String := none) :
+def packCache (hashMap : HashMap) (overwrite verbose : Bool) (comment : Option String := none) :
     IO $ Array String := do
   mkDir CACHEDIR
   IO.println "Compressing cache"
@@ -305,10 +305,14 @@ def packCache (hashMap : HashMap) (overwrite : Bool) (comment : Option String :=
             | unreachable!
           runCmd (← getLeanTar) $ #[zipPath.toString, trace] ++
             (if let some c := comment then #["-c", s!"git=mathlib4@{c}"] else #[]) ++ args
-      acc := acc.push zip
+      acc := acc.push (path, zip)
   for task in tasks do
     _ ← IO.ofExcept task.get
-  return acc
+  acc := acc.qsort (·.1.1 < ·.1.1)
+  if verbose then
+    for (path, zip) in acc do
+      println! "packing {path} as {zip}"
+  return acc.map (·.2)
 
 /-- Gets the set of all cached files -/
 def getLocalCacheSet : IO $ Lean.RBTree String compare := do
@@ -347,12 +351,6 @@ def unpackCache (hashMap : HashMap) (force : Bool) : IO Unit := do
     IO.println s!"unpacked in {(← IO.monoMsNow) - now} ms"
   else IO.println "No cache files to decompress"
 
-/-- Retrieves the azure token from the environment -/
-def getToken : IO String := do
-  let some token ← IO.getEnv "MATHLIB_CACHE_SAS"
-    | throw $ IO.userError "environment variable MATHLIB_CACHE_SAS must be set to upload caches"
-  return token
-
 instance : Ord FilePath where
   compare x y := compare x.toString y.toString
 

Cache/Main.lean

@@ -86,16 +86,16 @@ def main (args : List String) : IO Unit := do
     getFiles (← hashMemo.filterByFilePaths (toPaths args)) true true goodCurl true
   | "get-" :: args =>
     getFiles (← hashMemo.filterByFilePaths (toPaths args)) false false goodCurl false
-  | ["pack"] => discard $ packCache hashMap false (← getGitCommitHash)
-  | ["pack!"] => discard $ packCache hashMap true (← getGitCommitHash)
+  | ["pack"] => discard $ packCache hashMap false false (← getGitCommitHash)
+  | ["pack!"] => discard $ packCache hashMap true false (← getGitCommitHash)
   | ["unpack"] => unpackCache hashMap false
   | ["unpack!"] => unpackCache hashMap true
   | ["clean"] =>
     cleanCache $ hashMap.fold (fun acc _ hash => acc.insert $ CACHEDIR / hash.asLTar) .empty
   | ["clean!"] => cleanCache
   -- We allow arguments for `put` and `put!` so they can be added to the `roots`.
-  | "put" :: _ => putFiles (← packCache hashMap false (← getGitCommitHash)) false (← getToken)
-  | "put!" :: _ => putFiles (← packCache hashMap false (← getGitCommitHash)) true (← getToken)
+  | "put" :: _ => putFiles (← packCache hashMap false true (← getGitCommitHash)) false (← getToken)
+  | "put!" :: _ => putFiles (← packCache hashMap false true (← getGitCommitHash)) true (← getToken)
   | ["commit"] =>
     if !(← isGitStatusClean) then IO.println "Please commit your changes first" return else
     commit hashMap false (← getToken)

Cache/Requests.lean

@@ -10,9 +10,22 @@ set_option autoImplicit true
 
 namespace Cache.Requests
 
-/-- Azure blob URL -/
+-- FRO cache is flaky so disable until we work out the kinks: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20cache.20doesn't.20work/near/411058849
+def useFROCache : Bool := false
+
+/-- Public URL for mathlib cache -/
 def URL : String :=
-  "https://lakecache.blob.core.windows.net/mathlib4"
+  if useFROCache then
+    "https://mathlib4.lean-cache.cloud"
+  else
+    "https://lakecache.blob.core.windows.net/mathlib4"
+
+/-- Retrieves the azure token from the environment -/
+def getToken : IO String := do
+  let envVar := if useFROCache then "MATHLIB_CACHE_S3_TOKEN" else "MATHLIB_CACHE_SAS"
+  let some token ← IO.getEnv envVar
+    | throw $ IO.userError s!"environment variable {envVar} must be set to upload caches"
+  return token
 
 open System (FilePath)
 
@@ -21,10 +34,8 @@ Given a file name like `"1234.tar.gz"`, makes the URL to that file on the server
 
 The `f/` prefix means that it's a common file for caching.
 -/
-def mkFileURL (fileName : String) (token : Option String) : IO String :=
-  return match token with
-  | some token => s!"{URL}/f/{fileName}?{token}"
-  | none => s!"{URL}/f/{fileName}"
+def mkFileURL (URL fileName : String) : String :=
+  s!"{URL}/f/{fileName}"
 
 section Get
 
@@ -47,13 +58,13 @@ def mkGetConfigContent (hashMap : IO.HashMap) : IO String := do
 
     -- Note we append a '.part' to the filenames here,
     -- which `downloadFiles` then removes when the download is successful.
-    pure $ acc ++ s!"url = {← mkFileURL fileName none}\n-o {
-      (IO.CACHEDIR / (fileName ++ ".part")).toString.quote}\n"
+    pure $ acc ++ s!"url = {mkFileURL URL fileName}\n\
+      -o {(IO.CACHEDIR / (fileName ++ ".part")).toString.quote}\n"
 
 /-- Calls `curl` to download a single file from the server to `CACHEDIR` (`.cache`) -/
 def downloadFile (hash : UInt64) : IO Bool := do
   let fileName := hash.asLTar
-  let url ← mkFileURL fileName none
+  let url := mkFileURL URL fileName
   let path := IO.CACHEDIR / fileName
   let partFileName := fileName ++ ".part"
   let partPath := IO.CACHEDIR / partFileName
@@ -161,23 +172,38 @@ end Get
 
 section Put
 
+/-- FRO cache S3 URL -/
+def UPLOAD_URL : String :=
+  if useFROCache then
+    "https://a09a7664adc082e00f294ac190827820.r2.cloudflarestorage.com/mathlib4"
+  else
+    URL
+
 /-- Formats the config file for `curl`, containing the list of files to be uploaded -/
 def mkPutConfigContent (fileNames : Array String) (token : String) : IO String := do
+  let token := if useFROCache then "" else s!"?{token}" -- the FRO cache doesn't pass the token here
   let l ← fileNames.data.mapM fun fileName : String => do
-    pure s!"-T {(IO.CACHEDIR / fileName).toString}\nurl = {← mkFileURL fileName (some token)}"
+    pure s!"-T {(IO.CACHEDIR / fileName).toString}\nurl = {mkFileURL UPLOAD_URL fileName}{token}"
   return "\n".intercalate l
 
 /-- Calls `curl` to send a set of cached files to the server -/
 def putFiles (fileNames : Array String) (overwrite : Bool) (token : String) : IO Unit := do
+  -- TODO: reimplement using HEAD requests?
+  let _ := overwrite
   let size := fileNames.size
   if size > 0 then
     IO.FS.writeFile IO.CURLCFG (← mkPutConfigContent fileNames token)
     IO.println s!"Attempting to upload {size} file(s)"
-    if overwrite then
-      discard $ IO.runCurl #["-X", "PUT", "-H", "x-ms-blob-type: BlockBlob", "--parallel",
+    if useFROCache then
+      -- TODO: reimplement using HEAD requests?
+      let _ := overwrite
+      discard $ IO.runCurl #["-s", "-X", "PUT", "--aws-sigv4", "aws:amz:auto:s3", "--user", token,
+        "--parallel", "-K", IO.CURLCFG.toString]
+    else if overwrite then
+      discard $ IO.runCurl #["-s", "-X", "PUT", "-H", "x-ms-blob-type: BlockBlob", "--parallel",
         "-K", IO.CURLCFG.toString]
     else
-      discard $ IO.runCurl #["-X", "PUT", "-H", "x-ms-blob-type: BlockBlob",
+      discard $ IO.runCurl #["-s", "-X", "PUT", "-H", "x-ms-blob-type: BlockBlob",
         "-H", "If-None-Match: *", "--parallel", "-K", IO.CURLCFG.toString]
     IO.FS.removeFile IO.CURLCFG
   else IO.println "No files to upload"
@@ -201,10 +227,16 @@ def commit (hashMap : IO.HashMap) (overwrite : Bool) (token : String) : IO Unit
   let path := IO.CACHEDIR / hash
   IO.mkDir IO.CACHEDIR
   IO.FS.writeFile path $ ("\n".intercalate $ hashMap.hashes.toList.map toString) ++ "\n"
-  let params := if overwrite
-    then #["-X", "PUT", "-H", "x-ms-blob-type: BlockBlob"]
-    else #["-X", "PUT", "-H", "x-ms-blob-type: BlockBlob", "-H", "If-None-Match: *"]
-  discard $ IO.runCurl $ params ++ #["-T", path.toString, s!"{URL}/c/{hash}?{token}"]
+  if useFROCache then
+    -- TODO: reimplement using HEAD requests?
+    let _ := overwrite
+    discard $ IO.runCurl $ #["-T", path.toString, "--aws-sigv4", "aws:amz:auto:s3",
+      "--user", token, s!"{UPLOAD_URL}/c/{hash}"]
+  else
+    let params := if overwrite
+      then #["-X", "PUT", "-H", "x-ms-blob-type: BlockBlob"]
+      else #["-X", "PUT", "-H", "x-ms-blob-type: BlockBlob", "-H", "If-None-Match: *"]
+    discard $ IO.runCurl $ params ++ #["-T", path.toString, s!"{URL}/c/{hash}?{token}"]
   IO.FS.removeFile path
 
 end Commit
@@ -233,6 +265,8 @@ Retrieves metadata about hosted files: their names and the timestamps of last mo
 Example: `["f/39476538726384726.tar.gz", "Sat, 24 Dec 2022 17:33:01 GMT"]`
 -/
 def getFilesInfo (q : QueryType) : IO $ List (String × String) := do
+  if useFROCache then
+    throw <| .userError "FIXME: getFilesInfo is not adapted to FRO cache yet"
   IO.println s!"Downloading info list of {q.desc}"
   let ret ← IO.runCurl #["-X", "GET", s!"{URL}?comp=list&restype=container{q.prefix}"]
   match ret.splitOn "<Name>" with