Re: [Why3-club] Compiling Why3 with OCaml 4.06.0

2018-01-30 Thread Claude Marché
Le 30/01/2018 à 16:47, Guillaume Melquiond a écrit : >> 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

Re: [Why3-club] Compiling Why3 with OCaml 4.06.0

2018-01-30 Thread Guillaume Melquiond
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,

Re: [Why3-club] Compiling Why3 with OCaml 4.06.0

2018-01-30 Thread Gabriel Scherer
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