Frama-C Bug Tracking System - Frama-C
View Issue Details
0002399Frama-COpampublic2018-09-11 17:502018-11-30 10:07
Reporterhugo.gimbert 
Assigned Tomaroneze 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformAppleOSmacosxOS VersionHighSierra 10.3.
Product VersionFrama-C 17-Chlorine 
Target VersionFrama-C 18-ArgonFixed in VersionFrama-C 18-Argon 
Summary0002399: Failed to install framaC on macosx using opam
DescriptionFollowed 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
TagsNo tags attached.
Attached Files

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".

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