Hello, I don't know why it does fail, but a possible workaround is to disable the compilation of the Coq tactic, which is not essential at all.
./configure --disable-coq-tactic make Another suggestion is to compile and install ocaml, coq, why3 via opam. You will get a much more recent version of OCaml and the build process is simpler. Hope this helps, - Claude Le 11/02/2018 à 18:25, Julia Lawall a écrit : > Hello, > > I am trying to compile why3 on Ubuntu 16.04 with ocaml 4.02.3. I get the > error: > > File "./lib/coq-tactic/Why3.v", line 14, characters 0-28: > Error: > while loading /home/jll/why3-0.88.3/lib/coq-tactic/why3tac.cmxs: > error loading shared library: > /home/jll/why3-0.88.3/lib/coq-tactic/why3tac.cmxs: undefined symbol: > camlLtac_plugin__Taccoerce__coerce_to_int_4757 > > The output of configure (fl) and of make (fl1) are attached. > > thanks, > julia > > > > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
