Stream: math-comp users

Topic: ssreflect incompatible with analysis


view this post on Zulip Congyan (Cruise) Song (Nov 22 2023 at 23:12):

Hi, I am running into a compatibility issue when trying to upgrade the ssreflect into 2.0.0, and I wanna find out whether this is a issue specific to my machine.

Basically, when I pinned my coq to 8.16.1 and ssreflect to 2.0.0, opam automatically removed the 'mathcomp-analysis', which is required by my project. But when I tried to opam install analysis back , it showed me the following conflict.
Weixin-Image_20231122181048.jpg

view this post on Zulip Reynald Affeldt (Nov 22 2023 at 23:50):

We have not yet released a version of mathcomp-analysis compatible with mathcomp 2. There is however a compatible development branch that you can use in the meantime: https://github.com/math-comp/analysis/wiki#new-compatibility-of-mathcomp-analysis-with-mathcomp-2

view this post on Zulip Reynald Affeldt (Nov 23 2023 at 00:05):

Alternatively, if you do no rely crucially on features of mathcomp 2, you can use mathcomp 1.18 (where results of mathcomp 2 are backported) to be able to use mathcomp-analysis 0.6.6 (this month’s release).


Last updated: Jul 15 2024 at 20:02 UTC