--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on February 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Why-discuss] Generate Coq file using Frama-c / Why



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