Re: [Why3-club] undefined symbol

2018-02-11 Thread Julia Lawall
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

Re: [Why3-club] undefined symbol

2018-02-11 Thread Claude Marché
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 o

[Why3-club] undefined symbol

2018-02-11 Thread Julia Lawall
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