mht208 / homebrew-formal

Homebrew formulae for formal methods
37 stars 10 forks source link

OCaml incompatibility with why3 install #15

Open BenHocking opened 8 years ago

BenHocking commented 8 years ago

In trying to install mht208/formal/why3, I got the following message:

Last 15 lines from /Users/benjaminhocking/Library/Logs/Homebrew/why3/02.make:
echo "(* generated automatically at compilation time *)" > drivers/pvs-realizations.aux
Ocamlopt src/tools/why3wc.ml
echo "(* generated automatically at compilation time *)" > drivers/isabelle-realizations.aux
clang -Wall -o lib/why3-cpulimit src/tools/cpulimit.c
Ocamlopt lib/ocaml/why3__BigInt_compat.ml
Ocamlc   src/why3doc/doc_html.mli
Ocamlopt src/util/bigInt.ml
Ocamlopt src/util/util.ml
Ocamlopt src/util/opt.ml
File "lib/ocaml/why3__BigInt_compat.ml", line 1:
Error: /usr/local/lib/ocaml/zarith/big_int_Z.cmi
is not a compiled interface for this version of OCaml.
It seems to be for an older version of OCaml.
make: *** [lib/ocaml/why3__BigInt_compat.cmx] Error 2
make: *** Waiting for unfinished jobs....

I have OCaml 4.03.0:

▶ ocaml --version
The OCaml toplevel, version 4.03.0

OCaml was installed with homebrew. I have the following OCaml related packages installed: mht208/formal/ocaml-findlib ✔ mht208/formal/ocamlgraph ✔ ocaml ✔ ocamlbuild ✔

brew doctor did not reveal anything other than the SHA1 messages that another bug report has already mentioned.

Here is the gist log.