--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on October 2012 ---
Hello Boris, thank you for your follow-up. In the meantime , I have made considerably progress installing Frama-C Oxygen on OS X in general and Mountain Lion (OS X 10.8.2) in particular. Despite some challenges I found Oxygen much easier to install under OS X than previous versions of Frama-C! Here is how I made it work: I installed macports and and from there the following packages: sudo port install gtksourceview2 sudo port install lablgtk2 +gtksourceview2 (this one was tricky because macports mentions only a variant +gtksourceview (without the "2")) sudo ocaml-zarith ocaml-ocamlgraph (thanks for the hint to install zarith, Boris!) sudo port install graphviz sudo port install coq sudo port install djvulibre (I am not sure I really needed this package but I remembered that Pascal Cuoq had mention these fonts earlier) Then I installed the alt-ergo binary under /opt/local/bin. (I took the binary because configuring alt-ergo with prefix "/opt/local" would not find ocamlgraph and I was too impatient to examine this more closely.) Finally, I configured the Frama-C sources with prefix "/opt/local". "make" and "make install" worked fine. NOTE 1: Under Mountain Lion the installed binaries "frama-c-gui" and "frama-c" DO NOT WORK (segmentation fault). This is probably related to the bug of ocaml under Mountain Lion mentioned here: http://stackoverflow.com/questions/11762774/why-do-ocaml-binaries-crash-on-mac-os-x-10-8-mountain-lion The solution is to use the executables "frama-c-gui.byte" and "frama-c.byte". Under Lion (OS X 10.7) and Snow Leopard (OS X 10.6) the other binaries do work. NOTE 2: So far I have only tested Frama-C/WP. Regards Jens On 05.10.2012, at 13:56, Boris Yakobowski <boris at yakobowski.org> wrote: > Hi Jens > > Disclaimer : I'm not a mac expert at all (quite the contrary in fact), > but not many people currently use one here. > > On Wed, Sep 26, 2012 at 8:47 AM, Jens Gerlach > <jens.gerlach at first.fraunhofer.de> wrote: >> configure: gui: no, /opt/local/lib/ocaml/site-lib/lablgtk2/lablgtksourceview2.cmxa missing >> >> but there is >> /opt/local/lib/ocaml/site-lib/lablgtk2/lablgtksourceview.cmxa >> available (without the the final "2"). > > I'm afraid this might the binding for labgtksourceview1. If so, the > compilation of the GUI will fail later. Did you compile Lablgtk > yourself, or did you get a package? > >> Generating src/lib/my_bigint.ml >> sed: RE error: illegal byte sequence >> make: *** [src/lib/my_bigint.ml] Error 1 > > According to someone more knowledgeable than me, this is the result of > a not-so intelligent change from Apple in its sed implementation. > Google tells us that the encoding of the file on which sed is applied > must correspond to you C locale (see eg. > https://trac.macports.org/ticket/35421). A few possibilities : > - reencode src/lib/my_bigint.ml.bigint in utf-8 (assuming you use this locale) > - change your C locale to iso8859-1 (untested, should work) > - install Zarith :-) > > A last word of warning: the C linker in Mountain Lion do not cooperate > very well with the current OCaml compilers, so it is not clear that > compilation will succeed afterwards anyway. > > HTH, > > -- > Boris > > _______________________________________________ > 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 -- Dr.-Ing. Jens Gerlach Quality for Embedded Systems (QUEST) Phone +49 (0)30 6392 1841, jens.gerlach at first.fraunhofer.de Fraunhofer Institute for Open Communication Systems Fraunhofer FOKUS, Kekulestrasse 7, D 12489 Berlin, Germany