Stream: jsCoq

Topic: math-comp for Coq 8.13


view this post on Zulip Shachar Itzhaky (Apr 30 2021 at 16:57):

Hi, trying to build our math-comp addon. Versions 1.11 and 1.12 seem to be incompatible with Coq 8.13. I do not see a tag for a later release; the master branch does seem to build, although @Emilio Jesús Gallego Arias's fast-load patch needs to be updated (or have you gotten it accepted upstream, finally). Anyone knows what the situation is?

view this post on Zulip Shachar Itzhaky (Apr 30 2021 at 17:25):

Correction: 1.12 does build with Coq 8.13; it is only the patch that is incompatible. The ball is yours @Emilio Jesús Gallego Arias :)

view this post on Zulip Emilio Jesús Gallego Arias (Apr 30 2021 at 17:59):

Will fix ASAP, sorry for the trouble.

view this post on Zulip Shachar Itzhaky (Apr 30 2021 at 20:11):

No trouble at all :) I think I figured out the problem, a new lemma count_subseqP in ssreflect.seq requires something that was removed by the patch.

view this post on Zulip Shachar Itzhaky (Apr 30 2021 at 20:28):

This ma new patch: https://github.com/jscoq/addon-mathcomp/blob/mathcomp-1.12.0/mathcomp-fast-load.patch
Notice that I had to also import Ring in ssrAC.v. Hope that's ok.


Last updated: Jan 30 2023 at 18:04 UTC