Michael Soegtrop (Jul 26 2020 at 13:08): Michael Soegtrop (Jul 26 2020 at 13:08):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.
Karl Palmskog (Jul 26 2020 at 13:40):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.
Michael Soegtrop (Jul 26 2020 at 14:02):@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.
Karl Palmskog (Jul 26 2020 at 14:03):fingroup is also included above, maybe you mean finmap? I would really like to see that one included
Michael Soegtrop (Jul 26 2020 at 14:04):Ah sorry. I meant fingroup but I mixed up what is included in the "basic set". Indeed finmap also makes sense to include.
Karl Palmskog (Jul 26 2020 at 14:04):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
Michael Soegtrop (Jul 26 2020 at 14:06):I agree - I am also using mczify and don't know how to live without it.
Michael Soegtrop (Jul 26 2020 at 14:14):See https://github.com/pi8027/mczify/issues/12
Karl Palmskog (Jul 26 2020 at 14:54):coq-mathcomp-finmap-1.5.0 works fine for me on 8.12.0
Karl Palmskog (Jul 26 2020 at 15:08):confirmed that mathcomp-analysis does not work on 8.12.0, neither for the latest release (0.3.1) nor for the master branch
Reynald Affeldt (Jul 26 2020 at 16:06):@Karl Palmskog Is there a log online that I can look at?
Reynald Affeldt (Jul 26 2020 at 16:32):@Karl Palmskog Never mind. :-)
Reynald Affeldt (Jul 26 2020 at 17:00):(By the way, we are planning to release 0.3.2 this week.)
Michael Soegtrop (Jul 26 2020 at 17:47):@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.
Reynald Affeldt (Jul 26 2020 at 18:10):I don't think you made a mistake, it looks like the opam files in finmap/real-closed say Coq < 8.12.
Reynald Affeldt (Jul 26 2020 at 18:11):(as it is the case for mathcomp-analysis)
Karl Palmskog (Jul 26 2020 at 21:02):hmm, let me check if real-closed actually works with 8.12.0 (but yes, real-closed might be the culprit in the above)
Reynald Affeldt (Jul 26 2020 at 21:10):I did succeed in compiling on my computer.
Karl Palmskog (Jul 26 2020 at 21:17):@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).
Michael Soegtrop (Jul 26 2020 at 21:29):@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.
Karl Palmskog (Jul 26 2020 at 21:31):ah, OK, so you mean: these are the only coq-mathcomp-* packages that work out-of-the-box with Coq 8.12.0?
Karl Palmskog (Jul 26 2020 at 21:33):for example, I just tested locally that multinomials work with 8.12.0 + MC 1.11.0
Karl Palmskog (Jul 26 2020 at 22:25):an 8.12-compatible coq-mathcomp-multinomials should be available now after opam update.
Michael Soegtrop (Jul 27 2020 at 08:49):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).
Karl Palmskog (Jul 27 2020 at 08:54):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:
Karl Palmskog (Jul 27 2020 at 08:57):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.
Reynald Affeldt (Jul 27 2020 at 09:07):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).
Karl Palmskog (Jul 27 2020 at 12:11):@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.
Michael Soegtrop (Jul 27 2020 at 13:18):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).
Cyril Cohen (Jul 27 2020 at 17:29):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?
Karl Palmskog (Jul 28 2020 at 09:10):I think the general target is 1-2 months after the Coq release
Michael Soegtrop (Jul 29 2020 at 08:53):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.
Pierre Roux (Aug 17 2020 at 10:35):Done for paramcoq, sorry for the delay. Thanks @Karl Palmskog for pointing this (and for the quick merging, as usual)!
Karl Palmskog (Aug 17 2020 at 10:39):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)
Karl Palmskog (Aug 17 2020 at 10:40):to me at least, going from nat to Z is a really basic thing to want to do
Last updated: Feb 08 2023 at 04:04 UTC