Stream: coqbot devs & users

Topic: CI minimization


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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"?

view this post on Zulip Théo Zimmermann (May 23 2021 at 11:45):

I guess the latter would be more bullet-proof.

view this post on Zulip Jason Gross (May 23 2021 at 11:53):

Updated, should be redeployed in 10


Last updated: Jan 31 2023 at 10:01 UTC