Hello, My guess is that you have an old version of Coq that was installed in OPAM and was not cleaned properly.
You should browse /home/pablo/.opam/4.02.1/lib/coq/ and manually remove all files that seem obviously older than the ones installed with the last version of Coq. Alternatively, you may consider start a fresh installation with a newer version of OCaml : opam switch 4.02.3 opam install conf-gmp conf-gtksourceview why3 (compilation of Coq will take some time, sorry about that) - Claude Le 02/03/2016 14:40, Pablo M. S. Farias a écrit : > Dear Claude Marché, > > I've tried to install Why3 through OPAM and got this error: > > ------------------------------------------------------------ > pablo@comp-rafaella:~$ opam install why3.0.86.3 > The following actions will be performed: > ∗ install why3-base 0.86.3 [required by why3] > ∗ install why3 0.86.3 > ===== ∗ 2 ===== > Do you want to continue ? [Y/n] Y > > =-=- Gathering sources > =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= > [why3-base] Archive in cache > > =-=- Processing actions > -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= > [ERROR] The compilation of why3-base failed at "make opt byte". > > #=== ERROR while installing why3-base.0.86.3 > ==================================# > # opam-version 1.2.2 > # os linux > # command make opt byte > # path /home/pablo/.opam/4.02.1/build/why3-base.0.86.3 > # compiler 4.02.1 > # exit-code 2 > # env-file > /home/pablo/.opam/4.02.1/build/why3-base.0.86.3/why3-base-2506-58c514.env > # stdout-file > /home/pablo/.opam/4.02.1/build/why3-base.0.86.3/why3-base-2506-58c514.out > # stderr-file > /home/pablo/.opam/4.02.1/build/why3-base.0.86.3/why3-base-2506-58c514.err > ### stdout ### > # [...] > # Ocamlopt src/why3session/why3session_latex.ml > # Ocamlopt src/why3session/why3session_html.ml > # Ocamlopt src/why3session/why3session_rm.ml > # Ocamlopt src/why3session/why3session_output.ml > # Ocamlopt src/why3session/why3session_run.ml > # Ocamlopt src/why3session/why3session_csv.ml > # Ocamlopt src/why3session/why3session_main.ml > # Linking bin/why3session.opt > # Coqc lib/coq/BuiltIn.v > # Ocamlopt src/coq-tactic/why3tac.ml > ### stderr ### > # [...] > # File "src/session/session.ml", line 1546, characters 16-27: > # Warning 3: deprecated: String.copy > # File "src/why3session/why3session_lib.ml", line 252, characters 10-23: > # Warning 3: deprecated: String.create > # Use Bytes.create instead. > # File "src/coq-tactic/why3tac.ml4", line 1: > # Error: The files /home/pablo/.opam/4.02.1/lib/coq/proofs/tacmach.cmi > # and /home/pablo/.opam/4.02.1/lib/coq/intf/tacexpr.cmi > # make inconsistent assumptions over interface Tacexpr > # make: ** [src/coq-tactic/why3tac.cmx] Erro 2 > > > > =-=- Error report > -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= > The following actions were aborted > ∗ install why3 0.86.3 > The following actions failed > ∗ install why3-base 0.86.3 > No changes have been performed > ------------------------------------------------------------ > > I have Coq 8.4.6 installed (I would be glad to upgrade to 8.5, but > cannot do it because the Verified Software Toolchain 1.6, which I'm > studying, specifically demands Coq 8.4pl6): > > ------------------------------------------------------------ > pablo@comp-rafaella:~$ opam show coqide > package: coqide > version: 8.4.6 > repository: default > upstream-url: > https://coq.inria.fr/distrib/V8.4pl6/files/coq-8.4pl6.tar.gz > upstream-kind: http > upstream-checksum: 2334a98b64578cb81d2b4127e327b368 > depends: camlp5 & coq = 8.4.6 & lablgtk >= 2.12.0 & ocamlbuild > installed-version: 8.4.6 [4.02.1] > available-versions: 8.4pl2, 8.4pl4, 8.4.5, 8.4.6, 8.5.0 > description: IDE of the coq formal proof management system > ------------------------------------------------------------ > > Presently I have no urgent need for Why3, but I'll be experimenting with > Frama-C soon, so please let me know in case you know solutions to the > above, ok? > > Thanks in advance, > -- 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 http://lists.gforge.inria.fr/mailman/listinfo/why3-club
