Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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