On Mon, 12 Feb 2018, Claude Marché wrote:
>
> 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
This works, thanks. The strange thing is that I don't find the variable
that it was complaining about anywhere in the source code, except in a
file where it is defined.
julia
>
> 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
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
