@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?
the reduced default CI PR was merged
I'm not working on anything atm
I'm preparing runners on Inria VMs
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.
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.
I added 8 runners from Inria CloudStack.
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.
I'm investigating system failures on the runners.
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.
I added 12 runners from our bench machines. Two machines remain dedicated for benchmarking, which should be enough for now.
Last updated: Jun 05 2023 at 09:01 UTC