Stream: math-comp analysis

Topic: Issues with 0.5.2 and coq 8.16+rc1


view this post on Zulip Michael Soegtrop (Jul 12 2022 at 13:28):

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.

view this post on Zulip Cyril Cohen (Jul 12 2022 at 13:37):

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.

view this post on Zulip Pierre Roux (Jul 12 2022 at 13:38):

I thought we were missing coq-elpi (hence HB) anyway for Coq 8.16?

view this post on Zulip Cyril Cohen (Jul 12 2022 at 13:39):

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?

view this post on Zulip Michael Soegtrop (Jul 12 2022 at 13:48):

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.

view this post on Zulip Michael Soegtrop (Jul 12 2022 at 13:49):

I have to do such hacks - otherwise making a Coq Platform release takes too long.

view this post on Zulip Michael Soegtrop (Jul 12 2022 at 13:49):

I want to release the preview in the next days and would like to include coq-mathcomp-analysis.

view this post on Zulip Cyril Cohen (Jul 12 2022 at 13:50):

Working on it...

view this post on Zulip Cyril Cohen (Jul 12 2022 at 14:08):

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

view this post on Zulip Cyril Cohen (Jul 12 2022 at 14:13):

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

view this post on Zulip Michael Soegtrop (Jul 12 2022 at 14:15):

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: Feb 05 2023 at 14:02 UTC