Raul (May 08 2022 at 10:34): Raul (May 08 2022 at 10:34):How can I import mathcomp without getting the Compiled library mathcomp.ssreflect.all_ssreflect (in file /lib/mathcomp/ssreflect/all_ssreflect.vo) makes inconsistent assumptions over library Coq.Init.Notations error?
I've the mathcomp package installed in /node_modules but it seems to override some Coq Notations.
My code is basically the same of npm-template but importing all_ssreflect from mathcomp (which is already added init_pkgs and all_pkgs wacoq options).
Shachar Itzhaky (May 08 2022 at 11:56):The notation overrides are standard, but ssreflect should load nevertheless. Are you using 0.15.0? Make sure both jscoq and @jscoq/mathcomp are the same version.
Shachar Itzhaky (May 08 2022 at 11:56):npm ls jscoq @jscoq/mathcomp
Raul (May 08 2022 at 12:25):Shachar Itzhaky said:
The notation overrides are standard, but ssreflect should load nevertheless. Are you using 0.15.0? Make sure both
jscoqand@jscoq/mathcompare the same version.
Yes, both are in 0.15.0.
Just checked again, and it only happens in wacoq, it isn't intended for mathcomp or packages?
Jscoq is completely fine.
Shachar Itzhaky (May 08 2022 at 17:25):oh for waCoq you need to install @wacoq/mathcomp.
Shachar Itzhaky (May 08 2022 at 17:25):Sry, the two are not binary-compat. We may want to change that but currently I am not sure how.
Last updated: Nov 29 2023 at 05:01 UTC