Karl Palmskog (Jul 09 2023 at 15:04): 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.
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.
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?
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).
Karl Palmskog (Jul 09 2023 at 15:37):OK, it may be worth adding some small metadata and permissions in Coq-community then
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: Sep 09 2024 at 04:02 UTC