Le 20/08/2018 à 21:59, Евгений Макаров a écrit :

Do I understand right that to use the opam version of Why3 with Coq I
need to install the why3-coq package? But this requires installing Coq
via opam in addition to the existing installation. So does this mean
that I have to install Coq and why3 either both via opam or both by
manually compiling from sources?

That is right.

That said, you don't have to compile all of Why3 at once. So, even if Why3's binaries have already been compiled and installed by opam, you can fetch Why3 sources and type the following to add support for Coq:

./configure --disable-why3-lib --disable-ide --prefix=`opam config var prefix`
make coq
make install-coq

Best regards,

Guillaume
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Reply via email to