I just tried to compile the 0.5.2 opam package for Coq 8.16+rc1 and I get this error:
# File "./theories/functions.v", line 244, characters 48-61:
# Error: Record parameters must be named.
Thanks for reporting this. I was so focused on releasing a version compatible with mathcomp 1.15 that I forgot to check it for coq 8.16.
I thought we were missing coq-elpi (hence HB) anyway for Coq 8.16?
We are indeed (I can still test with dev version)... but you're right @Pierre Roux ...
@Michael Soegtrop how did you even reach the compilation of mathcomp-analysis in opam?
I am currently preparing a preview for Coq Platform 2022.09. For that I use "preview" opam packages for e.g. coq-elpi in a Coq Platform local opam patch repo. A preview version is similar to dev, but points to a specific commit which works for me.
You can have a look at: (https://github.com/MSoegtropIMC/platform/tree/prepare-2022.09.0-1/opam/opam-coq-archive) to see what is patched. The preview packages live in extra-dev. The packages in release are release version with Coq version restrictions relaxed but otherwise untouched. Currently I have PRs runnings to merge these upstream.
You can (hopefully - CI did not yet run on this branch) reproduce this by installing Coq Platform from this branch either full, or just base level and then opam install coq-mathcomp-analysis.
I have to do such hacks - otherwise making a Coq Platform release takes too long.
I want to release the preview in the next days and would like to include coq-mathcomp-analysis.
Working on it...
@Michael Soegtrop I managed to reproduce the error. The branch context-section
(PR math-comp/hierarchy-builder#295) happens to fix the bug (and it will be merged soon, and if not I can isolate the part of the PR that fixes it).
Cyril Cohen said:
Michael Soegtrop I managed to reproduce the error. The branch
context-section
(PR math-comp/hierarchy-builder#295) happens to fix the bug (and it will be merged soon, and if not I can isolate the part of the PR that fixes it).
Actually, it fixes this one and introduces a new one... so I will do a separate fix...
Thanks. I can easily point to a specific commit, so you can just give me the (full) commit hash. For a preview release this is just fine.
Last updated: Oct 13 2024 at 01:02 UTC