Warning: ... not found. Skipping all files that depend on it

Stream: general

[Yaël Dillies]

I just saw an insane job where the runner printed out

Warning: ./Mathlib/Algebra/Support.lean not found. Skipping all files that depend on it

for 6 hours. Arguably, the PR is not building (I am moving Algebra.Support to Algebra.Support.Basic and forgot to update some of the import Mathlib.Algebra.Support), but this still is an impressive failure mode.

[Mario Carneiro]

I have seen this issue before, there was a bug fix to cache to fix it. How old is the mathlib branch you are testing?

[Yaël Dillies]

It's branch#sink_support whose latest master commit is https://github.com/leanprover-community/mathlib4/commit/5d4fa55028ca22525074d4c2141f8f2a04dc0e32 from earlier today.

[Mario Carneiro]

wait a minute, the bug fix never landed

[Mario Carneiro]

now I have to find where it ended up

[Mario Carneiro]

#7876

[Mario Carneiro]

Well I cherry picked that commit to sink_support and it fixes the infinite loop so I'm going to call that a successful test

[Mario Carneiro]

(Note that this only happens when you import a file that doesn't exist, so it would have already failed for other reasons)