Congyan (Cruise) Song (Nov 22 2023 at 23:12): 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
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
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: Oct 13 2024 at 01:02 UTC