bot icon indicating copy to clipboard operation
bot copied to clipboard

Confusion between stdlib and stdlib-flambda when it fails

Open SkySkimmer opened this issue 10 months ago • 4 comments

https://github.com/coq/coq/pull/20215#issuecomment-2646324322

🏃 @coqbot ci minimize will minimize the following targets: ci-stdlib, ci-stdlib

SkySkimmer avatar Feb 09 '25 14:02 SkySkimmer

As far as I can tell https://github.com/coq/bot/blob/e838d62bd395390659d4aa4805841c163420eb54/src/actions.ml#L1007-L1012 seems fine ... I'm trying to find/recall where the library: / plugin: bits get chopped off

JasonGross avatar Feb 09 '25 14:02 JasonGross

The solution should be to just include + in https://github.com/coq/bot/blob/e838d62bd395390659d4aa4805841c163420eb54/src/actions.ml#L901

I don't have time to take care of & test this right now, unfortunately

JasonGross avatar Feb 09 '25 17:02 JasonGross

I don't think fixing this is as trivial as adding + to this regexp, because while the CI job is called ci-stdlib+flambda, the Makefile.ci target is ci-stdlib. So, we would need specific support for +flambda jobs (or +whatever jobs) for which we would be able to store a separate GitLab job name and Makefile.ci target.

Zimmi48 avatar Feb 10 '25 12:02 Zimmi48

After https://github.com/rocq-prover/bot/pull/336 I think we shouldn't be getting the ci target from the job name so maybe it is now trivial?

SkySkimmer avatar Apr 02 '25 13:04 SkySkimmer