Your change proposal sounds very reasonable, but note that, as a workaround, it is easy to compile and install the "num" module (if you use Opam, "opam install num" should do). If Why3's compilation README/documentation was not updated to indicate the Num module is an external dependency, it would be a change to make as well.
On Tue, Jan 30, 2018 at 1:22 PM, Stefan Berghofer <bergh...@in.tum.de> wrote: > 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)? > > Greetings, > Stefan > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
