Debugging failed "Build mathlib" check

Stream: new members

[Sebastian Monnet]

My PR #13307 is failing the continuous integration / Build mathlib (push) check and I'm unable to figure out why.

The first thing I tried was looking through the code in the "Files changed" section of the PR, which usually contains error messages when my commits fail linter checks. This didn't work though, since I guess building mathlib is much more complicated than checking style.

I also tried running leanproject get-cache on my machine, expecting that my code would stop compiling as a result of something in the new mathlib, but everything still seems to work.

I'm not sure how to find the problem - can anyone advise me? Thanks!

[Yaël Dillies]

This means the runner (the machine running CI) disconnected from the network. I've just restarted the job.

[Sebastian Monnet]

Oh, so the code is probably fine? Why would the runner disconnect?

[Yaël Dillies]

Yeah it's not your fault. I'm not sure why the runner disconnected but there are several possible reasons:

• It crashed
• It ran out of memory
• It genuinely lost the internet connection

[Sebastian Monnet]

Makes sense - thanks for your help:)