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.
We don't have any formalized process for inclusion. We tend to include whatever is in Nix / when people ask.
OK, but if something is included, and it breaks, the overlay stuff might work similarly to Coq CI?
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).
OK, it may be worth adding some small metadata and permissions in Coq-community then
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: Nov 29 2023 at 21:01 UTC