--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Mac install



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