Karl Palmskog (Oct 15 2022 at 11:43): Karl Palmskog (Oct 15 2022 at 11:43):Before opening an issue, just wanted to check what the general sentiment is regarding additional packages in MathComp Docker images.
The current images only have the "core" MathComp packages: coq-mathcomp-ssreflect, coq-mathcomp-fingroup, coq-mathcomp-algebra, coq-mathcomp-solvable, coq-mathcomp-field, coq-mathcomp-character
Yet, according to the Coq Community Survey 2022 as seen here, there are quite a few MathComp packages that are more popular than solvable and character that are not among the core packages - for example, finmap, analysis, real-closed, mathcomp-zify.
Even if the main purpose of the Docker images is to enable testing of some of these projects, how about at least including the "utility" packages like mathcomp-zify and hierarchy builder? That would save a ton of CI time for many projects in Coq-community, for example. And via the Coq Platform releases, there is already a default choice of version.
Last updated: Dec 07 2023 at 09:01 UTC