I am working on the Coq 8.12.0 platform release. In the 8.12.0 Windows installer mathcomp is build with the usual configure / make / make install process. I wonder what opam packages this would correspond to. All matchcomp opam packages? Btw.: I think it makes sense to supply a meta opam package for mathcomp which includes all or the commonly used packages.

with the usual reservations that I'm not a MathComp dev, it seems quite clear that `make && make install`

basically corresponds to doing:

```
opam install coq-mathcomp-algebra coq-mathcomp-character \
coq-mathcomp-field coq-mathcomp-fingroup \
coq-mathcomp-solvable coq-mathcomp-ssreflect
```

However, the correspondence is not perfect, since there is a file `mathcomp/all/all.v`

(exporting all the content of all the packages) that to my knowledge is not installed by doing this in opam.

@Karl Palmskog : thanks! I am thinking about also including real-closed (contains the fundamental theorem of algrebra) and fingroup (also generally useful). Most of the other packages (except gigenough) anyway are not compatible with recent Coq.

fingroup is also included above, maybe you mean finmap? I would really like to see that one included

Ah sorry. I meant fingroup but I mixed up what is included in the "basic set". Indeed finmap also makes sense to include.

as I expressed elsewhere I also wish we could package mczify, so one would not have to jump through hoops to use `lia`

with MathComp: https://github.com/pi8027/mczify/tree/coq-8.12

I agree - I am also using mczify and don't know how to live without it.

See https://github.com/pi8027/mczify/issues/12

coq-mathcomp-finmap-1.5.0 works fine for me on 8.12.0

confirmed that mathcomp-analysis does *not* work on 8.12.0, neither for the latest release (0.3.1) nor for the `master`

branch

@Karl Palmskog Is there a log online that I can look at?

@Karl Palmskog Never mind. :-)

(By the way, we are planning to release 0.3.2 this week.)

@Karl Palmskog : the modules I have now are:

```
# The standard set of mathcomp modules
# Plus two generally useful eextensions and their dependency
opam pin coq-mathcomp-ssreflect 1.11.0
opam install \
coq-mathcomp-algebra \
coq-mathcomp-character \
coq-mathcomp-field \
coq-mathcomp-fingroup \
coq-mathcomp-solvable \
\
coq-mathcomp-real-closed \
coq-mathcomp-finmap \
coq-mathcomp-bigenough
```

Unless I made a mistake for all other modules opam says that they are incompatible with either Coq 8.12.0 or ssreflect 1.11.0.

I don't think you made a mistake, it looks like the opam files in finmap/real-closed say Coq < 8.12.

(as it is the case for mathcomp-analysis)

hmm, let me check if real-closed actually works with 8.12.0 (but yes, real-closed might be the culprit in the above)

I did succeed in compiling on my computer.

@Michael Soegtrop I tried the exact command you used above for the standard set of modules, and it works for me in a switch where I **only** have the `released`

Coq opam repo. Maybe you have also added `extra-dev`

in the switch where you tried the command? In that case, I can definitely see downgrades happening, due to not-yet-updated dev packages (which will be interpreted as *later* than the 1.11.0 packages).

@Karl Palmskog : maybe there is a missunderstanding. The commands I gave to work for me. I meant that all other modules of mathcomp don't build for me. But I currently have extra-dev in my repo list, although with lower prio than the usual coq repo.

ah, OK, so you mean: these are the only `coq-mathcomp-*`

packages that work out-of-the-box with Coq 8.12.0?

for example, I just tested locally that multinomials work with 8.12.0 + MC 1.11.0

an 8.12-compatible `coq-mathcomp-multinomials`

should be available now after `opam update`

.

Coming back to my original question: as mathcomp newbie I need some advice on what to include and what not. It is not only a question of what compiles now. It is mostly a question of what is widely used and what will be maintained long term. Of cause it does make sense to make it easy for users to compile additional packages in case they need them (by supplying opam packages).

I'd personally like to see at least everything up to and including mathcomp-analysis in the platform. Then from there, there are also some very useful library/framework projects that directly or indirectly use mathcomp-analysis or other MathComp projects:

- https://github.com/affeldt-aist/infotheo
- https://github.com/affeldt-aist/monae
- https://github.com/CoqEAL/CoqEAL
- https://github.com/coq-community/reglang

from what I've seen, infotheo and monae are actively maintained going forward, but @affeldt-aist can confirm. I am a co-maintainer of reglang, so I will at the minimum keep it working with recent Coq/MathComp.

I'll update infotheo and monae as soon as mathcomp-analysis is up-to-date, which should happen this week (with the proviso that monae depends on paramcoq which does not seen to be on opam yet).

@Pierre Roux is a release of ParamCoq for Coq 8.12.0 planned in the near future? We have quite a few packages depending on it, such as monae and CoqEAL.

OK. There is no need to hurry this. The main reason for having the Coq platform is to do such things properly. For the time beeing I will include the set I mentioned. Please create a ticket at coq-platform to include additional mathcomp packages (beyond the list I named).

affeldt-aist said:

(By the way, we are planning to release 0.3.2 this week.)

When is the release of the Coq plateform due?

I think the general target is 1-2 months after the Coq release

When is the release of the Coq plateform due?

A first preview (developer environment setup scripts only - no windows / macOS installers yet) will come this week. My plan for doing the first official release is end of August.

Done for paramcoq, sorry for the delay. Thanks @Karl Palmskog for pointing this (and for the quick merging, as usual)!

thanks, this means I will suggest Multinomials and CoqEAL for inclusion in the platform as well. Basically, even if they may still be considered experimental, CoqEAL is seemingly the only up-to-date machinery for data refinement at the pCUIC level (rather than for some deeply embedded language)

to me at least, going from `nat`

to `Z`

is a really basic thing to want to do

Last updated: Jul 15 2024 at 20:02 UTC