Skip to content

Commit

Permalink
chore: skip lakefile.olean from ProofWidgets
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Oct 24, 2023
1 parent 005e771 commit 777278f
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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}"
Expand Down

0 comments on commit 777278f

Please sign in to comment.