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] Oxygen on Mac OS X Mountain Lion
- Subject: [Frama-c-discuss] Oxygen on Mac OS X Mountain Lion
- From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
- Date: Sat, 6 Oct 2012 06:24:59 +0000
- In-reply-to: <CABbVA-AX-=oLGn_Zar-KfdY2Z3MkECUAyMj25PwOcyHEactY-w@mail.gmail.com>
- References: <250FB41C2DF1D14FA9D5971909DE405629278034@exdb00.first.fraunhofer.de> <CABbVA-AX-=oLGn_Zar-KfdY2Z3MkECUAyMj25PwOcyHEactY-w@mail.gmail.com>
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
- Follow-Ups:
- [Frama-c-discuss] Oxygen on Mac OS X Mountain Lion
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] Oxygen on Mac OS X Mountain Lion
- References:
- [Frama-c-discuss] Oxygen on Mac OS X Mountain Lion
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] Oxygen on Mac OS X Mountain Lion
- Prev by Date: [Frama-c-discuss] Some information on invariant needs
- Next by Date: [Frama-c-discuss] Oxygen on Mac OS X Mountain Lion
- Previous by thread: [Frama-c-discuss] Oxygen on Mac OS X Mountain Lion
- Next by thread: [Frama-c-discuss] Oxygen on Mac OS X Mountain Lion
- Index(es):