CI error

Stream: mathlib4

[Sébastien Gouëzel]

I just got an unusual error from CI at https://github.com/leanprover-community/mathlib4/actions/runs/15684213692/job/44183232852: the cleanup step failed with

rm: cannot remove './pr-branch/.lake/build/ir/Mathlib/Data': Directory not empty

[Bryan Gin-ge Chen]

I took a look and it seems to be coming from this line which just tries to delete everything in the working directory, but we haven't changed that step since before the transition to forks. I don't know what could have changed here, maybe @Kim Morrison will have an idea. Anyways, if we see more failures on hoskinson7 we may have to disable it temporarily.

[Bryan Gin-ge Chen]

Claude suggested that the find command may have tried to delete a directory before it was emptied, and suggested a simpler command which I've put in #25967.

[Joscha Mennicken]

But the find command already calls rm -rf, which shouldn't fail on directories because it recursively deletes files before deleting the directory itself. It might fail if something else is creating new files while rm -rf is running.

[Robin Carlier]

Got hit by this in #25755 as well

[Bryan Gin-ge Chen]

Looks like it was hoskinson7 again. @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 when you have a chance could you investigate if there's something interfering with the cleanup step? Here's the log in question: https://github.com/leanprover-community/mathlib4/actions/runs/15771328806/job/44456712233#step:2:15

[Bryan Gin-ge Chen]

I also found a failure on hoskinson5: https://github.com/leanprover-community/mathlib4/actions/runs/15773286144/attempts/1?pr=26173

[Bryan Gin-ge Chen]

The effect of these should hopefully be alleviated by #26420. Thanks Kim!