| Anonymous | Login | Signup for a new account | 2018-06-20 22:27 CEST |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
| 0002375 | Frama-C | Opam | public | 2018-05-23 12:14 | 2018-06-06 08:31 | ||||
| Reporter | NewUser | ||||||||
| Assigned To | maroneze | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | resolved | Resolution | fixed | ||||||
| Platform | OS | Mac OS | OS Version | ||||||
| Product Version | |||||||||
| Target Version | Fixed in Version | ||||||||
| Summary | 0002375: Issues while installation of Frama-C using OPAM | ||||||||
| Description | I 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 | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |  Terminal Saved Output [^] (3,508 bytes) 2018-05-23 12:14 [Show Content] [Hide Content]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$
framaC_Output [^] (9,610 bytes) 2018-06-04 13:37 [Show Content] [Hide Content]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`
Frama-CUpgrade [^] (33,883 bytes) 2018-06-04 14:03 [Show Content] [Hide Content]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$
| ||||||||
 Relationships |
|
 Relationships |
|
Notes |
|
|
(0006552) maroneze (developer) 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 (developer) 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 (developer) 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 (developer) 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. |
|
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 |
|
Issue History |
| Copyright © 2000 - 2018 MantisBT Team |
|