Closed aogrcs closed 6 years ago
Some more details are needed, I'm afraid:
opam
should have given you the end of the log, and the name of the log files, that contain information that sould help understanding the issue. Could you please post the content of said files here?Hi @vprevosto I tried to install Frama-c Chlorine. Last time I used: add-apt-repository ppa:avsm/ppa apt-get update apt-get install ocaml ocaml-native-compilers camlp4-extra opam to install opam and this time I just used pre-compiled binaries.
All the log as following:
opam pin add frama-c ~/Downloads/frama-c-Chlorine-20180502.tar.gz
[NOTE] Package frama-c is already path-pinned to /home/talos/Downloads/frama-c-Chlorine-20180502.tar.gz.
This will erase any previous custom definition.
Proceed ? [Y/n] y
[frama-c] /home/talos/Downloads/frama-c-Chlorine-20180502.tar.gz synchronized
frama-c needs to be installed.
The following actions will be performed:
∗ install frama-c 20180502*
Alt-Ergo Graphical Interface can be used by the WP plug-in
Yojson enables kernel option -json-compilation-database
Do you want to continue ? [Y/n] y
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[frama-c.20180502] /home/talos/Downloads/frama-c-Chlorine-20180502.tar.gz already up-to-date
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of frama-c failed at "make -j4".
Processing 1/1: [frama-c: rm]
#=== ERROR while installing frama-c.20180502 ==================================#
# opam-version 1.2.2
# os linux
# command make -j4
# path /home/talos/.opam/system/build/frama-c.20180502
# compiler system (4.02.3)
# exit-code 2
# env-file /home/talos/.opam/system/build/frama-c.20180502/frama-c-4829-d2d111.env
# stdout-file /home/talos/.opam/system/build/frama-c.20180502/frama-c-4829-d2d111.out
# stderr-file /home/talos/.opam/system/build/frama-c.20180502/frama-c-4829-d2d111.err
### stdout ###
# [...]
# Coqc src/plugins/wp/share/why3/Cmath.vo
# Coqc src/plugins/wp/share/why3/Square.vo
# Coqc src/plugins/wp/share/why3/ExpLog.vo
# Coqc src/plugins/wp/share/why3/Vset.vo
# Coqc src/plugins/wp/share/coqwp/BuiltIn.v
# Generation of the extra-config for why3
# Ocamlc src/kernel_internals/runtime/frama_c_init.cmi
# Ocamlc src/libraries/stdlib/transitioning.cmo
# Ocamlc src/libraries/stdlib/FCSet.cmo
# share/Makefile.generic:77: recipe for target 'src/libraries/stdlib/transitioning.cmo' failed
### stderr ###
# 4 shift/reduce conflicts.
# 7 shift/reduce conflicts.
# File "src/libraries/stdlib/transitioning.ml", line 82, characters 15-24:
# Error: Unbound value Z.numbits
# Hint: Did you mean to_bits or of_bits?
# make: *** [src/libraries/stdlib/transitioning.cmo] Error 2
# make: *** Waiting for unfinished jobs....
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
∗ install frama-c 20180502
No changes have been performed
[NOTE] Pinning command successful, but your installed packages may be out of sync.
Maybe it caused by zarith, see this issue: https://bts.frama-c.com/view.php?id=2391#bugnotes But I do not find how to resolve it.
Do you tried opam install frama-c.20180502
(or just opam install frama-c
since it is the last version)? Before you should remove the pinned version opam pin remove frama-c
.
What is the current version of zarith you are using (opam show zarith
or opam list zarith
)?
I did not try neither of these, and I delete the images, but I will try later and post it as soon as possible. Thanks
Hi, I tried it again, and the zarith version is 1.7 installed by opam 1.2.2. I installed opam by add repository not binary this time. I did this time. I thought next time I should directly use opam install frama-c and this would save a lot of time. Thanks! Sincerely
Hi I have saw this error when used opam pin add --kind=path frama-c