From 3bc63aefb75dba8a850a0de9148c71c09242a28f Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Wed, 21 Jan 2026 22:27:30 -0500
Subject: [PATCH] fix: lake: small cache issues (#12037)

This PR fixes two Lake cache issues: a bug where a failed upload would
not produce an error and a mistake in the `--wfail` checks of the cache
commands.
---
 src/lake/Lake/CLI/Main.lean           |  6 +++---
 src/lake/Lake/Config/Cache.lean       | 18 +++++++++++++++---
 tests/lake/tests/cache/online-test.sh | 12 +++++++++++-
 3 files changed, 29 insertions(+), 7 deletions(-)

diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index 7684acdd6a..443c1757a3 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -395,7 +395,7 @@ protected def get : CliM PUnit := do
   if let some file := mappings? then liftM (m := LoggerIO) do
     if opts.platform?.isSome || opts.toolchain?.isSome then
       logWarning "the `--platform` and `--toolchain` options do nothing for `cache get` with a mappings file"
-      if .warning ≤ opts.failLv then
+      if opts.failLv ≤ .warning then
         failure
     let some remoteScope := opts.scope?
       | error "to use `cache get` with a mappings file, `--scope` or `--repo` must be set"
@@ -470,7 +470,7 @@ where
     if (← repo.hasDiff) then
       logWarning s!"{pkg.prettyName}: package has changes; \
         only artifacts for committed code will be downloaded"
-      if .warning ≤ opts.failLv then
+      if opts.failLv ≤ .warning then
         failure
     let n := opts.maxRevs
     let revs ← repo.getHeadRevisions n
@@ -505,7 +505,7 @@ protected def put : CliM PUnit := do
   if (← repo.hasDiff) then
     logWarning s!"{pkg.prettyName}: package has changes; \
       artifacts will be uploaded for the most recent commit"
-    if .warning ≤ opts.failLv then
+    if opts.failLv ≤ .warning then
       exit 1
   let rev ← repo.getHeadRevision
   let map ← CacheMap.load file
diff --git a/src/lake/Lake/Config/Cache.lean b/src/lake/Lake/Config/Cache.lean
index 2961889714..933aa86130 100644
--- a/src/lake/Lake/Config/Cache.lean
+++ b/src/lake/Lake/Config/Cache.lean
@@ -13,6 +13,7 @@ import Lake.Build.Actions
 import Lake.Util.Url
 import Lake.Util.Proc
 import Lake.Util.Reservoir
+import Lake.Util.JsonObject
 import Lake.Util.IO
 import Init.Data.String.Search
 import Init.Data.String.Lemmas.Basic
@@ -305,15 +306,26 @@ end Cache
 def uploadS3
   (file : FilePath) (contentType : String) (url : String) (key : String)
 : LoggerIO Unit := do
-  proc {
+  let out ← captureProc' {
     cmd := "curl"
     args := #[
-      "-s",
+      "-s", "-w", "%{stderr}%{json}\n",
       "--aws-sigv4", "aws:amz:auto:s3", "--user", key,
       "-X", "PUT", "-T", file.toString, url,
       "-H",  s!"Content-Type: {contentType}"
     ]
-  } (quiet := true)
+  }
+  match Json.parse out.stderr >>= JsonObject.fromJson? with
+  | .ok data =>
+    let code ← id do
+      match (data.get? "response_code" <|> data.get? "http_code") with
+      | .ok (some code) => return code
+      | .ok none => error s!"curl's JSON output did not contain a response code"
+      | .error e => error s!"curl's JSON output contained an invalid JSON response code: {e}"
+    unless code == 200 do
+      error s!"failed to upload artifact, error {code}; received:\n{out.stdout}"
+  | .error e =>
+    error s!"curl produced invalid JSON output: {e}"
 
 /--
 Configuration of a remote cache service (e.g., Reservoir or an S3 bucket).
diff --git a/tests/lake/tests/cache/online-test.sh b/tests/lake/tests/cache/online-test.sh
index ca07c1dfbb..a9bd3b10e0 100755
--- a/tests/lake/tests/cache/online-test.sh
+++ b/tests/lake/tests/cache/online-test.sh
@@ -34,6 +34,12 @@ with_cdn_endpoints() {
   "$@"
 }
 
+with_bogus_endpoints() {
+  LAKE_CACHE_ARTIFACT_ENDPOINT=https://example.com \
+  LAKE_CACHE_REVISION_ENDPOINT=https://example.com \
+  "$@"
+}
+
 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the repository on each test.
 init_git
@@ -79,7 +85,7 @@ test_err "revision not found" cache get --repo='leanprover/bogus' --rev='bogus'
 test_err "outputs not found for revision" cache get --repo='leanprover/bogus' --rev=$REV
 
 # Test `cache get` skipping non-Reservoir dependencies
-test_run -f  non-reservoir.toml update
+test_run -f non-reservoir.toml update
 test_out 'hello: skipping non-Reservoir dependency' -f non-reservoir.toml cache get
 
 # Build artifacts
@@ -88,6 +94,10 @@ test_exp -f .lake/outputs.jsonl
 test_cmd_eq 3 wc -l < .lake/outputs.jsonl
 test_cmd cp -r .lake/cache .lake/cache-backup
 
+# Test fetch from invalid URL
+with_bogus_endpoints test_err "failed to upload artifact" \
+  cache put .lake/outputs.jsonl --scope='!/test'
+
 # Test cache put/get with a custom endpoint
 with_upload_endpoints test_run cache put .lake/outputs.jsonl --scope='!/test'
 test_cmd rm -rf .lake/build "$LAKE_CACHE_DIR"