Stream: Coq devs & plugin devs

Topic: Actions taken on CI because of minutes running out


view this post on Zulip Maxime Dénès (Oct 03 2022 at 18:43):

@Théo Zimmermann @Gaëtan Gilbert @Pierre-Marie Pédrot Can you summarize what was done on CI so far, and if you are currently working on some more actions?

view this post on Zulip Gaëtan Gilbert (Oct 03 2022 at 18:43):

the reduced default CI PR was merged
I'm not working on anything atm

view this post on Zulip Maxime Dénès (Oct 03 2022 at 19:07):

I'm preparing runners on Inria VMs

view this post on Zulip Théo Zimmermann (Oct 04 2022 at 07:06):

I'm working on updates to coqbot to handle better the reduced default CI mechanism (inform reviewers and give an option to trigger a full CI, probably with a label). Please direct any suggestion for how to handle this to https://github.com/coq/bot/issues/159.

view this post on Zulip Théo Zimmermann (Oct 04 2022 at 07:30):

Something else that I planned to work on this week (independently of this problem) was to migrate the Nix infrastructure in the Coq repo to use the Coq Nix Toolbox. Then, the plan was to use the auto-generated GitHub Action and remove the GitLab job. So this action would also alleviate the GitLab CI a little.

view this post on Zulip Maxime Dénès (Oct 04 2022 at 12:41):

I added 8 runners from Inria CloudStack.

view this post on Zulip Maxime Dénès (Oct 11 2022 at 09:24):

I will remove the runners we have, to replace them with new ones featuring proper VM sandboxing. You may have to restart some failed jobs after that, sorry for the inconvenience.

view this post on Zulip Maxime Dénès (Oct 12 2022 at 07:17):

I'm investigating system failures on the runners.

view this post on Zulip Maxime Dénès (Oct 12 2022 at 09:00):

Should be now fixed. Rootcause: we reached our CloudStack quota limit, because the osx runner is using more than I thought. Some jobs may need to be restarted.

view this post on Zulip Maxime Dénès (Oct 14 2022 at 22:41):

I added 12 runners from our bench machines. Two machines remain dedicated for benchmarking, which should be enough for now.


Last updated: Feb 01 2023 at 15:04 UTC