Stream: math-comp users

Topic: Package pick ordering in Coq Platform


view this post on Zulip Michael Soegtrop (Nov 15 2023 at 10:19):

As discussed I will include two 8.18 picks in the upcoming Coq Platform release - one with MC 1.18 and one with MC 2.1. The latter misses mathcomp-analysis, mathcomp-classical and mathcomp-word. I wonder in which order I should present the picks - which depends on what you expect users to use mostly. I will include binary installers for both - what we discuss here is the position in the pick list presented when installing using the scripts.

The options are:

view this post on Zulip Karl Palmskog (Nov 15 2023 at 10:21):

since 8.18+MC2.1 is lacking packages, might make sense to not have it as the first choice

view this post on Zulip Michael Soegtrop (Nov 15 2023 at 10:23):

Karl Palmskog said:

since 8.18+MC2.1 is lacking packages, might make sense to not have it as the first choice

Yes, this matches my thinking, unless the assumption of the MC community is that close to nobody will use 1.18.

view this post on Zulip Reynald Affeldt (Nov 15 2023 at 10:23):

I don't think this is the case.

view this post on Zulip Michael Soegtrop (Nov 15 2023 at 10:27):

OK, so 1.18 goes on the top. Then the question remains if 8.18+MC2 follows at position 2 or behind all original picks.

I would say if the expected user base of MC2 is say > 30%, I would put it on position 2, otherwise after the original picks.

view this post on Zulip Pierre Roux (Nov 15 2023 at 10:37):

Position 2 sounds good, except Analysis and word\Jasmin, all major devs seem to be ported now.

view this post on Zulip Karl Palmskog (Nov 15 2023 at 10:39):

for example, there is a small MC-based ecosystem around FCSL that is still on 1.18 until some universe issues can be solved for MC2.

view this post on Zulip Michael Soegtrop (Nov 15 2023 at 11:02):

Live is difficult - there are three packages which don't support the combination of Coq 8.18.0 and MC 1.18 (coq-reglang, coq-deriving and coq-extructures) let's see if I can relax the restrictions ...

view this post on Zulip Karl Palmskog (Nov 15 2023 at 11:04):

coq-reglang.1.1.3 supports Coq 8.18.0 and MC 1.18 just fine: https://github.com/coq/opam/blob/master/released/packages/coq-reglang/coq-reglang.1.1.3/opam


Last updated: Jul 25 2024 at 16:02 UTC