search

mattam82 / Coq-Equations

A function definition package for Coq
http://mattam82.github.io/Coq-Equations
GNU Lesser General Public License v2.1
223 stars 44 forks source link

Incompatibility with MathComp due to notation levels. #21

Closed chdoc closed 6 years ago

chdoc commented 6 years ago

When trying to load mathcomp.ssreflect.ssrfun after Equations.Equations, I get the following error:

Error: Notation _ .1 is already defined at level 3 with arguments at next level while it is now required to be at level 2 with arguments at level 2.

Loading the libraries in reverse order of course yields the reverse error message. As far as I am concerned, this makes the package incompatible with MathComp. I suppose it's unlikely that MathComp is going to change this, so I hope it can be changed in Equations. There are likely further clashes, at the very least "_.2".

mattam82 commented 6 years ago

Indeed, there might be other issues, I'll have a look. Have you tried only [Require Equations] instead of an Import?

chdoc commented 6 years ago

OK, if I use [Require Equations] the library can be loaded. Haven't had the time yet to check for usability issues arising from this (or do anything really). Equations.Equations tries to export quite a bit.

mattam82 commented 6 years ago

Yes, the issue is we need typeclass instances defined in Equations .v files to process some definitions. I guess the best we could do for now is separate those instances. Clearly the notations defined for sigma etc... should not interfere with the user developments.

lastland commented 6 years ago

It looks like there are also some compatibility issues with VST.

To be specific, the following code:

Require Import VST.floyd.proofauto.
Require Import Equations.Equations.

gives me the following error information:

Error: Notation ` _ is already defined at level 9 with arguments at next level
while it is now required to be at level 10 with arguments at next level.

And, of course,Require Equations.Equations would work.

mattam82 commented 6 years ago

This is now fixed in the master branch (for 8.6) and the 8.7 branch. There are upcoming opam packages for these two versions (8.6.dev and 8.7.dev respectively in the extra-dev repo). I'll make a second beta version this week as well, integrating these fixes. Note I couldn't test with vst yet, whose installation looks fairly complicated but mathcomp and extlib can be loaded together alongside Equations with no conflicts now (Equations doesn't export any notation by default).

mattam82 commented 6 years ago

The packages are here now. I'll make a second beta release.