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:

- Put 8.18+MC1.18 at the top and 8.18+MC2.1 right behind it - before the original pick for 8.17
- Put 8.18+MC1.18 at the top and 8.18+MC2.1 after all original picks and at the top of the list of compatibility picks (rank 10 or so)
- Either of the above with MC2.1 and MC1.18 swapped

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

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.

I don't think this is the case.

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.

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

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.

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 ...

`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