From 777278fd59d7d42390d540a1b00b441389ef1395 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 24 Oct 2023 16:29:10 +1100 Subject: [PATCH] chore: skip lakefile.olean from ProofWidgets --- Main.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Main.lean b/Main.lean index d44ad9f..e236ce9 100644 --- a/Main.lean +++ b/Main.lean @@ -56,7 +56,11 @@ unsafe def main (args : List String) : IO UInt32 := do let mut tasks := #[] for path in (← SearchPath.findAllWithExt sp "olean") do if let some m := (← searchModuleNameOfFileName path sp) then - tasks := tasks.push (m, ← IO.asTask (replayFromImports m)) + -- It appears that `lakefile.olean`s are delivered via the lake release feature. + -- Pending answers about that https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ProofWidgets.20bump.20required/near/398206560 + -- we just skip a file that otherwise breaks Mathlib CI here: + unless s!"{m}" = "«._ProofWidgets»" do + tasks := tasks.push (m, ← IO.asTask (replayFromImports m)) for (m, t) in tasks do if let .error e := t.get then IO.eprintln s!"lean4checker found a problem in {m}"