Stream: jsCoq

Topic: Init.Notations and mathcomp


view this post on Zulip 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 jscoq options).

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (May 08 2022 at 11:56):

npm ls jscoq @jscoq/mathcomp

view this post on Zulip 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 jscoq and @jscoq/mathcomp are 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.

view this post on Zulip Shachar Itzhaky (May 08 2022 at 17:25):

oh for waCoq you need to install @wacoq/mathcomp.

view this post on Zulip 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: Jan 31 2023 at 10:01 UTC