Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
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

- Relationships

-  Notes
(0006643)
maroneze (developer)
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 (reporter)
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 (developer)
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 (developer)
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
Date Modified Username Field Change
2018-09-11 17:50 hugo.gimbert New Issue
2018-09-11 17:50 hugo.gimbert Status new => assigned
2018-09-11 17:50 hugo.gimbert Assigned To => maroneze
2018-09-11 19:16 maroneze Note Added: 0006643
2018-09-11 22:10 hugo.gimbert Note Added: 0006644
2018-09-12 15:34 maroneze Note Added: 0006645
2018-09-14 09:57 signoles Target Version => Frama-C 18-Argon
2018-10-29 15:13 maroneze Note Added: 0006671
2018-10-29 15:13 maroneze Status assigned => resolved
2018-10-29 15:13 maroneze Fixed in Version => Frama-C 18-Argon
2018-10-29 15:13 maroneze Resolution open => fixed
2018-11-30 10:07 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker