Stream: Coq devs & plugin devs

Topic: [CI] Remove library-undecidability


view this post on Zulip Andrej Dudenhefner (Oct 08 2024 at 07:31):

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

view this post on Zulip Pierre Roux (Oct 08 2024 at 08:27):

I guess so

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2024 at 08:30):

Personally I'd support full reintegration, but there has been some discussion recently about what we want in the CI.

view this post on Zulip Michael Soegtrop (Oct 08 2024 at 08:50):

@Emilio Jesús Gallego Arias : is the issue more server cost to run CI or manual labor to get things fixed?

view this post on Zulip Yannick Forster (Oct 08 2024 at 08:51):

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)

view this post on Zulip Pierre Roux (Oct 08 2024 at 08:57):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2024 at 10:33):

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.

view this post on Zulip Michael Soegtrop (Oct 08 2024 at 12:15):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 08 2024 at 13:53):

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)

view this post on Zulip Gaëtan Gilbert (Oct 08 2024 at 13:55):

servers seem plentiful since we got some from google

view this post on Zulip Yannick Forster (Oct 08 2024 at 14:55):

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?

view this post on Zulip Pierre Roux (Oct 08 2024 at 15:15):

Many repos are successfully using the coq-nix-toolbox: https://github.com/coq-community/coq-nix-toolbox but I may be biased

view this post on Zulip Yannick Forster (Oct 09 2024 at 15:06):

MetaCoq is not one of these repos -- not for a lack of trying :)

view this post on Zulip Pierre Roux (Oct 09 2024 at 15:07):

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.

view this post on Zulip Pierre Roux (Oct 09 2024 at 15:08):

What did you try / what was the issue?

view this post on Zulip Matthieu Sozeau (Oct 09 2024 at 17:39):

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

view this post on Zulip Pierre Roux (Oct 09 2024 at 19:02):

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

view this post on Zulip Kenji Maillard (Oct 09 2024 at 19:44):

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.

view this post on Zulip Pierre Roux (Oct 10 2024 at 07:45):

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.

view this post on Zulip Gaëtan Gilbert (Oct 10 2024 at 08:18):

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

view this post on Zulip Pierre Roux (Oct 10 2024 at 08:26):

Yes, CI policy still needs some work.

view this post on Zulip Pierre Roux (Oct 10 2024 at 08:26):

But considering how much discussion each detail requires, I prefer to improve it step by step.

view this post on Zulip Théo Zimmermann (Oct 11 2024 at 14:25):

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.

view this post on Zulip Théo Zimmermann (Oct 11 2024 at 14:26):

Would MetaCoq developers welcome a PR adding a Coq Nix Toolbox-based RDCT CI setup?

view this post on Zulip Théo Zimmermann (Oct 11 2024 at 14:34):

We will also need to do work to package the reverse dependencies that need to be tested, of course.

view this post on Zulip Théo Zimmermann (Oct 11 2024 at 14:35):

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