Jason Gross (May 21 2021 at 16:46): Jason Gross (May 21 2021 at 16:46):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?
Théo Zimmermann (May 21 2021 at 16:47):I think it should be a fatal error: the bug minimizer shouldn't have to manage everything else in the world.
Théo Zimmermann (May 21 2021 at 16:48):And then, if we decide this happens too often, we should consider even more than before how to alleviate this problem.
Jason Gross (May 21 2021 at 16:58):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.
Jason Gross (May 21 2021 at 16:59):(Current status is that I'm still trying to get a full minimization run on https://github.com/coq/coq/pull/14328)
Théo Zimmermann (May 22 2021 at 12:31):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?
Jason Gross (May 23 2021 at 01:15):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 string_match ~regexp:"test-suite"?
Théo Zimmermann (May 23 2021 at 11:45):I guess the latter would be more bullet-proof.
Jason Gross (May 23 2021 at 11:53):Updated, should be redeployed in 10
Last updated: May 28 2023 at 18:29 UTC