2021-02-27 10:47 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002375Frama-COpampublic2018-07-11 15:40
ReporterNewUser 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSMac OSOS Version
Product Version 
Target VersionFixed in VersionFrama-C 17-Chlorine 
Summary0002375: Issues while installation of Frama-C using OPAM
DescriptionI am having trouble while installation of frame-C on MacOS. I am trying to install it via OPAM.
I have installed all the dependencies also e.g
(brew install gmp gtk+ gtksourceview libgnomecanvas) but still it is not working.
please see the attached file for detailed error message
TagsNo tags attached.
Attached Files
  • ? file icon 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$ 
    
    ? file icon Terminal Saved Output (3,508 bytes) 2018-05-23 12:14 +
  • ? file icon 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`
    
    ? file icon framaC_Output (9,610 bytes) 2018-06-04 13:37 +
  • ? file icon 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$ 
    
    ? file icon Frama-CUpgrade (33,883 bytes) 2018-06-04 14:03 +

-Relationships
+Relationships

-Notes

~0006552

maroneze (administrator)

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)

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)

And if try to upgrade to the latest frame-c version then still error occurs.
see the attached upgrade file

~0006559

maroneze (administrator)

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)

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)

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)

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)

Fixed in Frama-C Sulfur.
+Notes

-Issue History
Date Modified Username Field Change
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