--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on October 2013 ---
Thanks Claude, that fixed that problem (I had to opam update). Now I am having a GTK problem ... why3ide --extra-config /Users/siegel/.opam/4.00.1/lib/why/lib/why/why3/why3.conf allZeroes.mlw [Info] Init the GTK interface...Fatal error: exception Gtk.Error("GtkMain.init: initialization failed ml_gtk_init: initialization failed") make: *** [why3ide] Error 2 [jessie] user error: Jessie subprocess failed: make -f allZeroes.makefile why3ide I guess there is some problem with lablgtk or gtksourceview2 or one of those packages. Or maybe there could be a PATH problem or some other environment variable? I installed gtksourceview2 with MacPorts; lablgtk is installed by opam. Anyone else have an issue like this? Thanks, Steve basic$ opam info lablgtk package: lablgtk version: 2.16.0 homepage: http://lablgtk.forge.ocamlcore.org/ depends: ocamlfind depopts: conf-gtksourceview | conf-gnomecanvas | lablgl installed-version: lablgtk.2.16.0 [system 4.00.1] available-version: 2.14.2-oasis8 description: Objective Caml interface to GTK+ If you have problems compiling this on MacOS X, try this using Homebrew: $ brew install gtk+ $ export PKG_CONFIG_PATH=/opt/X11/lib/pkgconfig $ opam install lablgtk basic$ ls ~/.opam/4.00.1/lib/ alt-ergo/ conf-gtksourceview/ labltk/ stublibs/ base-bigarray/ coq/ num/ threads/ base-threads/ dynlink/ num-top/ toplevel/ base-unix/ findlib/ ocaml/ unix/ bigarray/ findlib.conf ocamlbuild/ why/ camlp4/ frama-c/ ocamlfind/ why3/ camlp5/ graphics/ ocamlgraph/ zarith/ compiler-libs/ lablgtk/ stdlib/ conf-gnomecanvas/ lablgtk2/ str/ basic$ basic$ ls /opt/local/lib/gtk* /opt/local/lib/gtk-2.0: 2.10.0/ include/ modules/ /opt/local/lib/gtk-3.0: 3.0.0/ modules/ basic$ basic$ port info gtksourceview2 gtksourceview2 @2.10.5_6 (gnome) Variants: quartz, universal Description: GtkSourceView is a text widget that extends the standard gtk+ 2.x text widget GtkTextView. It improves GtkTextView by implementing syntax highlighting and other features typical of a source editor. This port contains version 2 of the GtkSourceView widget. Port GtkSourceView contains version 1 of the widget. Homepage: https://projects.gnome.org/gtksourceview/ Build Dependencies: intltool, pkgconfig, gtk-doc Library Dependencies: glib2, gettext, gtk2, libffi, libpixman, libpng, libxml2 Platforms: darwin License: LGPL-2.1+ Maintainers: micah.lerner at gmail.com, openmaintainer at macports.org basic$ On Oct 10, 2013, at 8:22 AM, Claude March? <Claude.Marche at inria.fr> wrote: > > > Le 09/10/2013 21:42, Stephen Siegel a ?crit : >> Then I was able to complete opam install frama-c and opam install why. >> However when I run "frama-c -jessie" I get "[kernel] user error: option >> `-jessie' is unknown." and jessie is not in my list of available plug-ins. >> >> why3config seems to be working normally. >> >> why2 is there: >> >> system$ why -version >> This is why version 2.32, compiled on Mon Apr 8 15:56:31 MDT 2013 >> >> Any ideas? > > > why 2.32 is compatible with Frama-C Oxygen but not fluorine. If Why find > a Frama-C version that is not compatible, it still compiles but does not > compile the plugin. > > The latest version of why in opam is 2.33, you should install this one, > I guess. Read carefully the output of compilation, in particular the > configure process at the beginning > > > Hope this helps, > > - claude > > > > -- > Claude March? | tel: +33 1 72 92 59 69 > INRIA Saclay - ?le-de-France | > Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ > F-91405 ORSAY Cedex | > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss