--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on February 2010 ---
Hello, I tried to compile the Why 2.23 distribution, following Pascal recommendations and I got an error after executing "make" ... Ocamlopt src/hypotheses_filtering.ml File "src/hypotheses_filtering.ml", line 1, characters 0-1: Error: The files src/ident.cmi and /opt/local/lib/ocaml/ocamlgraph/graph.cmi make inconsistent assumptions over interface Buffer make: *** [src/hypotheses_filtering.cmx] Error 2 It seems that something is not correctly installed or there is some inconsistency in my ocaml distribution, which is 3.11.2. Could you help please? Best regards, B?rbara A 2010/02/19, ?s 15:03, Pascal Cuoq escreveu: > Hello, > >> Anyway, I will try to follow the instructions from Pascal. > > If you mean "install a version of Why where Coq V8 has been detected, > compiled with 64-bit OCaml 3.11.2 for Snow Leopard, your best bet to > avoid interference between the two is to overwrite the Why provided in > the Frama-C binary package. > > Compile with: > export PATH=/usr/local/Frama-C_Be/bin:$PATH > ./configure --prefix=/usr/local/Frama-C_Be/ > make > sudo make install > > Note that there is an OCaml compiler in the Frama-C package, but it > was compiled for Leopard and I don't recommend using it. It is better > to use a Snow Leopard OCaml compiler. > > Pascal > > > _______________________________________________ > 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