-
Notifications
You must be signed in to change notification settings - Fork 667
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Split github CI actions into 2 workflows + disable windows while it's broken #15535
Conversation
To be able to rerun one OS without rerunning the other.
6b045f1
to
9a97a14
Compare
Another way of disabling the Windows workflow would have been to call it |
BTW, the reason why the Windows CI fails seems to be simply because the |
9a97a14
to
36055a3
Compare
Still not working (different error though) |
FWIW, the first error is the following one:
The call is done in: coq/dev/ci/platform/coq-pf-03-build.bat Lines 14 to 24 in 24a705b
@MSoegtropIMC The Windows CI is failing for Coq because the |
36055a3
to
15db345
Compare
Will merge after confirming that macOS CI passes. |
@Zimmi48 : OK, I cleaned up a bit too much. What would you recommend? I don't think I still want the dev-ci branch since it is effort to maintain it. I now have a working dev pick, but it points to master for all packages. I guess it would make sense to create a "ci" pick which honors the -override-dev-pkg option and/or possibly also takes the overlay information for -extent=f and -extent=x. @gares started something like this in coq/platform#44. |
@coqbot merge now |
@MSoegtropIMC Indeed, I agree that reintroducing the |
OK, I will add a ci pick which at first only contains coq + coqide (f and x extents will be empty) and which honors the -override-dev-pkg flag. In addition I would mid term like to have a pick which mimics Coq's CI. Any suggestions how these two picks should be named? |
"dev"? |
There is already a "dev" pick which uses the dev opam packages (that is default branch) for all packages. In addition I propose to have two picks:
For package maintainers the latter might be more useful than the dev pick. The dev pick is mostly for me to know where issues are. Maybe dev (opam .dev) |
Sounds good to me. |
Looks like I'm backporting this since it's also broken for 8.15 |
…able windows while it's broken
To be able to rerun one OS without rerunning the other.