[Why3-club] zarith causes compilation error

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Mon Mar 24 16:58:30 CET 2014


Dear Stefan

> 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
> 4.01.0.

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
--- a/configure.in
+++ b/configure.in
@@ -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)"
       else
-         BIGINTINCLUDE="+zarith"
+         BIGINTINCLUDE="-I +zarith"
       fi
    fi
 fi

-- 
Jean-Christophe



More information about the Why3-club mailing list