CI "lake exe mk_all" failure

Stream: mathlib4

[Nailin Guan]

In my PR #31706, CI failed and showed the following. But when I run lake exe mk_all, it showed No update necessary.
图片.png

[Nailin Guan]

There is also another error. I also have no idea.
图片.png

[Bryan Gin-ge Chen]

For the second one, I think it might be fixed if you merge master into your branch.

[Nailin Guan]

The first problem also happened to many other PRs of mine. I have no idea why only changing name of some lemma cause this problem.

[Vasilii Nesterov]

It happened to my #31673 too and after merging master it failed with

The self-hosted runner lost communication with the server. Verify the machine is running and has a healthy network connection. Anything in your workflow that terminates the runner process, starves it for CPU/Memory, or blocks its network access can cause this error.

https://github.com/leanprover-community/mathlib4/actions/runs/19425942369

[Kevin Buzzard]

I've hit "rerun jobs" in the hope that this is a transient network error.

[Bryan Gin-ge Chen]

It looks like the runner this job was running on went down (along with another one, so there's probably another job out there that failed with the same error). I've just restarted them.

[Kenny Lau]

#30336 is also failing with a mysterious error, can someone confirm that master is ok before i merge master

[Bryan Gin-ge Chen]

#30336 looks like an occurrence of #mathlib4 > "verify that everything was available in the cache" fails CI @ 💬 . Merging master or pushing more commits should eventually fix it.

[Nailin Guan]

Updates

Nailin Guan 說：

In my PR #31706, CI failed and showed the following. But when I run lake exe mk_all, it showed No update necessary.
图片.png

today broke my PR by this problem, in both #31697 #31706, do anyone know why?

[Damiano Testa]

I wonder whether the mk_all error is simply due to the fact that the step with the mk_all command did not run, as the proofWidgets one broke before it.

[Damiano Testa]

So, I suspect that, in case the early mk_all step does not run, maybe CI should not run the later mk_all step.

[Nailin Guan]

Thanks for your deduction, I'll try update then.

[Damiano Testa]

#31743

[Damiano Testa]

Now that the PR above has been merged, if you merge master it will probably not solve the issue, but mk_all should no longer complain! :upside_down: