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:

view this post on Zulip Théo Zimmermann (Mar 20 2023 at 22:13):

@Maxime Dénès I'm getting a lot of errors like this again. See https://gitlab.com/coq/coq/-/jobs/3967868406 and https://gitlab.com/coq/coq/-/jobs/3967868389 for examples. They are on ci-coq-02-runner-03 and coq-gitlab-runner-10.ci.

view this post on Zulip Théo Zimmermann (Mar 23 2023 at 14:05):

Same problem on ci-coq-01-runner-06 at https://gitlab.com/coq/coq/-/jobs/3988774436


Last updated: Dec 07 2023 at 06:38 UTC