[Why3-club] zarith causes compilation error
Jean-Christophe.Filliatre at lri.fr
Mon Mar 24 16:58:30 CET 2014
> I recently had to install the zarith library for OCaml because it was
> required for
> compiling Alt-Ergo 0.95.2. After installing zarith, I tried to compile
> Why3 again,
> but it now failed with the strange error message
> ocamlopt.opt: don't know what to do with +zarith
> To fix the problem, I had to invoke configure with the
> --enable-zarith=no option.
> Is this a known problem, or have I done something wrong? I'm using OCaml
This was a bug. We haven't spotted it because we are all using zarith
installed from opam, and thus found via ocamlfind.
Commit 1ce26290c0e7cd fixes the issue. This is a one-line patch:
diff --git a/configure.in b/configure.in
index 6aef58c..cd16de1 100644
@@ -354,7 +354,7 @@ if test "$enable_zarith" = yes; then
AC_MSG_WARN([Lib Zarith not found, using Nums instead.])
reason_zarith=" (zarith not found)"
+ BIGINTINCLUDE="-I +zarith"
More information about the Why3-club