Stream: math-comp devs

Topic: Status of MathComp CI


view this post on Zulip Karl Palmskog (Jul 09 2023 at 15:04):

Should MathComp CI these days be viewed analogously to Coq's CI, i.e., as both a test suite and a way to have projects be updated/fixed as MathComp evolves? Is there a process for requesting a project to be included?

I ask because we may want to have specific support for this in Coq-community, e.g., a MathComp maintainer team that can merge overlays and so on, and tracking MathComp-using projects that are CI vs. not in CI.

view this post on Zulip Pierre Roux (Jul 09 2023 at 15:32):

We don't have any formalized process for inclusion. We tend to include whatever is in Nix / when people ask.

view this post on Zulip Karl Palmskog (Jul 09 2023 at 15:35):

OK, but if something is included, and it breaks, the overlay stuff might work similarly to Coq CI?

view this post on Zulip Pierre Roux (Jul 09 2023 at 15:36):

Compared to Coq CI I'd say the goal is more to check that we don't break too much than to write a lot of overlays. We have nothing similar to OCaml plugins and we try to go through deprecation phases as much as possible. In my experience the most overlay heavy PR are the one that remove these deprecations (after being deprecated for two versions).

view this post on Zulip Karl Palmskog (Jul 09 2023 at 15:37):

OK, it may be worth adding some small metadata and permissions in Coq-community then

view this post on Zulip Karl Palmskog (Jul 09 2023 at 15:38):

and I guess we can use the general rule of thumb that if a MathComp-dependent project joins Coq-community, we recommend it joins MC CI. An exception might be experimental/immature projects (e.g., https://github.com/coq-community/regexp-Brzozowski)


Last updated: May 18 2024 at 08:40 UTC