Le 30/01/2018 à 13:22, Stefan Berghofer a écrit :
Dear Why3-Club,
I just tried to compile Why3 with the latest OCaml 4.06.0 version, but this
failed due to
a missing Big_int module. I am aware that the Num library is now distributed
separately,
but since the webpage says that Num is outdated, I tried to install Zarith
instead and
also specified --enable-zarith when running the configure script for Why3.
Unfortunately,
compilation still failed with the same error message, because Big_int is still
used in
src/util/bigInt.ml. Would it be possible to adapt this file in such a way that
it uses
Big_int_Z instead of Big_int if Zarith is available (as it is done in
lib/ocaml/why3__BigInt.ml)?
I don't think so. If I remember correctly, the main issue is that using
Zarith in that file breaks the Why3 plugin for Coq. I am unfortunately
not savvy enough with the intricacies of dynamic linking in OCaml to
understand what is needed to make it work.
Best regards,
Guillaume
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
