PR https://github.com/coq/coq/pull/19339 removed ci-coq_library_undecidability
from Coq CI.
Shorty after that there were overlooked regressions which broke said project.
The reason given in the PR is
This depends from metacoq and it appears it is not tested in metacoq CI, which means any change in metacoq could subrepticly break the CI here.
Would it be correct to assume that if ci-coq_library_undecidability
removed all dependencies (besides Coq itself), then it could be reintegrated into Coq CI? Or are there other reasons hindering reintegration?
In the past this library helped catch some Coq regressions and several other projects depend on this library.
@Pierre Roux
I guess so
Personally I'd support full reintegration, but there has been some discussion recently about what we want in the CI.
@Emilio Jesús Gallego Arias : is the issue more server cost to run CI or manual labor to get things fixed?
The initial discussion about removing the library was about this being a pure library, not having any OCaml code. I think that's a fine rule, but I have no strong opinions. But if that's not a rule, I don't think the reliance on MetaCoq should be a blocker to be in the CI. If anything, this allows catching regressions where changing something in Coq affects behaviour of MetaCoq. (and the worry that changes in MetaCoq break the CI via the undecidability library is theoretical I think, at least I'm not aware that this has ever happened)
Anything with dependencies should definitely be tested in each dependencies' CI, otherwise it canbreak to easily. We are again seeing it recently with itree -> paco.
Michael Soegtrop said:
Emilio Jesús Gallego Arias : is the issue more server cost to run CI or manual labor to get things fixed?
IIRC both points where made. I still like the model where breakage of compat (specially if unintended) has a exponential cost factor, so IMHO server costs are nothing compared to human cost.
Managing compatibility IMHO doesn't mean that we need to remain compatible. The CI is about (or was, as originally conceived) _detecting_ breakage, not about _avoiding_ it.
In case server cost is a severe issue, one workable model would be to have a 3rd level of CI (besides the current partial and full CI). The 3rd level CI one runs only say every other day (time based). One can then move packages between the full and 3rd level CI based on how much interesting (not found by other packages) breakage they find.
IMHO human cost is way higher than any server cost (you can buy a state-of-the art server that can do the CI like a cake for less than an engineer costs for 2 months)
servers seem plentiful since we got some from google
Pierre Roux said:
Anything with dependencies should definitely be tested in each dependencies' CI, otherwise it canbreak to easily. We are again seeing it recently with itree -> paco.
Is there a workable "forward" CI solution by now?
Many repos are successfully using the coq-nix-toolbox: https://github.com/coq-community/coq-nix-toolbox but I may be biased
MetaCoq is not one of these repos -- not for a lack of trying :)
Metacoq is in nixpkgs and I managed to get it effortless working (from the Nix side) in the Stdlib test repo so it definitely seems feasible.
What did you try / what was the issue?
As we are no experts on this, the first time our nix CI broke we didn't manage to fix it... That was already a year ago I think. @Kenji Maillard might have a good recollection of it
Note that we have a zulip stream to help in such cases https://coq.zulipchat.com/#narrow/stream/290990-Nix-and-Coq-Nix-Toolbox-devs-.26-users
I never managed to get a fully working nix derivation for metacoq after spending too much time, and nobody have been actively using the nix CI for metacoq (e.g. the caching features), so it was purely duplicating the CI for no good reason.
Well, the derivation that you created in nixpkgs https://github.com/NixOS/nixpkgs/tree/master/pkgs/development/coq-modules still works well, so seems rather successfull to me. But indeed, if you were not doing any reverse dependency checking, I understand there was not much gain in it. Note however that getting reverse dependency checking is exactly what the current discussion is all about.
BTW our current CI doc (https://github.com/coq/coq/blob/master/dev/ci/README-users.md) doesn't say anything about doing reverse dep testing for projects whose dependents are in our CI
in fact we don't even require having CI, just recommend it
You do not push, to the branch that we test, commits that haven't been
first tested to compile with the corresponding branch of Coq.For that, we recommend setting a CI system for you project, see for instance
supported CI images for Coq below.
Yes, CI policy still needs some work.
But considering how much discussion each detail requires, I prefer to improve it step by step.
I think it was probably a mistake to remove the library for this reason (especially given that the breakage was purely theoretical), but I also consider that we should expand our CI policy to mandate RDCT (reverse dependency compatibility testing) and work with users such as MetaCoq to make sure that we provide a well-supported solution to do this.
Would MetaCoq developers welcome a PR adding a Coq Nix Toolbox-based RDCT CI setup?
We will also need to do work to package the reverse dependencies that need to be tested, of course.
But given that we are also planning to move to a Nix-based RDCT CI for the split stdlib repo, this work will be done once for both CI.
Last updated: Oct 13 2024 at 01:02 UTC