Stream: Coq devs & plugin devs

Topic: No space left on device


view this post on Zulip Enrico Tassi (Jan 16 2022 at 15:27):

$ dev/tools/check-cachekey.sh
$ tar xfj _build.tar.bz2
tar: _build/default/theories/Init/Specif.glob: Cannot write: No space left on device

This is on a snared runner... ideas?

view this post on Zulip Gaëtan Gilbert (Jan 16 2022 at 17:46):

context?

view this post on Zulip Enrico Tassi (Jan 16 2022 at 21:41):

example: https://gitlab.com/coq/coq/-/jobs/1980350426

view this post on Zulip Enrico Tassi (Jan 16 2022 at 21:42):

but I've seen it in different jobs IIRC

view this post on Zulip Enrico Tassi (Jan 17 2022 at 09:15):

Another one: https://github.com/coq/coq/pull/15220/checks?check_run_id=4838419593

view this post on Zulip Gaëtan Gilbert (Jan 17 2022 at 09:42):

Enrico Tassi said:

This is on a snared runner... ideas?

This Runner: #857051 is not a shared runner, it says it's ours https://gitlab.com/coq/coq/-/runners/857051
no idea where it comes from
If it's a problem we can disable it

view this post on Zulip Enrico Tassi (Jan 17 2022 at 09:58):

It must be someone eavesdropping on our secret code :-)

view this post on Zulip Guillaume Melquiond (Jan 17 2022 at 10:07):

Secret code, maybe not, but if you control a runner, you actually have access to all the secret keys, which is not a good prospect.

view this post on Zulip Théo Zimmermann (Jan 17 2023 at 17:02):

FWIW, I had three jobs fail with "No space left on device" on runner ci-coq-02-runner-04 yesterday:


Last updated: Feb 06 2023 at 18:03 UTC