Skip to content

Commit bde7e02

Browse files
committed
fix(Cache): misleading ProofWidgets fetch failure (leanprover-community#29886)
This PR fixes an issue with `lake cache get` where it would incorrectly appear that cache failed to ProofWidgets. This was caused by cache printing output of the `lake build --no-build` invocation used to check whether a fetch was necessary. This also improves the output on a real failure by the running the `lake build` command to fetch the release with a `-v` and only printing the output on a failure.
1 parent f914ea5 commit bde7e02

File tree

1 file changed

+25
-7
lines changed

1 file changed

+25
-7
lines changed

Cache/Requests.lean

Lines changed: 25 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -440,23 +440,41 @@ def getProofWidgets (buildDir : FilePath) : IO Unit := do
440440
-- Check if the ProofWidgets build is out-of-date via `lake`.
441441
-- This is done through Lake as cache has no simple heuristic
442442
-- to determine whether the ProofWidgets JS is out-of-date.
443-
let exitCode ← (← IO.Process.spawn {cmd := "lake", args := #["-q", "build", "--no-build", "proofwidgets:release"]}).wait
444-
if exitCode == 0 then -- up-to-date
443+
let out ← IO.Process.output
444+
{cmd := "lake", args := #["-v", "build", "--no-build", "proofwidgets:release"]}
445+
if out.exitCode == 0 then -- up-to-date
445446
return
446-
else if exitCode == 3 then -- needs fetch (`--no-build` triggered)
447+
else if out.exitCode == 3 then -- needs fetch (`--no-build` triggered)
447448
pure ()
448449
else
449-
throw <| IO.userError s!"Failed to validate ProofWidgets cloud release: lake failed with error code {exitCode}"
450+
printLakeOutput out
451+
throw <| IO.userError s!"Failed to validate ProofWidgets cloud release: \
452+
lake failed with error code {out.exitCode}"
450453
-- Download and unpack the ProofWidgets cloud release (for its `.js` files)
451-
let exitCode ← (← IO.Process.spawn {cmd := "lake", args := #["-q", "build", "proofwidgets:release"]}).wait
452-
if exitCode != 0 then
453-
throw <| IO.userError s!"Failed to fetch ProofWidgets cloud release: lake failed with error code {exitCode}"
454+
IO.print "Fetching ProofWidgets cloud release..."
455+
let out ← IO.Process.output
456+
{cmd := "lake", args := #["-v", "build", "proofwidgets:release"]}
457+
if out.exitCode == 0 then
458+
IO.println " done!"
459+
else
460+
IO.print "\n"
461+
printLakeOutput out
462+
throw <| IO.userError s!"Failed to fetch ProofWidgets cloud release: \
463+
lake failed with error code {out.exitCode}"
454464
-- Prune non-JS ProofWidgets files (e.g., `olean`, `.c`)
455465
try
456466
IO.FS.removeDirAll (buildDir / "lib")
457467
IO.FS.removeDirAll (buildDir / "ir")
458468
catch e =>
459469
throw <| IO.userError s!"Failed to prune ProofWidgets cloud release: {e}"
470+
where
471+
printLakeOutput out := do
472+
unless out.stdout.isEmpty do
473+
IO.eprintln "lake stdout:"
474+
IO.eprint out.stderr
475+
unless out.stderr.isEmpty do
476+
IO.eprintln "lake stderr:"
477+
IO.eprint out.stderr
460478

461479
/-- Downloads missing files, and unpacks files. -/
462480
def getFiles

0 commit comments

Comments
 (0)