Skip to content

Commit

Permalink
chore: skip all '._' files
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Oct 24, 2023
1 parent 777278f commit 04b771a
Showing 1 changed file with 5 additions and 4 deletions.
9 changes: 5 additions & 4 deletions Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -56,10 +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
-- 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
-- It appears that sometimes with ProofWidgets
-- (or more generally anything delivered via `lake release`)
-- contains files like `._ProofWidgets.olean` (which is not a real `.olean` file).
-- We just skip these files, as otherwise they break Mathlib CI:
unless s!"{m}".take 3 = "«._" do
tasks := tasks.push (m, ← IO.asTask (replayFromImports m))
for (m, t) in tasks do
if let .error e := t.get then
Expand Down

0 comments on commit 04b771a

Please sign in to comment.