Hi,
First of all, the error is in the installation of Why3 and not Why, and second the problem is not that files are missing but that coqc segfaults:
> # /bin/sh: line 1: 63283 Segmentation fault: 11 WHY3CONFIG="" coqc -opt -I lib/coq-tactic/ lib/coq-tactic/Why3.v
I have no idea why it happens, I forward your mail to the Why3 list, hoping someone's has an idea.
You may also try to install a more recent version of Why3 to see if it has the same problem: opam install why3
- Claude Le 02/10/2014 03:53, Jackie Wang a écrit :
Hi, I tried 'opam install why' but got the following error. All dependent packages are installed, and the errors seem to complain about missing files but they actually exist in the 'build' directory. Please advise! Thanks. Jackie ==== jackie$ opam install why The following actions will be performed: - install why3.0.83 [required by why] - install why.2.34 2 to install | 0 to reinstall | 0 to upgrade | 0 to downgrade | 0 to remove Do you want to continue ? [Y/n] Y =-=-= Installing why3.0.83 =-=-= Building why3.0.83: ./configure --prefix /Users/jackie/.opam/3.12.1 --sbindir=/Users/jackie/.opam/3.12.1/lib/why3/sbin --libexecdir=/Users/jackie/.opam/3.12.1/lib/why3/libexec --sysconfdir=/Users/jackie/.opam/3.12.1/lib/why3/etc --sharedstatedir=/Users/jackie/.opam/3.12.1/lib/why3/com --localstatedir=/Users/jackie/.opam/3.12.1/lib/why3/var --libdir=/Users/jackie/.opam/3.12.1/lib/why3/lib --includedir=/Users/jackie/.opam/3.12.1/lib/why3/include --datarootdir=/Users/jackie/.opam/3.12.1/lib/why3/share --disable-bench make opt byte make install install-lib [ERROR] The compilation of why3.0.83 failed. Removing why3.0.83. [ERROR] Due to some errors while processing why3.0.83, the following actions will NOT proceed: - install why.2.34 ===== ERROR while installing why3.0.83 ===== # opam-version 1.1.1 # os darwin # command make opt byte # path /Users/jackie/.opam/3.12.1/build/why3.0.83 # compiler 3.12.1 # exit-code 2 # env-file /Users/jackie/.opam/3.12.1/build/why3.0.83/why3-61617-5f1023.env # stdout-file /Users/jackie/.opam/3.12.1/build/why3.0.83/why3-61617-5f1023.out # stderr-file /Users/jackie/.opam/3.12.1/build/why3.0.83/why3-61617-5f1023.err ### stdout ### # ...[truncated] # Ocamlopt src/why3session/why3session_run.ml # Ocamlopt src/why3session/why3session_csv.ml # Ocamlopt src/why3session/why3session.ml # Linking bin/why3session.opt # Ocamlc src/coq-tactic/coqCompat.mli # Ocamlopt src/coq-tactic/coqCompat.ml # Ocamlopt src/coq-tactic/why3tac.ml # Ocamlopt src/coq-tactic/g_why3tac.ml # Linking lib/coq-tactic/why3tac.cmxs # Coqc lib/coq-tactic/Why3.v ### stderr ### # ...[truncated] # Makefile:952: lib/coq/option/Option.vd: No such file or directory # Makefile:1215: lib/ocaml/why3__BigInt.dep: No such file or directory # Makefile:1215: lib/ocaml/why3__IntAux.dep: No such file or directory # Makefile:1215: lib/ocaml/why3__Array.dep: No such file or directory # Makefile:1340: src/why3doc/doc_html.dep: No such file or directory # Makefile:1340: src/why3doc/doc_def.dep: No such file or directory # Makefile:1340: src/why3doc/doc_lexer.dep: No such file or directory # Makefile:1340: src/why3doc/doc_main.dep: No such file or directory # /bin/sh: line 1: 63283 Segmentation fault: 11 WHY3CONFIG="" coqc -opt -I lib/coq-tactic/ lib/coq-tactic/Why3.v # make: *** [src/coq-tactic/.why3-vo-opt] Error 139 'opam install why' failed.
-- Claude Marché | tel: +33 1 72 92 59 69 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/cgi-bin/mailman/listinfo/why3-club
