Shachar Itzhaky (Apr 30 2021 at 16:57): 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?
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 :)
Emilio Jesús Gallego Arias (Apr 30 2021 at 17:59):Will fix ASAP, sorry for the trouble.
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.
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: Apr 20 2024 at 00:02 UTC