feat(Cache): environment-configurable URLs (leanprover-community#33605)

Makes the URLs used by Mathlib's cache (`lake exe cache`) configurable via environment variables. The download URL is configured through `MATHLIB_CACHE_GET_URL` and the upload URL is configured through `MATHLIB_CACHE_PUT_URL`.

Author: tydeu

Cache/Init.lean

@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2023 Arthur Paulino. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur Paulino
+-/
+
+namespace Cache.Requests
+
+open System (FilePath)
+
+-- FRO cache may be flaky: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/The.20cache.20doesn't.20work/near/411058849
+-- This is defined in a separate file because it is used in the definition of `URL` and `UPLOAD_URL`
+-- and Lean does not allow one `initialize` to use another `initialize` defined in the same file
+initialize useFROCache : Bool ← do
+  let froCache ← IO.getEnv "USE_FRO_CACHE"
+  return froCache == some "1" || froCache == some "true"

Cache/Requests.lean

@@ -6,16 +6,12 @@ Authors: Arthur Paulino
 
 import Batteries.Data.String.Matcher
 import Cache.Hashing
+import Cache.Init
 
 namespace Cache.Requests
 
 open System (FilePath)
 
--- FRO cache may be flaky: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/The.20cache.20doesn't.20work/near/411058849
-initialize useFROCache : Bool ← do
-  let froCache ← IO.getEnv "USE_FRO_CACHE"
-  return froCache == some "1" || froCache == some "true"
-
 /--
 Structure to hold repository information with priority ordering
 -/
@@ -244,11 +240,14 @@ def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
   return {repo := repo, useFirst := false}
 
 /-- Public URL for mathlib cache -/
-def URL : String :=
-  if useFROCache then
-    "https://mathlib4.lean-cache.cloud"
-  else
-    "https://lakecache.blob.core.windows.net/mathlib4"
+initialize URL : String ← do
+  let url? ← IO.getEnv "MATHLIB_CACHE_GET_URL"
+  let defaultUrl :=
+    if useFROCache then
+      "https://mathlib4.lean-cache.cloud"
+    else
+      "https://lakecache.blob.core.windows.net/mathlib4"
+  return url?.getD defaultUrl
 
 /-- Retrieves the azure token from the environment -/
 def getToken : IO String := do
@@ -508,11 +507,14 @@ end Get
 section Put
 
 /-- FRO cache S3 URL -/
-def UPLOAD_URL : String :=
-  if useFROCache then
-    "https://a09a7664adc082e00f294ac190827820.r2.cloudflarestorage.com/mathlib4"
-  else
-    URL
+initialize UPLOAD_URL : String ← do
+  let url? ← IO.getEnv "MATHLIB_CACHE_PUT_URL"
+  let defaultUrl :=
+    if useFROCache then
+      "https://a09a7664adc082e00f294ac190827820.r2.cloudflarestorage.com/mathlib4"
+    else
+      "https://lakecache.blob.core.windows.net/mathlib4"
+  return url?.getD defaultUrl
 
 /-- Formats the config file for `curl`, containing the list of files to be uploaded -/
 def mkPutConfigContent (repo : String) (fileNames : Array String) (token : String) : IO String := do