Error: No space left on device

Stream: mathlib4

[Jack McKoen]

I pushed some changes to my PR #13710 and the build immediately failed with
Error: No space left on device : '/home/lean/actions-runner/_work/_actions/dcarbone/install-jq-action/v1.0.1'
What does this error mean?

[Matthew Ballard]

The computer running the CI ran out of fish space. Nothing you did

[Jack McKoen]

Thanks, that makes sense :sweat_smile:

[Bryan Gin-ge Chen]

I've taken the faulty machine out of the pool of runners until it can be fixed; hopefully you won't run into this again if you re-run the job.

[Damiano Testa]

I also hit this here.

[Bryan Gin-ge Chen]

OK, I've removed that runner temporarily.

[Bryan Gin-ge Chen]

According to @Wojciech Nawrocki who is working on fixing this, there might be a branch or PR which is generating abnormally large oleans. Does that ring a bell for anyone?

[Matthew Ballard]

I saw abnormally large oleans earlier today

[Matthew Ballard]

@Damiano Testa

[Matthew Ballard]

But I saw failures yesterday too

[Damiano Testa]

I was experimenting with the abnormally large oleans yesterday indeed...

[Damiano Testa]

I hope that the new PRs do not suffer from the same problem.

[Matthew Ballard]

Was it all on branch#adomani/linter_assertNotExists_or_imported?

[Damiano Testa]

I think that this one might be the good one. If a branch starts with test or ends in dev it can safely be removed.

[Damiano Testa]

Unless of course that branch (https://github.com/leanprover-community/mathlib4/tree/adomani%2Flinter_assertNotExists_or_imported) has large oleans, in which case I need to work more on the PR.

[Damiano Testa]

(I'm not at a computer, so I'm not able to remove the branches that I think are large.)

[Bryan Gin-ge Chen]

I think it's OK if the branches exist in the repo; we just don't want CI to run on them.

Though maybe we just need our CI workflow to clean up the runners more thoroughly.

[Damiano Testa]

Anyway, I'll remove the branches, probably tomorrow. If you want to remove the oleans as well, feel free to do so for all my PRs.

[Matthew Ballard]

Is this just preventing future bloat or can things be cleaned out more surgically with precise knowledge of the problem?

[Damiano Testa]

Should there be a CI step that reports the size of the oleans?

[Bryan Gin-ge Chen]

More info never hurts... probably.

[Damiano Testa]

So, a du invocation in check the cache, maybe?

[Damiano Testa]

I had never considered this issue before, but calling du -h, even just on .lake should be cheap and informative.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Damiano Testa said:

Should there be a CI step that reports the size of the oleans?

This is a good idea

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Damiano Testa said:

Unless of course that branch (https://github.com/leanprover-community/mathlib4/tree/adomani%2Flinter_assertNotExists_or_imported) has large oleans, in which case I need to work more on the PR.

I don't think it's that branch, at least not on the latest commit. It produces about the expected size

[Damiano Testa]

I am happy to hear that the oleans of that branch are normal-sized, since that is the branch that I contains the "good" version of the PR!

I also think that branch#adomani/linter_assertNotExists_or_imported_dev is the one with the big oleans and I deleted it. The latest commit might have reasonable sized ones, but the earlier commits probably were the ones filling up memory: sorry!

[Damiano Testa]

Also, #16020 adds a report of the size of .lake. Most of the space in .lake is the oleans, so I only added the size of the whole dir, rather than the sizes of all the subdirs. Let me know if you think a more granular approach is more informative.

[Damiano Testa]

If you expand check the cache in this CI run, the last line tells you the size of .lake.

[Rémy Degenne]

I just got a "no space left on device" in CI for PR #22271 (running on hoskinson2).

[Daniel Weber]

I alao got this in #22180

[Jakob von Raumer]

Me too, guess someone either needs to clear some caches or pay someone else more money :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

#22280 also hit this (does anyone dare merge it anyway? ;-) )

[Kevin Buzzard]

(deleted)

[Bryan Gin-ge Chen]

@Wojciech Nawrocki Could you take a look when you have a chance?

[Bryan Gin-ge Chen]

For now, I've removed the bors and pr tags from hoskinson2 so no more jobs should go its way. I've also retriggered CI / bors on the abovementioned PRs.

[Jakob von Raumer]

Can you restart #22248 as well?

[Floris van Doorn]

done

[Bryan Gin-ge Chen]

(Note that if you have write access to mathlib, you should be able to restart failed jobs yourself by clicking the "Re-run jobs" button in the upper right corner on the CI job page: https://github.com/leanprover-community/mathlib4/actions/runs/13518357916/job/37780479089)

[Kevin Buzzard]

(this is true but it wasn't clear to me whether spamming the runners was a good idea when there was a problem with the runners)

[Bryan Gin-ge Chen]

Right, I maybe also should have added: in general don't try re-running a job unless you have a reasonable expectation that the same thing won't happen again. Also, if you have to resort to re-running, it's probably a good idea to report it on Zulip as well. In this case it doesn't look like any other runners are broken and there's already a thread here so it's pretty safe.

[Kevin Buzzard]

My ignorance of the system is sufficiently deep that I didn't know whether (a) hitting retry would send it to the same machine again and (b) whether one machine having the problem meant that all machines had the problem. This was why I didn't retry. I was happy to wait :-)

[Bryan Gin-ge Chen]

With regards to (a), GitHub actions searches for a new runner every time a job is started. To be quite honest I was gambling a bit on (b) not being the case - I figured that the worst that could happen is that we'd find out a few more runners were broken, and better to find out sooner rather than later, so that Wojciech can reset them all in one go.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

The main issue seems to be ~60GiB of .cache. There is already code to cleanup the toolchains, should there also be something to clean up .cache?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

hoskinson2 should be back up.

[Pim Otte]

@Wojciech Nawrocki Fyi, this build makes it seem like hoskinson7 has the same issue:)

[Sébastien Gouëzel]

@Bryan Gin-ge Chen , indeed it looks like hoskinson7 is also full.

[Jakob von Raumer]

Yes, just hit this on hoskinson7 for #22248 as well

[Floris van Doorn]

Maybe the runners can do a weekly/monthly lake exe cache clean?

[Bryan Gin-ge Chen]

I've removed the pr and bors labels from hoskinson7. BTW, any maintainer should be able to do this via https://github.com/organizations/leanprover-community/settings/actions/runners (click on the runner name, then on the gear icon next to the list of tags to edit them)

[Floris van Doorn]

I tried to do this just now, but didn't find how to do this (I tried to press the dots to the right of the runner, which only gives the option to delete the runner).

[Bryan Gin-ge Chen]

Oh, can't you click the runner name itself? Doing so takes me to a page like this: https://github.com/organizations/leanprover-community/settings/actions/runners/106
edit: ah, I guess maybe you meant before you saw my message

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Cleaned hoskinson7. Actually, cleaned all of them as they all seem to be running out of .cache space. This may result in some one-off build failures.

[Floris van Doorn]

Bryan Gin-ge Chen said:

Oh, can't you click the runner name itself? Doing so takes me to a page like this: https://github.com/organizations/leanprover-community/settings/actions/runners/106
edit: ah, I guess maybe you meant before you saw my message

Sorry, I indeed wasn't clear in my previous message. I indeed meant before reading what you wrote. Thanks for the clarification!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

The main issue seems to be ~60GiB of .cache. There is already code to cleanup the toolchains, should there also be something to clean up .cache?

FYI, we are seeing more build failures because of this. I would recommend adding a .cache cleaning step.

[Bryan Gin-ge Chen]

If someone can confirm that all we need is a weekly action to run lake exe cache clean on the self-hosted runners than I can put that together later today.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I cannot confirm that it won't run out of space for other reasons, but all of the runner disk space issues happening recently have been due to .cache folders growing large; it would certainly help prevent that.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

If I understand the CI scripts, cleaning toolchains happens on every build. Are you suggesting to have a dedicated CI action just for cleaning .cache that is somehow scheduled to run weekly?

[Bryan Gin-ge Chen]

That was my understanding of @Floris van Doorn’s message above; sorry, I should have linked it earlier:

Floris van Doorn said:

Maybe the runners can do a weekly/monthly lake exe cache clean?

[Bryan Gin-ge Chen]

Ah, thinking about this more, the CI action approach doesn't really make sense after all, since it's not guaranteed that it will run on every machine. Not sure what I was thinking... would it be possible to set up a weekly cron job on the machines that runs lake exe cache clean then? Maybe we could even have them each send a weekly message to a Zulip channel with basic diagnostic info.

[Kim Morrison]

Why not just include this in the standard CI? On every run, check the size of the cache directory, and if it is above some limit, clear it out.

[Kim Morrison]

One could even be clever and delete the oldest files, hopefully avoiding any cache misses.

[Bryan Gin-ge Chen]

OK! I put together something (with Claude's help) in #22863.

[Kevin Buzzard]

I guess a potential cron job might remove a bunch of oleans in the middle of a CI run, which would be an exciting new way of things going wrong...

[Damiano Testa]

The I'm feeling naughty cron job.

[Bryan Gin-ge Chen]

Bryan Gin-ge Chen said:

OK! I put together something (with Claude's help) in #22863.

This is now merged so hopefully this thread will be quiet from now on...

[Arthur Paulino]

I'd suggest at least some way of getting a feel for how big the current mathlib cache is. Losing track of this number will some day put maintainers in a hurry, with a tight response time.

One loose method is following up the cache clean with a message to be posted here on Zulip. Then if the cleanup is being performed every two weeks or so, things are about to get really ugly.

[Bryan Gin-ge Chen]

For the time being, the workflow step is logging the total size of the cache folder on that specific machine: looks like it's around 5 GB on hoskinson9 at the moment.

[Arthur Paulino]

Minor: with du -sh instead of du -sb it would print the size in "human readable format". (e.g. 1K, 234M, 2G etc). So you'd be able to remove the "(in bytes)" part from the printed string. Though I see you're using that same number for the check of size

[Junyan Xu]

I'm getting

/home/lean/actions-runner/_work/_temp/2ee3dddc-a39c-4a1f-94d4-804fedfb62b4.sh: line 17: lake: command not found
Cache size (in bytes): 47178990759
Cache size exceeds threshold, running lake exe cache clean
Error: Process completed with exit code 127.

on #22885

[Bryan Gin-ge Chen]

Ah, that was silly. lake isn't installed yet in that step. :man_facepalming:
Let me put together a quick fix.

[Bryan Gin-ge Chen]

@Damiano Testa if you're around, would mind putting #22887 on the queue real quick before this breaks more builds? Looks like we have a red checkmark on master due to this issue as well... for now I'll remove the tags from hoskinson5 temporarily.

[Damiano Testa]

Oops, I should have also noticed that lake was not available!

[Junyan Xu]

Seems I bumped into another machine with almost full cache:

/home/lean/actions-runner/_work/_temp/92b4c16c-37b2-4537-88b9-6011d77103cc.sh: line 17: lake: command not found
Cache size (in bytes): 43540418002
Cache size exceeds threshold, running lake exe cache clean
Error: Process completed with exit code 127.

[Bryan Gin-ge Chen]

Looks like that was hoskinson1 this time. Sorry for all the trouble!

[Junyan Xu]

No worries, thanks for the quick fix!

[Damiano Testa]

The PR with the fix seems to be going well through CI!

[Damiano Testa]

And the "clean up" step was executed and gave no problem.

[Bryan Gin-ge Chen]

Great! I've re-enabled hoskinson1 and hoskinson5.