Attached Files |
-
Terminal Saved Output (3,508 bytes) 2018-05-23 12:14
Last login: Wed May 23 12:00:05 on ttys000
wlan022015:~ fauzia$ opam install frama-c
The following actions will be performed:
∗ install conf-pkg-config 1.0 [required by conf-gtksourceview]
∗ install conf-gnomecanvas 2 [required by frama-c]
∗ install conf-gtksourceview 2 [required by frama-c]
∗ install lablgtk 2.18.5 [required by frama-c]
∗ install ocamlgraph 1.8.8 [required by frama-c]
∗ install alt-ergo 2.2.0 [required by frama-c]
∗ install frama-c 20171101
Why3 can be used by the WP plug-in for running additional automatic solvers
Coq can be used with the WP plug-in for proving interactively proof obligations
Alt-Ergo Graphical Interface can be used by the WP plug-in
===== ∗ 7 =====
Do you want to continue ? [Y/n] Y
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
[alt-ergo] Archive in cache
[frama-c] Archive in cache
[lablgtk] Archive in cache
[ocamlgraph] Archive in cache
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
[ERROR] The compilation of conf-gnomecanvas failed at "pkg-config
libgnomecanvas-2.0".
[ERROR] The compilation of conf-pkg-config failed at "pkg-config --help".
#=== ERROR while installing conf-gnomecanvas.2 ================================#
# opam-version 1.2.2
# os darwin
# command pkg-config libgnomecanvas-2.0
# path /Users/fauzia/.opam/4.05.0/build/conf-gnomecanvas.2
# compiler 4.05.0
# exit-code 127
# env-file /Users/fauzia/.opam/4.05.0/build/conf-gnomecanvas.2/conf-gnomecanvas-17330-ffb3fd.env
# stdout-file /Users/fauzia/.opam/4.05.0/build/conf-gnomecanvas.2/conf-gnomecanvas-17330-ffb3fd.out
# stderr-file /Users/fauzia/.opam/4.05.0/build/conf-gnomecanvas.2/conf-gnomecanvas-17330-ffb3fd.err
#=== ERROR while installing conf-pkg-config.1.0 ===============================#
# opam-version 1.2.2
# os darwin
# command pkg-config --help
# path /Users/fauzia/.opam/4.05.0/build/conf-pkg-config.1.0
# compiler 4.05.0
# exit-code 127
# env-file /Users/fauzia/.opam/4.05.0/build/conf-pkg-config.1.0/conf-pkg-config-17330-05296d.env
# stdout-file /Users/fauzia/.opam/4.05.0/build/conf-pkg-config.1.0/conf-pkg-config-17330-05296d.out
# stderr-file /Users/fauzia/.opam/4.05.0/build/conf-pkg-config.1.0/conf-pkg-config-17330-05296d.err
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
The following actions were aborted
∗ install alt-ergo 2.2.0
∗ install conf-gtksourceview 2
∗ install frama-c 20171101
∗ install lablgtk 2.18.5
∗ install ocamlgraph 1.8.8
The following actions failed
∗ install conf-gnomecanvas 2
∗ install conf-pkg-config 1.0
No changes have been performed
=-=- conf-gnomecanvas.2 troobleshooting -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
=> This package relies on external (system) dependencies that may be missing.
`opam depext conf-gnomecanvas.2' may help you find the correct installation
for your system.
=-=- conf-pkg-config.1.0 troobleshooting =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
=> This package relies on external (system) dependencies that may be missing.
`opam depext conf-pkg-config.1.0' may help you find the correct installation
for your system.
wlan022015:~ fauzia$
-
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`
-
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$
|
---|