0002375: Issues while installation of Frama-C using OPAM

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Tags

No tags attached.

Attached Files

Terminal Saved Output (3,508 bytes) 2018-05-23 12:14

Last login: Wed May 23 12:00:05 on ttys000
wlan022015:~ fauzia$ opam install frama-c
The following actions will be performed:
  ∗  install conf-pkg-config    1.0           [required by conf-gtksourceview]
  ∗  install conf-gnomecanvas   2             [required by frama-c]
  ∗  install conf-gtksourceview 2             [required by frama-c]
  ∗  install lablgtk            2.18.5        [required by frama-c]
  ∗  install ocamlgraph         1.8.8         [required by frama-c]
  ∗  install alt-ergo           2.2.0         [required by frama-c]
  ∗  install frama-c            20171101
       Why3 can be used by the WP plug-in for running additional automatic solvers
       Coq can be used with the WP plug-in for proving interactively proof obligations
       Alt-Ergo Graphical Interface can be used by the WP plug-in
===== ∗  7 =====
Do you want to continue ? [Y/n] Y

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[alt-ergo] Archive in cache
[frama-c] Archive in cache
[lablgtk] Archive in cache
[ocamlgraph] Archive in cache

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[ERROR] The compilation of conf-gnomecanvas failed at "pkg-config
        libgnomecanvas-2.0".
[ERROR] The compilation of conf-pkg-config failed at "pkg-config --help".

#=== ERROR while installing conf-gnomecanvas.2 ================================#
# opam-version 1.2.2
# os           darwin
# command      pkg-config libgnomecanvas-2.0
# path         /Users/fauzia/.opam/4.05.0/build/conf-gnomecanvas.2
# compiler     4.05.0
# exit-code    127
# env-file     /Users/fauzia/.opam/4.05.0/build/conf-gnomecanvas.2/conf-gnomecanvas-17330-ffb3fd.env
# stdout-file  /Users/fauzia/.opam/4.05.0/build/conf-gnomecanvas.2/conf-gnomecanvas-17330-ffb3fd.out
# stderr-file  /Users/fauzia/.opam/4.05.0/build/conf-gnomecanvas.2/conf-gnomecanvas-17330-ffb3fd.err


#=== ERROR while installing conf-pkg-config.1.0 ===============================#
# opam-version 1.2.2
# os           darwin
# command      pkg-config --help
# path         /Users/fauzia/.opam/4.05.0/build/conf-pkg-config.1.0
# compiler     4.05.0
# exit-code    127
# env-file     /Users/fauzia/.opam/4.05.0/build/conf-pkg-config.1.0/conf-pkg-config-17330-05296d.env
# stdout-file  /Users/fauzia/.opam/4.05.0/build/conf-pkg-config.1.0/conf-pkg-config-17330-05296d.out
# stderr-file  /Users/fauzia/.opam/4.05.0/build/conf-pkg-config.1.0/conf-pkg-config-17330-05296d.err



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
The following actions were aborted
  ∗  install alt-ergo           2.2.0   
  ∗  install conf-gtksourceview 2       
  ∗  install frama-c            20171101
  ∗  install lablgtk            2.18.5  
  ∗  install ocamlgraph         1.8.8   
The following actions failed
  ∗  install conf-gnomecanvas 2  
  ∗  install conf-pkg-config  1.0
No changes have been performed

=-=- conf-gnomecanvas.2 troobleshooting -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
=> This package relies on external (system) dependencies that may be missing.
   `opam depext conf-gnomecanvas.2' may help you find the correct installation
   for your system.

=-=- conf-pkg-config.1.0 troobleshooting =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
=> This package relies on external (system) dependencies that may be missing.
   `opam depext conf-pkg-config.1.0' may help you find the correct installation
   for your system.
wlan022015:~ fauzia$

Terminal Saved Output (3,508 bytes) 2018-05-23 12:14

framaC_Output (9,610 bytes) 2018-06-04 13:37

Last login: Wed May 30 14:09:54 on ttys000
wlan017014:~ fauzia$ cd software/frama-c
wlan017014:frama-c fauzia$ opam init --auto-setup
OPAM has already been initialized.User configuration:
  ~/.ocamlinit is already up-to-date.
  ~/.bash_profile is already up-to-date.
Global configuration:
  ~/.opam/opam-init/init.sh is already up-to-date.
  ~/.opam/opam-init/init.zsh is already up-to-date.
  ~/.opam/opam-init/init.csh is already up-to-date.
  ~/.opam/opam-init/init.fish is already up-to-date.
wlan017014:frama-c fauzia$ opam eval $(opam config env)
opam: unknown command `eval'.
Usage: opam COMMAND ...
Try `opam --help' for more information.
wlan017014:frama-c fauzia$ eval $(opam config env)
wlan017014:frama-c fauzia$ brew install autoconf pkg-config opam
Updating Homebrew...
==> Auto-updated Homebrew!
Updated 1 tap (homebrew/cask-versions).
No changes to formulae.

Warning: autoconf 2.69 is already installed and up-to-date
To reinstall 2.69, run `brew reinstall autoconf`
Warning: pkg-config 0.29.2 is already installed and up-to-date
To reinstall 0.29.2, run `brew reinstall pkg-config`
Warning: opam 1.2.2_4 is already installed and up-to-date
To reinstall 1.2.2_4, run `brew reinstall opam`
wlan017014:frama-c fauzia$ brew reinstall autoconf pkg-config opam
==> Reinstalling autoconf 
==> Downloading https://homebrew.bintray.com/bottles/autoconf-2.69.high_sierra.b
Already downloaded: /Users/fauzia/Library/Caches/Homebrew/autoconf-2.69.high_sierra.bottle.4.tar.gz
==> Pouring autoconf-2.69.high_sierra.bottle.4.tar.gz
==> Caveats
Emacs Lisp files have been installed to:
  /usr/local/share/emacs/site-lisp/autoconf
==> Summary
🍺  /usr/local/Cellar/autoconf/2.69: 71 files, 3.0MB
==> Reinstalling pkg-config 
==> Downloading https://homebrew.bintray.com/bottles/pkg-config-0.29.2.high_sier
Already downloaded: /Users/fauzia/Library/Caches/Homebrew/pkg-config-0.29.2.high_sierra.bottle.tar.gz
==> Pouring pkg-config-0.29.2.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/pkg-config/0.29.2: 11 files, 627.2KB
==> Reinstalling opam 
==> Installing dependencies for opam: ocamlbuild
==> Installing opam dependency: ocamlbuild
==> Downloading https://homebrew.bintray.com/bottles/ocamlbuild-0.12.0_1.high_si
==> Downloading from https://akamai.bintray.com/15/15cfc6410c77840c1c30a97fc9e26
######################################################################## 100.0%
==> Pouring ocamlbuild-0.12.0_1.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/ocamlbuild/0.12.0_1: 30 files, 7.5MB
==> Installing opam
==> Downloading https://homebrew.bintray.com/bottles/opam-1.2.2_4.high_sierra.bo
Already downloaded: /Users/fauzia/Library/Caches/Homebrew/opam-1.2.2_4.high_sierra.bottle.tar.gz
==> Pouring opam-1.2.2_4.high_sierra.bottle.tar.gz
==> Caveats
OPAM uses ~/.opam by default for its package database, so you need to
initialize it first by running (as a normal user):

$  opam init

Run the following to initialize your environment variables:

$  eval `opam config env`

To export the needed variables every time, add them to your dotfiles.
  * On Bash, add them to `~/.bash_profile`.
  * On Zsh, add them to `~/.zprofile` or `~/.zshrc` instead.

Documentation and tutorials are available at https://opam.ocaml.org, or
via "man opam" and "opam --help".

Bash completion has been installed to:
  /usr/local/etc/bash_completion.d

zsh completions have been installed to:
  /usr/local/share/zsh/site-functions
==> Summary
🍺  /usr/local/Cellar/opam/1.2.2_4: 31 files, 16.3MB
wlan017014:frama-c fauzia$ opam init
OPAM has already been initialized.
In normal operation, OPAM only alters files within ~/.opam.

During this initialisation, you can allow OPAM to add information to two
other files for best results. You can also make these additions manually
if you wish.

If you agree, OPAM will modify:

  - ~/.bash_profile (or a file you specify) to set the right environment
    variables and to load the auto-completion scripts for your shell (bash)
    on startup. Specifically, it checks for and appends the following line:

    . /Users/fauzia/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true


  - ~/.ocamlinit to ensure that non-system installations of `ocamlfind`
    (i.e. those installed by OPAM) will work correctly when running the
    OCaml toplevel. It does this by adding $OCAML_TOPLEVEL_PATH to the list
    of include directories.

If you choose to not configure your system now, you can either configure
OPAM manually (instructions will be displayed) or launch the automatic setup
later by running:

   opam config setup -a


Do you want OPAM to modify ~/.bash_profile and ~/.ocamlinit?
(default is 'no', use 'f' to name a file other than ~/.bash_profile)
    [N/y/f] y

User configuration:
  ~/.ocamlinit is already up-to-date.
  ~/.bash_profile is already up-to-date.
Global configuration:
  ~/.opam/opam-init/init.sh is already up-to-date.
  ~/.opam/opam-init/init.zsh is already up-to-date.
  ~/.opam/opam-init/init.csh is already up-to-date.
  ~/.opam/opam-init/init.fish is already up-to-date.
wlan017014:frama-c fauzia$ eval `opam config env`
wlan017014:frama-c fauzia$ brew install gmp gtk+ gtksourceview libgnomecanvas
Updating Homebrew...
==> Auto-updated Homebrew!
Updated 1 tap (homebrew/cask).
No changes to formulae.

Warning: gmp 6.1.2_2 is already installed and up-to-date
To reinstall 6.1.2_2, run `brew reinstall gmp`
Warning: gtk+ 2.24.32_2 is already installed and up-to-date
To reinstall 2.24.32_2, run `brew reinstall gtk+`
Warning: gtksourceview 2.10.5_3 is already installed and up-to-date
To reinstall 2.10.5_3, run `brew reinstall gtksourceview`
Warning: libgnomecanvas 2.30.3_3 is already installed and up-to-date
To reinstall 2.30.3_3, run `brew reinstall libgnomecanvas`
wlan017014:frama-c fauzia$ brew reinstall gmp gtk+ gtksourceview libgnomecanvas
==> Reinstalling gmp 
==> Downloading https://homebrew.bintray.com/bottles/gmp-6.1.2_2.high_sierra.bot
Already downloaded: /Users/fauzia/Library/Caches/Homebrew/gmp-6.1.2_2.high_sierra.bottle.tar.gz
==> Pouring gmp-6.1.2_2.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/gmp/6.1.2_2: 18 files, 3.1MB
==> Reinstalling gtk+ 
==> Downloading https://homebrew.bintray.com/bottles/gtk+-2.24.32_2.high_sierra.
Already downloaded: /Users/fauzia/Library/Caches/Homebrew/gtk+-2.24.32_2.high_sierra.bottle.tar.gz
==> Pouring gtk+-2.24.32_2.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/gtk+/2.24.32_2: 1,174 files, 50.6MB
==> Reinstalling gtksourceview 
==> Installing dependencies for gtksourceview: libepoxy, gtk-mac-integration
==> Installing gtksourceview dependency: libepoxy
==> Downloading https://homebrew.bintray.com/bottles/libepoxy-1.5.2.high_sierra.
==> Downloading from https://akamai.bintray.com/07/0748efd9737fe67c0b55dc6b21b92
######################################################################## 100.0%
==> Pouring libepoxy-1.5.2.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/libepoxy/1.5.2: 11 files, 2.6MB
==> Installing gtksourceview dependency: gtk-mac-integration
==> Downloading https://homebrew.bintray.com/bottles/gtk-mac-integration-2.1.2.h
######################################################################## 100.0%
==> Pouring gtk-mac-integration-2.1.2.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/gtk-mac-integration/2.1.2: 53 files, 336.8KB
==> Installing gtksourceview
==> Downloading https://homebrew.bintray.com/bottles/gtksourceview-2.10.5_3.high
Already downloaded: /Users/fauzia/Library/Caches/Homebrew/gtksourceview-2.10.5_3.high_sierra.bottle.tar.gz
==> Pouring gtksourceview-2.10.5_3.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/gtksourceview/2.10.5_3: 230 files, 4.6MB
==> Reinstalling libgnomecanvas 
==> Downloading https://homebrew.bintray.com/bottles/libgnomecanvas-2.30.3_3.hig
Already downloaded: /Users/fauzia/Library/Caches/Homebrew/libgnomecanvas-2.30.3_3.high_sierra.bottle.tar.gz
==> Pouring libgnomecanvas-2.30.3_3.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/libgnomecanvas/2.30.3_3: 142 files, 1.6MB
wlan017014:frama-c fauzia$ opam install frama-c
[ERROR] Timeout trying to acquire write lock to
        "/Users/fauzia/.opam/system/lock", is another opam process running ?
wlan017014:frama-c fauzia$ opam install frama-c
The following dependencies couldn't be met:
  - frama-c -> coq
  - frama-c -> frama-c-base (= 20150201 | = 20151002 | = 20160502 | = 20161101 | = 20170501)
Your request can't be satisfied:
  - coq.8.7.0 is in conflict with frama-c.20171101
  - coq.8.7.1 is in conflict with frama-c.20171101
  - coq.8.7.1+1 is in conflict with frama-c.20171101
  - coq.8.7.1+2 is in conflict with frama-c.20171101
  - coq.8.7.2 is in conflict with frama-c.20171101
  - coq.8.8.0 is in conflict with frama-c.20171101
  - frama-c-base.20150201 is not available because your system doesn't comply with ocaml-version >= "4.0" & ocaml-version != "4.02.0" & ocaml-version < "4.04.0".
  - frama-c-base.20151002 is not available because your system doesn't comply with ocaml-version >= "4.0" & ocaml-version != "4.02.0" & ocaml-version != "4.02.2" & ocaml-version < "4.04.0".
  - frama-c-base.20160502 is not available because your system doesn't comply with ocaml-version >= "4.00.1" & ocaml-version != "4.02.0" & ocaml-version != "4.02.2" & ocaml-version < "4.04.0".
  - frama-c-base.20161101 is not available because your system doesn't comply with ocaml-version >= "4.02.3" & ocaml-version < "4.06".
  - frama-c-base.20170501 is not available because your system doesn't comply with ocaml-version >= "4.02.3" & ocaml-version < "4.06".

No solution found, exiting
wlan017014:frama-c fauzia$ eval `opam config env`

framaC_Output (9,610 bytes) 2018-06-04 13:37

Frama-CUpgrade (33,883 bytes) 2018-06-04 14:03

Last login: Mon Jun  4 13:27:24 on ttys000
wlan017014:~ fauzia$ cd software/frama-c/
wlan017014:frama-c fauzia$ opam upgrade
The following actions will be performed:
  ↗  upgrade   coq             8.7.2 to 8.8.0      
  ↗  upgrade   ocplib-simplex  0.3 to 0.4          
  ↗  upgrade   conf-pkg-config 1.0 to 1.1          
  ↗  upgrade   menhir          20171222 to 20180530
  ↗  upgrade   coqide          8.7.2 to 8.8.0      
  ↻  recompile psmt2-frontend  0.1                   [uses menhir]
===== ↻  1   ↗  5 =====
Do you want to continue ? [Y/n] Y

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[default] https://opam.ocaml.org/archives/coq.8.8.0+opam.tar.gz downloaded
[default] https://opam.ocaml.org/archives/coqide.8.7.2+opam.tar.gz downloaded
[default] https://opam.ocaml.org/archives/coq.8.7.2+opam.tar.gz downloaded
[default] https://opam.ocaml.org/archives/menhir.20171222+opam.tar.gz downloaded
[ocplib-simplex] Archive in cache
[default] https://opam.ocaml.org/archives/psmt2-frontend.0.1+opam.tar.gz downloaded
[default] https://opam.ocaml.org/archives/menhir.20180530+opam.tar.gz downloaded
[default] https://opam.ocaml.org/archives/coqide.8.8.0+opam.tar.gz downloaded

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
⊘  removed   conf-pkg-config.1.0
⊘  removed   ocplib-simplex.0.3
∗  installed conf-pkg-config.1.1
⊘  removed   psmt2-frontend.0.1
⊘  removed   coqide.8.7.2
⊘  removed   menhir.20171222
⊘  removed   coq.8.7.2
∗  installed ocplib-simplex.0.4
∗  installed menhir.20180530
∗  installed psmt2-frontend.0.1
∗  installed coq.8.8.0
∗  installed coqide.8.8.0
Done.
wlan017014:frama-c fauzia$ opam install frama-c
The following actions will be performed:
  ∗  install alt-ergo 2.2.0                   [required by frama-c]
  ∗  install frama-c  20180501
       Why3 can be used by the WP plug-in for running additional automatic solvers
       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
[default] https://opam.ocaml.org/archives/frama-c.20180501+opam.tar.gz downloaded

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
[ERROR] The compilation of alt-ergo failed at "make install
        MANDIR=/Users/fauzia/.opam/system/man".
[WARNING] Directory /Users/fauzia/.opam/system/lib/alt-ergo is not empty, not
          removing

#=== ERROR while installing alt-ergo.2.2.0 ====================================#
# opam-version 1.2.2
# os           darwin
# command      make install MANDIR=/Users/fauzia/.opam/system/man
# path         /Users/fauzia/.opam/system/build/alt-ergo.2.2.0
# compiler     system (4.06.1)
# exit-code    2
# env-file     /Users/fauzia/.opam/system/build/alt-ergo.2.2.0/alt-ergo-14788-0a5907.env
# stdout-file  /Users/fauzia/.opam/system/build/alt-ergo.2.2.0/alt-ergo-14788-0a5907.out
# stderr-file  /Users/fauzia/.opam/system/build/alt-ergo.2.2.0/alt-ergo-14788-0a5907.err
### stdout ###
# [...]
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -for-pack AltErgoLib parsers/why/why_parser.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -for-pack AltErgoLib parsers/why/why_lexer.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -for-pack AltErgoLib parsers/smt2/psmt2_to_alt_ergo.ml
# ocamlc.opt -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -pack -o altErgoLib.cmo lib/util/config.cmo lib/util/version.cmo lib/util/emap.cmo lib/util/myUnix.cmo lib/util/myDynlink.cmo lib/util/myZip.cmo lib/util/util.cmo lib/util/lists.cmo lib/util/numsNumbers.cmo lib/util/zarithNumbers.cmo lib/util/numbers.cmo lib/util/options.cmo lib/util/vec.cmo lib/util/iheap.cmo lib/util/timers.cmo lib/util/gc_debug.cmo lib/util/loc.cmo lib/util/hconsing.cmo lib/util/hstring.cmo lib/structures/exception.cmo lib/structures/symbols.cmo lib/structures/ty.cmo lib/structures/parsed.cmo lib/structures/errors.cmo lib/structures/typed.cmo lib/structures/term.cmo lib/structures/fpa_rounding.cmo lib/structures/literal.cmo lib/structures/formula.cmo lib/structures/satml_types.cmo lib/structures/explanation.cmo lib/structures/commands.cmo lib/structures/profiling.cmo lib/reasoners/matching.cmo lib/reasoners/instances.cmo lib/reasoners/polynome.cmo lib/reasoners/ac.cmo lib/reasoners/uf.cmo lib/reasoners/use.cmo lib/reasoners/intervals.cmo lib/reasoners/inequalities.cmo lib/reasoners/intervalCalculus.cmo lib/reasoners/arith.cmo lib/reasoners/records.cmo lib/reasoners/bitv.cmo lib/reasoners/arrays.cmo lib/reasoners/sum.cmo lib/reasoners/ite.cmo lib/reasoners/combine.cmo lib/reasoners/ccx.cmo lib/reasoners/theory.cmo lib/reasoners/sat_solver_sig.cmo lib/reasoners/fun_sat.cmo lib/reasoners/satml.cmo lib/reasoners/satml_frontend.cmo lib/reasoners/sat_solver.cmo lib/frontend/triggers.cmo lib/frontend/cnf.cmo lib/frontend/typechecker.cmo lib/frontend/parsed_interface.cmo lib/frontend/frontend.cmo lib/frontend/parsers.cmo parsers/why/why_parser.cmo parsers/why/why_lexer.cmo parsers/smt2/psmt2_to_alt_ergo.cmo lib/reasoners/sig.cmi
# ocamlc.opt -a -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -o altErgoLib.cma altErgoLib.cmo
# ocamlopt.opt -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -inline 100 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex  -pack -o altErgoLib.cmx lib/util/config.cmx lib/util/version.cmx lib/util/emap.cmx lib/util/myUnix.cmx lib/util/myDynlink.cmx lib/util/myZip.cmx lib/util/util.cmx lib/util/lists.cmx lib/util/numsNumbers.cmx lib/util/zarithNumbers.cmx lib/util/numbers.cmx lib/util/options.cmx lib/util/vec.cmx lib/util/iheap.cmx lib/util/timers.cmx lib/util/gc_debug.cmx lib/util/loc.cmx lib/util/hconsing.cmx lib/util/hstring.cmx lib/structures/exception.cmx lib/structures/symbols.cmx lib/structures/ty.cmx lib/structures/parsed.cmx lib/structures/errors.cmx lib/structures/typed.cmx lib/structures/term.cmx lib/structures/fpa_rounding.cmx lib/structures/literal.cmx lib/structures/formula.cmx lib/structures/satml_types.cmx lib/structures/explanation.cmx lib/structures/commands.cmx lib/structures/profiling.cmx lib/reasoners/matching.cmx lib/reasoners/instances.cmx lib/reasoners/polynome.cmx lib/reasoners/ac.cmx lib/reasoners/uf.cmx lib/reasoners/use.cmx lib/reasoners/intervals.cmx lib/reasoners/inequalities.cmx lib/reasoners/intervalCalculus.cmx lib/reasoners/arith.cmx lib/reasoners/records.cmx lib/reasoners/bitv.cmx lib/reasoners/arrays.cmx lib/reasoners/sum.cmx lib/reasoners/ite.cmx lib/reasoners/combine.cmx lib/reasoners/ccx.cmx lib/reasoners/theory.cmx lib/reasoners/sat_solver_sig.cmx lib/reasoners/fun_sat.cmx lib/reasoners/satml.cmx lib/reasoners/satml_frontend.cmx lib/reasoners/sat_solver.cmx lib/frontend/triggers.cmx lib/frontend/cnf.cmx lib/frontend/typechecker.cmx lib/frontend/parsed_interface.cmx lib/frontend/frontend.cmx lib/frontend/parsers.cmx parsers/why/why_parser.cmx parsers/why/why_lexer.cmx parsers/smt2/psmt2_to_alt_ergo.cmx lib/reasoners/sig.cmi
# ocamlopt.opt -a -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -inline 100 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -o altErgoLib.cmxa altErgoLib.cmx
# ocamlopt.opt -shared -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -inline 100 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -o altErgoLib.cmxs altErgoLib.cmx
# OCAMLFIND_DESTDIR=/Users/fauzia/.opam/system/lib \
# 	  ocamlfind install alt-ergo altErgoLib.* META
### stderr ###
# ocamlfind: Conflict with file: /Users/fauzia/.opam/system/lib/alt-ergo/altErgoLib.cmx
# make: *** [install-lib] Error 2



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
The following actions were aborted
  ∗  install frama-c 20180501
The following actions failed
  ∗  install alt-ergo 2.2.0
No changes have been performed
wlan017014:frama-c fauzia$  brew install autoconf pkg-config opam
Warning: autoconf 2.69 is already installed and up-to-date
To reinstall 2.69, run `brew reinstall autoconf`
Warning: pkg-config 0.29.2 is already installed and up-to-date
To reinstall 0.29.2, run `brew reinstall pkg-config`
Warning: opam 1.2.2_4 is already installed and up-to-date
To reinstall 1.2.2_4, run `brew reinstall opam`
wlan017014:frama-c fauzia$ brew install gmp gtk+ gtksourceview libgnomecanvas
Warning: gmp 6.1.2_2 is already installed and up-to-date
To reinstall 6.1.2_2, run `brew reinstall gmp`
Warning: gtk+ 2.24.32_2 is already installed and up-to-date
To reinstall 2.24.32_2, run `brew reinstall gtk+`
Warning: gtksourceview 2.10.5_3 is already installed and up-to-date
To reinstall 2.10.5_3, run `brew reinstall gtksourceview`
Warning: libgnomecanvas 2.30.3_3 is already installed and up-to-date
To reinstall 2.30.3_3, run `brew reinstall libgnomecanvas`
wlan017014:frama-c fauzia$ opam install frama-c
The following actions will be performed:
  ∗  install alt-ergo 2.2.0                   [required by frama-c]
  ∗  install frama-c  20180501
       Why3 can be used by the WP plug-in for running additional automatic solvers
       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 install MANDIR=/Users/fauzia/.opam/system/man".
[WARNING] Directory /Users/fauzia/.opam/system/lib/alt-ergo is not empty, not removing

#=== ERROR while installing alt-ergo.2.2.0 ====================================#
# opam-version 1.2.2
# os           darwin
# command      make install MANDIR=/Users/fauzia/.opam/system/man
# path         /Users/fauzia/.opam/system/build/alt-ergo.2.2.0
# compiler     system (4.06.1)
# exit-code    2
# env-file     /Users/fauzia/.opam/system/build/alt-ergo.2.2.0/alt-ergo-17320-d0f245.env
# stdout-file  /Users/fauzia/.opam/system/build/alt-ergo.2.2.0/alt-ergo-17320-d0f245.out
# stderr-file  /Users/fauzia/.opam/system/build/alt-ergo.2.2.0/alt-ergo-17320-d0f245.err
### stdout ###
# [...]
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -for-pack AltErgoLib parsers/why/why_parser.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -for-pack AltErgoLib parsers/why/why_lexer.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -for-pack AltErgoLib parsers/smt2/psmt2_to_alt_ergo.ml
# ocamlc.opt -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -pack -o altErgoLib.cmo lib/util/config.cmo lib/util/version.cmo lib/util/emap.cmo lib/util/myUnix.cmo lib/util/myDynlink.cmo lib/util/myZip.cmo lib/util/util.cmo lib/util/lists.cmo lib/util/numsNumbers.cmo lib/util/zarithNumbers.cmo lib/util/numbers.cmo lib/util/options.cmo lib/util/vec.cmo lib/util/iheap.cmo lib/util/timers.cmo lib/util/gc_debug.cmo lib/util/loc.cmo lib/util/hconsing.cmo lib/util/hstring.cmo lib/structures/exception.cmo lib/structures/symbols.cmo lib/structures/ty.cmo lib/structures/parsed.cmo lib/structures/errors.cmo lib/structures/typed.cmo lib/structures/term.cmo lib/structures/fpa_rounding.cmo lib/structures/literal.cmo lib/structures/formula.cmo lib/structures/satml_types.cmo lib/structures/explanation.cmo lib/structures/commands.cmo lib/structures/profiling.cmo lib/reasoners/matching.cmo lib/reasoners/instances.cmo lib/reasoners/polynome.cmo lib/reasoners/ac.cmo lib/reasoners/uf.cmo lib/reasoners/use.cmo lib/reasoners/intervals.cmo lib/reasoners/inequalities.cmo lib/reasoners/intervalCalculus.cmo lib/reasoners/arith.cmo lib/reasoners/records.cmo lib/reasoners/bitv.cmo lib/reasoners/arrays.cmo lib/reasoners/sum.cmo lib/reasoners/ite.cmo lib/reasoners/combine.cmo lib/reasoners/ccx.cmo lib/reasoners/theory.cmo lib/reasoners/sat_solver_sig.cmo lib/reasoners/fun_sat.cmo lib/reasoners/satml.cmo lib/reasoners/satml_frontend.cmo lib/reasoners/sat_solver.cmo lib/frontend/triggers.cmo lib/frontend/cnf.cmo lib/frontend/typechecker.cmo lib/frontend/parsed_interface.cmo lib/frontend/frontend.cmo lib/frontend/parsers.cmo parsers/why/why_parser.cmo parsers/why/why_lexer.cmo parsers/smt2/psmt2_to_alt_ergo.cmo lib/reasoners/sig.cmi
# ocamlc.opt -a -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -o altErgoLib.cma altErgoLib.cmo
# ocamlopt.opt -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -inline 100 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex  -pack -o altErgoLib.cmx lib/util/config.cmx lib/util/version.cmx lib/util/emap.cmx lib/util/myUnix.cmx lib/util/myDynlink.cmx lib/util/myZip.cmx lib/util/util.cmx lib/util/lists.cmx lib/util/numsNumbers.cmx lib/util/zarithNumbers.cmx lib/util/numbers.cmx lib/util/options.cmx lib/util/vec.cmx lib/util/iheap.cmx lib/util/timers.cmx lib/util/gc_debug.cmx lib/util/loc.cmx lib/util/hconsing.cmx lib/util/hstring.cmx lib/structures/exception.cmx lib/structures/symbols.cmx lib/structures/ty.cmx lib/structures/parsed.cmx lib/structures/errors.cmx lib/structures/typed.cmx lib/structures/term.cmx lib/structures/fpa_rounding.cmx lib/structures/literal.cmx lib/structures/formula.cmx lib/structures/satml_types.cmx lib/structures/explanation.cmx lib/structures/commands.cmx lib/structures/profiling.cmx lib/reasoners/matching.cmx lib/reasoners/instances.cmx lib/reasoners/polynome.cmx lib/reasoners/ac.cmx lib/reasoners/uf.cmx lib/reasoners/use.cmx lib/reasoners/intervals.cmx lib/reasoners/inequalities.cmx lib/reasoners/intervalCalculus.cmx lib/reasoners/arith.cmx lib/reasoners/records.cmx lib/reasoners/bitv.cmx lib/reasoners/arrays.cmx lib/reasoners/sum.cmx lib/reasoners/ite.cmx lib/reasoners/combine.cmx lib/reasoners/ccx.cmx lib/reasoners/theory.cmx lib/reasoners/sat_solver_sig.cmx lib/reasoners/fun_sat.cmx lib/reasoners/satml.cmx lib/reasoners/satml_frontend.cmx lib/reasoners/sat_solver.cmx lib/frontend/triggers.cmx lib/frontend/cnf.cmx lib/frontend/typechecker.cmx lib/frontend/parsed_interface.cmx lib/frontend/frontend.cmx lib/frontend/parsers.cmx parsers/why/why_parser.cmx parsers/why/why_lexer.cmx parsers/smt2/psmt2_to_alt_ergo.cmx lib/reasoners/sig.cmi
# ocamlopt.opt -a -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -inline 100 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -o altErgoLib.cmxa altErgoLib.cmx
# ocamlopt.opt -shared -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -inline 100 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -o altErgoLib.cmxs altErgoLib.cmx
# OCAMLFIND_DESTDIR=/Users/fauzia/.opam/system/lib \
# 	  ocamlfind install alt-ergo altErgoLib.* META
### stderr ###
# ocamlfind: Conflict with file: /Users/fauzia/.opam/system/lib/alt-ergo/altErgoLib.cmx
# make: *** [install-lib] Error 2



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
The following actions were aborted
  ∗  install frama-c 20180501
The following actions failed
  ∗  install alt-ergo 2.2.0
No changes have been performed
wlan017014:frama-c fauzia$ opam init
OPAM has already been initialized.
In normal operation, OPAM only alters files within ~/.opam.

During this initialisation, you can allow OPAM to add information to two
other files for best results. You can also make these additions manually
if you wish.

If you agree, OPAM will modify:

  - ~/.bash_profile (or a file you specify) to set the right environment
    variables and to load the auto-completion scripts for your shell (bash)
    on startup. Specifically, it checks for and appends the following line:

    . /Users/fauzia/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true


  - ~/.ocamlinit to ensure that non-system installations of `ocamlfind`
    (i.e. those installed by OPAM) will work correctly when running the
    OCaml toplevel. It does this by adding $OCAML_TOPLEVEL_PATH to the list
    of include directories.

If you choose to not configure your system now, you can either configure
OPAM manually (instructions will be displayed) or launch the automatic setup
later by running:

   opam config setup -a


Do you want OPAM to modify ~/.bash_profile and ~/.ocamlinit?
(default is 'no', use 'f' to name a file other than ~/.bash_profile)
    [N/y/f] y

User configuration:
  ~/.ocamlinit is already up-to-date.
  ~/.bash_profile is already up-to-date.
Global configuration:
  ~/.opam/opam-init/init.sh is already up-to-date.
  ~/.opam/opam-init/init.zsh is already up-to-date.
  ~/.opam/opam-init/init.csh is already up-to-date.
  ~/.opam/opam-init/init.fish is already up-to-date.
wlan017014:frama-c fauzia$ eval `opam config env`
wlan017014:frama-c fauzia$ opam install frama-c
The following actions will be performed:
  ∗  install alt-ergo 2.2.0                   [required by frama-c]
  ∗  install frama-c  20180501
       Why3 can be used by the WP plug-in for running additional automatic solvers
       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 install MANDIR=/Users/fauzia/.opam/system/man".
[WARNING] Directory /Users/fauzia/.opam/system/lib/alt-ergo is not empty, not removing

#=== ERROR while installing alt-ergo.2.2.0 ====================================#
# opam-version 1.2.2
# os           darwin
# command      make install MANDIR=/Users/fauzia/.opam/system/man
# path         /Users/fauzia/.opam/system/build/alt-ergo.2.2.0
# compiler     system (4.06.1)
# exit-code    2
# env-file     /Users/fauzia/.opam/system/build/alt-ergo.2.2.0/alt-ergo-18970-d0f245.env
# stdout-file  /Users/fauzia/.opam/system/build/alt-ergo.2.2.0/alt-ergo-18970-d0f245.out
# stderr-file  /Users/fauzia/.opam/system/build/alt-ergo.2.2.0/alt-ergo-18970-d0f245.err
### stdout ###
# [...]
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -for-pack AltErgoLib parsers/why/why_parser.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -for-pack AltErgoLib parsers/why/why_lexer.ml
# ocamlc.opt -c -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -for-pack AltErgoLib parsers/smt2/psmt2_to_alt_ergo.ml
# ocamlc.opt -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -pack -o altErgoLib.cmo lib/util/config.cmo lib/util/version.cmo lib/util/emap.cmo lib/util/myUnix.cmo lib/util/myDynlink.cmo lib/util/myZip.cmo lib/util/util.cmo lib/util/lists.cmo lib/util/numsNumbers.cmo lib/util/zarithNumbers.cmo lib/util/numbers.cmo lib/util/options.cmo lib/util/vec.cmo lib/util/iheap.cmo lib/util/timers.cmo lib/util/gc_debug.cmo lib/util/loc.cmo lib/util/hconsing.cmo lib/util/hstring.cmo lib/structures/exception.cmo lib/structures/symbols.cmo lib/structures/ty.cmo lib/structures/parsed.cmo lib/structures/errors.cmo lib/structures/typed.cmo lib/structures/term.cmo lib/structures/fpa_rounding.cmo lib/structures/literal.cmo lib/structures/formula.cmo lib/structures/satml_types.cmo lib/structures/explanation.cmo lib/structures/commands.cmo lib/structures/profiling.cmo lib/reasoners/matching.cmo lib/reasoners/instances.cmo lib/reasoners/polynome.cmo lib/reasoners/ac.cmo lib/reasoners/uf.cmo lib/reasoners/use.cmo lib/reasoners/intervals.cmo lib/reasoners/inequalities.cmo lib/reasoners/intervalCalculus.cmo lib/reasoners/arith.cmo lib/reasoners/records.cmo lib/reasoners/bitv.cmo lib/reasoners/arrays.cmo lib/reasoners/sum.cmo lib/reasoners/ite.cmo lib/reasoners/combine.cmo lib/reasoners/ccx.cmo lib/reasoners/theory.cmo lib/reasoners/sat_solver_sig.cmo lib/reasoners/fun_sat.cmo lib/reasoners/satml.cmo lib/reasoners/satml_frontend.cmo lib/reasoners/sat_solver.cmo lib/frontend/triggers.cmo lib/frontend/cnf.cmo lib/frontend/typechecker.cmo lib/frontend/parsed_interface.cmo lib/frontend/frontend.cmo lib/frontend/parsers.cmo parsers/why/why_parser.cmo parsers/why/why_lexer.cmo parsers/smt2/psmt2_to_alt_ergo.cmo lib/reasoners/sig.cmi
# ocamlc.opt -a -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -o altErgoLib.cma altErgoLib.cmo
# ocamlopt.opt -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -inline 100 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex  -pack -o altErgoLib.cmx lib/util/config.cmx lib/util/version.cmx lib/util/emap.cmx lib/util/myUnix.cmx lib/util/myDynlink.cmx lib/util/myZip.cmx lib/util/util.cmx lib/util/lists.cmx lib/util/numsNumbers.cmx lib/util/zarithNumbers.cmx lib/util/numbers.cmx lib/util/options.cmx lib/util/vec.cmx lib/util/iheap.cmx lib/util/timers.cmx lib/util/gc_debug.cmx lib/util/loc.cmx lib/util/hconsing.cmx lib/util/hstring.cmx lib/structures/exception.cmx lib/structures/symbols.cmx lib/structures/ty.cmx lib/structures/parsed.cmx lib/structures/errors.cmx lib/structures/typed.cmx lib/structures/term.cmx lib/structures/fpa_rounding.cmx lib/structures/literal.cmx lib/structures/formula.cmx lib/structures/satml_types.cmx lib/structures/explanation.cmx lib/structures/commands.cmx lib/structures/profiling.cmx lib/reasoners/matching.cmx lib/reasoners/instances.cmx lib/reasoners/polynome.cmx lib/reasoners/ac.cmx lib/reasoners/uf.cmx lib/reasoners/use.cmx lib/reasoners/intervals.cmx lib/reasoners/inequalities.cmx lib/reasoners/intervalCalculus.cmx lib/reasoners/arith.cmx lib/reasoners/records.cmx lib/reasoners/bitv.cmx lib/reasoners/arrays.cmx lib/reasoners/sum.cmx lib/reasoners/ite.cmx lib/reasoners/combine.cmx lib/reasoners/ccx.cmx lib/reasoners/theory.cmx lib/reasoners/sat_solver_sig.cmx lib/reasoners/fun_sat.cmx lib/reasoners/satml.cmx lib/reasoners/satml_frontend.cmx lib/reasoners/sat_solver.cmx lib/frontend/triggers.cmx lib/frontend/cnf.cmx lib/frontend/typechecker.cmx lib/frontend/parsed_interface.cmx lib/frontend/frontend.cmx lib/frontend/parsers.cmx parsers/why/why_parser.cmx parsers/why/why_lexer.cmx parsers/smt2/psmt2_to_alt_ergo.cmx lib/reasoners/sig.cmi
# ocamlopt.opt -a -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -inline 100 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -o altErgoLib.cmxa altErgoLib.cmx
# ocamlopt.opt -shared -annot -absname -bin-annot -short-paths -strict-sequence -g -w +A-45-27-4-9-44-32-48-41-6-22 -inline 100 -I /Users/fauzia/.opam/system/lib/num -I /Users/fauzia/.opam/system/lib/zarith -I /Users/fauzia/.opam/system/lib/lablgtk2 -I +threads  -I /Users/fauzia/.opam/system/lib/camlzip/../zip -I /Users/fauzia/.opam/system/lib/ocplib-simplex -I /Users/fauzia/.opam/system/lib/psmt2-frontend -I lib/util -I lib/structures -I lib/reasoners -I lib/frontend -I tools/text -I tools/gui -I parsers/why -I parsers/smt2 -I plugins/fm-simplex -o altErgoLib.cmxs altErgoLib.cmx
# OCAMLFIND_DESTDIR=/Users/fauzia/.opam/system/lib \
# 	  ocamlfind install alt-ergo altErgoLib.* META
### stderr ###
# ocamlfind: Conflict with file: /Users/fauzia/.opam/system/lib/alt-ergo/altErgoLib.cmx
# make: *** [install-lib] Error 2



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 
The following actions were aborted
  ∗  install frama-c 20180501
The following actions failed
  ∗  install alt-ergo 2.2.0
No changes have been performed
wlan017014:frama-c fauzia$

Frama-CUpgrade (33,883 bytes) 2018-06-04 14:03

Relationships

Relationships

Notes
~0006552 maroneze (administrator) 2018-05-28 18:26	From the error messages, all I can see is that there seems to be an issue with pkg-config: either it is not installed, or not working properly Did you run the command suggested at the end of the log? If so, what did that output? Please try: opam depext conf-pkg-config.1.0 For some context concerning opam: - Some opam packages rely on external (as in, non-OCaml) packages, such as pkg-config. Whenever this is the case, opam cannot install the packages directly (since they're not OCaml code). opam has a convention of creating a helper package "conf-<package name>" to detect if the external package is installed. It serves only to ensure the dependency is there, but it doesn't actually install the external package. - opam has a tool called "depext" which helps installing such external dependencies. This tool needs to be installed (via `opam install depext`). Then, typing `opam depext pkg-config` will make opam try to install the external package, usually by calling a native tool, such as apt, yum, or brew. You can do it yourself, the advantage of depext is that it knows (in most cases) the name of the package to be installed. If you install pkg-config yourself, or via `opam depext pkg-config`, you might be able to then install Frama-C. If so, please report, so that we will add "pkg-config" to the list of packages to be installed.

~0006555 NewUser (reporter) 2018-06-04 13:39	No...the problem is not solved. I have tried to reinstall all the things but now it couldn't install frame-c. See the new attached file.

~0006556 NewUser (reporter) 2018-06-04 14:04	And if try to upgrade to the latest frame-c version then still error occurs. see the attached upgrade file

~0006559 maroneze (administrator) 2018-06-05 10:20	Thanks for the log files. These are different and mostly unrelated issues, but in any way they are progressing. - In the first case (file from 13:39), Frama-C 17 Chlorine was not available, so you had a conflict related to Coq 8.8 (incompatible with all but the most recent Frama-C) and Frama-C, which prevented opam from finding a compatible version. - In the second case (file from 14:04), the specific error message is this one: # ocamlfind: Conflict with file: /Users/fauzia/.opam/system/lib/alt-ergo/altErgoLib.cmx I'm not familiar enough with macOS to know exactly what causes it, but it seems it could be related to trying to install a package that is somehow already installed (?). It is possible that by completely uninstalling alt-ergo (manually erasing its directory if necessary afterwards), and then trying to install it again, the issue could be resolved. I'll check with our macOS developers, but in any case, you can try to install alt-ergo on its own, sort any remaining issues, and then try to install Frama-C. It shouldn't be far now.

~0006560 maroneze (administrator) 2018-06-05 19:54	A macOS colleague recommended starting from scratch to avoid issues with leftover files: opam switch 4.06.1 opam init eval `opam config env` And then install Frama-C.

~0006561 NewUser (reporter) 2018-06-05 23:15	I have tried to reinstall and update all the things. But frama-c-gui was not working. There was some problem with gtk on my laptop so I tried this command gdk-pixbuf-query-loaders --update-cache and frama-c-gui is working fine now, accidentally. Thank you for all the help

~0006562 maroneze (administrator) 2018-06-06 08:31	Good to know it worked in the end! It's unfortunate though that it was that hard. We are working towards providing a Frama-C Homebrew package, which should make things easier in the future. It does require some dependencies to also exist as Homebrew packages though, which may slow things down.

~0006576 signoles (manager) 2018-07-11 15:34	Fixed in Frama-C Sulfur.

Notes

Date Modified	Username	Field	Change
Issue History
2018-05-23 12:14	NewUser	New Issue
2018-05-23 12:14	NewUser	File Added: Terminal Saved Output
2018-05-28 18:26	maroneze	Note Added: 0006552
2018-05-28 18:26	maroneze	Assigned To	=> maroneze
2018-05-28 18:26	maroneze	Status	new => assigned
2018-05-31 09:10	signoles	Category	Kernel => Opam
2018-06-04 13:37	NewUser	File Added: framaC_Output
2018-06-04 13:39	NewUser	Note Added: 0006555
2018-06-04 14:03	NewUser	File Added: Frama-CUpgrade
2018-06-04 14:04	NewUser	Note Added: 0006556
2018-06-05 10:20	maroneze	Note Added: 0006559
2018-06-05 19:54	maroneze	Note Added: 0006560
2018-06-05 23:15	NewUser	Note Added: 0006561
2018-06-06 08:31	maroneze	Note Added: 0006562
2018-06-06 08:31	maroneze	Status	assigned => resolved
2018-06-06 08:31	maroneze	Resolution	open => fixed
2018-07-11 15:33	signoles	Fixed in Version	=> Frama-C 16-Sulfur
2018-07-11 15:34	signoles	Status	resolved => closed
2018-07-11 15:34	signoles	Note Added: 0006576
2018-07-11 15:40	signoles	Fixed in Version	Frama-C 16-Sulfur => Frama-C 17-Chlorine

Issue History