feat: Fail validation when a required Mathlib cache is missing

Falling back to a source build is not a smaller version of using the
cache: Mathlib takes hours to compile and the run usually dies on the job
timeout, so the warning scrolls past and the answer never arrives. Stop
instead, before the build starts, and report the directory along with
what `lake exe cache get` printed.

`mathlib_cache: optional` restores the old behaviour for anyone who would
rather have a slow answer than none.

The failure travels as a build error rather than an exception because
`createIssue` re-runs validation to compose the issue body; raising here
would leave the notification path with nothing to report.

Author: samuelburnham

LeanUpdate/Input.lean

@@ -193,6 +193,28 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
     throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
   return kept
 
+/-- What to do when a target package's Mathlib cache cannot be fetched.
+
+Defaults to `require`: building Mathlib from source takes hours and usually ends in a timeout,
+so a run that silently falls back to it costs far more than the one that stops. -/
+public inductive MathlibCache where
+  /-- fail validation when `lake exe cache get` fails -/
+  | require
+  /-- report the failure and build without the cache -/
+  | optional
+deriving Repr, BEq, ToString, HasParser
+
+public instance : Input MathlibCache where
+  envName := "MATHLIB_CACHE"
+  parse := parseAs MathlibCache
+  localValue? := some .require
+
+#guard
+  let lst : List MathlibCache := [.require, .optional]
+  lst.map toString == ["require", "optional"]
+
+#guard (parseAs MathlibCache "optional").toOption == some .optional
+
 /-- The input whether to update the `lean-toolchain` file. -/
 public inductive UpdateLeanToolchain where
   | auto

LeanUpdate/PostUpdateValidation.lean

@@ -98,26 +98,35 @@ def dependsOnMathlib (cwd : FilePath) : IO Bool := do
     return false
   return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"
 
-/-- Download Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.
+/-- Get Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.
 
 Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
 per package; the downloads behind it are pooled in a single per-user directory, so only the first
-package pays for the network. Failing to get the cache only means a slower build, so it is
-reported rather than raised.
+package pays for the network. Whether a failure stops the run is `MathlibCache`'s to decide.
 -/
-def getMathlibCache (cwd : FilePath) : IO Unit := do
+def getMathlibCache (cwd : FilePath) : IO (Except String Unit) := do
   unless ← dependsOnMathlib cwd do
-    return
+    return .ok ()
   IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
   let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
-  if out.exitCode != 0 then
+  if out.exitCode == 0 then
+    return .ok ()
+  let details := out.stdout.trimAscii.copy ++ "\n" ++ out.stderr.trimAscii.copy
+  match ← GitHub.Action.Input.get MathlibCache with
+  | .optional =>
     IO.println <| log%
       s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
+    return .ok ()
+  | .require =>
+    return .error s!"`lake exe cache get` exited with {out.exitCode}\n{details}"
 
 /-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
 def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
     IO PostUpdateValidationResult := do
-  getMathlibCache targetLakePackageDir
+  match ← getMathlibCache targetLakePackageDir with
+  | .error e =>
+    return { buildResult := .error e, testResult? := none, lintResult? := none }
+  | .ok _ => pure ()
   let buildResult ← runLakeBuild targetLakePackageDir buildArgs
 
   let hasTestDriverResult ← hasTestDriver targetLakePackageDir

action.yml

@@ -102,6 +102,17 @@ inputs:
       Build arguments to pass to `lake build` during post-update validation.
     required: false
     default: "--log-level=warning"
+  mathlib_cache:
+    description: |
+      What to do when a target package depends on Mathlib and `lake exe cache get` fails.
+      Allowed values:
+        * `require`: fail validation, reporting the directory and the cache output (default)
+        * `optional`: report the failure and build without the cache
+      Building Mathlib from source takes hours and usually ends in a timeout, so falling back to
+      it silently costs far more than stopping does. Set `optional` when a slow build is
+      preferable to no answer at all.
+    required: false
+    default: "require"
   validate:
     description: |
       Whether to run post-update validation (`lake build`, and `lake test`/`lake lint` when
@@ -330,6 +341,7 @@ runs:
         lake exe leanUpdate validateUpdate
       env:
         BUILD_ARGS: ${{ inputs.build_args }}
+        MATHLIB_CACHE: ${{ inputs.mathlib_cache }}
         LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
       shell: bash
       working-directory: ${{ github.action_path }}
@@ -428,6 +440,7 @@ runs:
         # Could be best to use the default token here
         GH_TOKEN: ${{ inputs.token }}
         BUILD_ARGS: ${{ inputs.build_args }}
+        MATHLIB_CACHE: ${{ inputs.mathlib_cache }}
         LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
       shell: bash
       working-directory: ${{ github.action_path }}
@@ -452,6 +465,7 @@ runs:
       env:
         GH_TOKEN: ${{ inputs.token }}
         BUILD_ARGS: ${{ inputs.build_args }}
+        MATHLIB_CACHE: ${{ inputs.mathlib_cache }}
         LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
       shell: bash
       working-directory: ${{ github.action_path }}