Frama-C Bug Tracking System - Frama-C
View Issue Details
0002399Frama-COpampublic2018-09-11 17:502018-11-30 10:07
hugo.gimbert 
maroneze 
normalmajoralways
closedfixed 
ApplemacosxHighSierra 10.3.
Frama-C 17-Chlorine 
Frama-C 18-ArgonFrama-C 18-Argon 
0002399: Failed to install framaC on macosx using opam
Followed step by step the install procedure on http://frama-c.com/install-chlorine-20180501.html#installing-frama-c-on-macos Failed at the last step, because compilation of alt-ergo 1.30 fails with following message hugo-3:~ gimbert$ opam install frama-c The following actions will be performed: ∗ install alt-ergo 1.30 [required by frama-c] ∗ install frama-c 20180502 Alt-Ergo Graphical Interface can be used by the WP plug-in Yojson enables kernel option -json-compilation-database ===== ∗ 2 ===== Do you want to continue ? [Y/n] Y =-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫 [alt-ergo] Archive in cache [frama-c] Archive in cache =-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫 [ERROR] The compilation of alt-ergo failed at "make". Processing 1/2: [alt-ergo: rm] #=== ERROR while installing alt-ergo.1.30 =====================================# # opam-version 1.2.2 # os darwin # command make # path /Users/gimbert/.opam/system/build/alt-ergo.1.30 # compiler system (4.07.0) # exit-code 2 # env-file /Users/gimbert/.opam/system/build/alt-ergo.1.30/alt-ergo-78161-c61e7b.env # stdout-file /Users/gimbert/.opam/system/build/alt-ergo.1.30/alt-ergo-78161-c61e7b.out # stderr-file /Users/gimbert/.opam/system/build/alt-ergo.1.30/alt-ergo-78161-c61e7b.err ### stdout ### # [...] # ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myDynlink.mli # ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myDynlink.ml # ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myZip.mli # ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myZip.ml # ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/util.mli # ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/util.ml # ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/lists.mli # ocamlopt.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/lists.ml # ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/numbersInterface.mli # ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -I /Users/gimbert/.opam/system/lib/zarith -I /Users/gimbert/.opam/system/lib/lablgtk2 -I +threads -I /Users/gimbert/.opam/system/lib/camlzip/../zip -I /Users/gimbert/.opam/system/lib/ocplib-simplex -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/numsNumbers.mli ### stderr ### # Makefile.users:264: .depend: No such file or directory # File "/Users/gimbert/.opam/system/build/alt-ergo.1.30/src/util/numsNumbers.mli", line 24, characters 47-62: # Error: Unbound module Big_int # make: *** [src/util/numsNumbers.cmi] Error 2 =-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫 The following actions were aborted ∗ install frama-c 20180502 The following actions failed ∗ install alt-ergo 1.30 No changes have been performed
No tags attached.
Issue History
2018-09-11 17:50hugo.gimbertNew Issue
2018-09-11 17:50hugo.gimbertStatusnew => assigned
2018-09-11 17:50hugo.gimbertAssigned To => maroneze
2018-09-11 19:16maronezeNote Added: 0006643
2018-09-11 22:10hugo.gimbertNote Added: 0006644
2018-09-12 15:34maronezeNote Added: 0006645
2018-09-14 09:57signolesTarget Version => Frama-C 18-Argon
2018-10-29 15:13maronezeNote Added: 0006671
2018-10-29 15:13maronezeStatusassigned => resolved
2018-10-29 15:13maronezeFixed in Version => Frama-C 18-Argon
2018-10-29 15:13maronezeResolutionopen => fixed
2018-11-30 10:07signolesStatusresolved => closed

Notes
(0006643)
maroneze   
2018-09-11 19:16   
Thanks for the report. It seems that altgr-ergo is no longer being released, so installing alt-ergo directly should give better results, since there are newer versions of it available. I recommend trying `opam remove altgr-ergo`, then `opam install alt-ergo.2.2.0` (or the latest release currently available), then `opam install frama-c`. On Linux, alt-ergo 1.30 does compile with OCaml 4.07.0, but it's possible that in macOS that is not the case (I am currently unable to test the exact configuration on macOS). If that works, we will update the installation instructions to no longer refer to `altgr-ergo`, but to `alt-ergo` directly.
(0006644)
hugo.gimbert   
2018-09-11 22:10   
Thanks a lot for the quick feedback. I followed your recommendation and everything went fine, Log below hugo-3:~ gimbert$ opam remove altgr-ergo [NOTE] altgr-ergo is not installed. Nothing to do. hugo-3:~ gimbert$ opam install alt-ergo The following actions will be performed: ∗ install psmt2-frontend 0.1 [required by alt-ergo] ↗ upgrade ocplib-simplex 0.3 to 0.4 [required by alt-ergo] ∗ install alt-ergo 2.2.0 ===== ∗ 2 ↗ 1 ===== Do you want to continue ? [Y/n] Y =-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫 [default] https://opam.ocaml.org/archives/psmt2-frontend.0.1+opam.tar.gz downloaded [default] https://opam.ocaml.org/archives/ocplib-simplex.0.4+opam.tar.gz downloaded [default] https://opam.ocaml.org/archives/alt-ergo.2.2.0+opam.tar.gz downloaded =-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫 ⊘ removed ocplib-simplex.0.3 ∗ installed ocplib-simplex.0.4 ∗ installed psmt2-frontend.0.1 Processing 4/4: [alt-ergo: make install]opam install frama-c ∗ installed alt-ergo.2.2.0 Done. hugo-3:~ gimbert$ opam install frama-c 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 =-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫 [frama-c] Archive in cache =-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫 ∗ installed frama-c.20180502 Done. hugo-3:~ gimbert$
(0006645)
maroneze   
2018-09-12 15:34   
Great! It has been brought to my attention that alt-ergo >=2.0.0 already includes altgr-ergo, so everything should work just fine. Therefore, recommending altgr-ergo is only useful for alt-ergo <= 1.30, and detrimental for recent versions. However, since alt-ergo >= 2.0 requires OCaml 4.04.0 or higher, recommending altgr-ergo is still useful for users with older OCaml versions. The installation instructions will be updated to take those elements into account.
(0006671)
maroneze   
2018-10-29 15:13   
The Frama-C opam file has been updated to detect both cases and emit a relevant message, e.g. "the package altgr-ergo could prevent the installation of newer versions of Alt-Ergo".