What should we do when the base job hasn't run? (e.g., https://gitlab.com/coq/coq/-/pipelines/306442866 says "The pipeline job activity limit was exceeded.") The artifact urls are created but fail to download. Should I make the bug minimizer rebuild the base job itself? Or should this be a fatal error, and the solution should be to start the base job on Coq?
I think it should be a fatal error: the bug minimizer shouldn't have to manage everything else in the world.
And then, if we decide this happens too often, we should consider even more than before how to alleviate this problem.
In any case, I think the coqbot interaction part of CI minimization is now working well, and I'm hopeful that the rest of the changes will not need further updates to coqbot.
(Current status is that I'm still trying to get a full minimization run on https://github.com/coq/coq/pull/14328)
This comment posted 18 hours ago looks like a bug. There were failures in the test-suite jobs, not just in the VST job (see https://github.com/coq/coq/runs/2640956167). Do you understand what happened?
I bet the issue is that we're doing
String.is_prefix name ~prefix:"test-suite" on
GitLab CI job test-suite:base (pull request). Should we instead do
String.is_prefix name ~prefix:"GitLab CI job test-suite"? Or
I guess the latter would be more bullet-proof.
Updated, should be redeployed in 10
Last updated: Jan 31 2023 at 10:01 UTC