Stream: math-comp devs

Topic: More packages in MathComp Docker?


view this post on Zulip 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: Jan 29 2023 at 15:02 UTC