Anonymous | Login | Signup for a new account | 2019-12-10 03:24 CET | ![]() |
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-07-11 15:40 | ||||
Reporter | NewUser | ||||||||
Assigned To | maroneze | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | OS | Mac OS | OS Version | ||||||
Product Version | |||||||||
Target Version | Fixed in Version | Frama-C 17-Chlorine | |||||||
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 | ![]() 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$ ![]() 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` ![]() 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$ | ||||||||
![]() |
|
(0006552) maroneze (administrator) 2018-05-28 18:26 |
From the error messages, all I can see is that there seems to be an issue with pkg-config: either it is not installed, or not working properly
Did you run the command suggested at the end of the log? If so, what did that output? Please try:
opam depext conf-pkg-config.1.0
For some context concerning opam:
- Some opam packages rely on external (as in, non-OCaml) packages, such as pkg-config. Whenever this is the case, opam cannot install the packages directly (since they're not OCaml code). opam has a convention of creating a helper package "conf- |
(0006555) NewUser (reporter) 2018-06-04 13:39 |
No...the problem is not solved. I have tried to reinstall all the things but now it couldn't install frame-c. See the new attached file. |
(0006556) NewUser (reporter) 2018-06-04 14:04 |
And if try to upgrade to the latest frame-c version then still error occurs. see the attached upgrade file |
(0006559) maroneze (administrator) 2018-06-05 10:20 |
Thanks for the log files. These are different and mostly unrelated issues, but in any way they are progressing. - In the first case (file from 13:39), Frama-C 17 Chlorine was not available, so you had a conflict related to Coq 8.8 (incompatible with all but the most recent Frama-C) and Frama-C, which prevented opam from finding a compatible version. - In the second case (file from 14:04), the specific error message is this one: # ocamlfind: Conflict with file: /Users/fauzia/.opam/system/lib/alt-ergo/altErgoLib.cmx I'm not familiar enough with macOS to know exactly what causes it, but it seems it could be related to trying to install a package that is somehow already installed (?). It is possible that by completely uninstalling alt-ergo (manually erasing its directory if necessary afterwards), and then trying to install it again, the issue could be resolved. I'll check with our macOS developers, but in any case, you can try to install alt-ergo on its own, sort any remaining issues, and then try to install Frama-C. It shouldn't be far now. |
(0006560) maroneze (administrator) 2018-06-05 19:54 |
A macOS colleague recommended starting from scratch to avoid issues with leftover files: opam switch 4.06.1 opam init eval `opam config env` And then install Frama-C. |
(0006561) NewUser (reporter) 2018-06-05 23:15 |
I have tried to reinstall and update all the things. But frama-c-gui was not working. There was some problem with gtk on my laptop so I tried this command gdk-pixbuf-query-loaders --update-cache and frama-c-gui is working fine now, accidentally. Thank you for all the help |
(0006562) maroneze (administrator) 2018-06-06 08:31 |
Good to know it worked in the end! It's unfortunate though that it was that hard. We are working towards providing a Frama-C Homebrew package, which should make things easier in the future. It does require some dependencies to also exist as Homebrew packages though, which may slow things down. |
(0006576) signoles (manager) 2018-07-11 15:34 |
Fixed in Frama-C Sulfur. |
![]() |
|||
Date Modified | Username | Field | Change |
2018-05-23 12:14 | NewUser | New Issue | |
2018-05-23 12:14 | NewUser | File Added: Terminal Saved Output | |
2018-05-28 18:26 | maroneze | Note Added: 0006552 | |
2018-05-28 18:26 | maroneze | Assigned To | => maroneze |
2018-05-28 18:26 | maroneze | Status | new => assigned |
2018-05-31 09:10 | signoles | Category | Kernel => Opam |
2018-06-04 13:37 | NewUser | File Added: framaC_Output | |
2018-06-04 13:39 | NewUser | Note Added: 0006555 | |
2018-06-04 14:03 | NewUser | File Added: Frama-CUpgrade | |
2018-06-04 14:04 | NewUser | Note Added: 0006556 | |
2018-06-05 10:20 | maroneze | Note Added: 0006559 | |
2018-06-05 19:54 | maroneze | Note Added: 0006560 | |
2018-06-05 23:15 | NewUser | Note Added: 0006561 | |
2018-06-06 08:31 | maroneze | Note Added: 0006562 | |
2018-06-06 08:31 | maroneze | Status | assigned => resolved |
2018-06-06 08:31 | maroneze | Resolution | open => fixed |
2018-07-11 15:33 | signoles | Fixed in Version | => Frama-C 16-Sulfur |
2018-07-11 15:34 | signoles | Status | resolved => closed |
2018-07-11 15:34 | signoles | Note Added: 0006576 | |
2018-07-11 15:40 | signoles | Fixed in Version | Frama-C 16-Sulfur => Frama-C 17-Chlorine |
Copyright © 2000 - 2019 MantisBT Team |