--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why-2.34 compile problem



Hello list,

update:

I got success by removing /usr/local/lib/why3 from previous installed why3.


> now I'm trying to get why-2.34 compiled but I ran into trouble:
> 
> 
> WHYLIB=lib bin/why.opt --no-pervasives -tc lib/why/prelude.why
> for f in lib/why/bool.why lib/why/integer.why lib/why/divisions.why 
> lib/why/real.why lib/why/arrays.why lib/why/jessie.why 
> lib/why/jessie_bitvectors.why lib/why/mybag.why lib/why/mix.why 
> lib/why/floats_common.why lib/why/floats_strict.why 
> lib/why/floats_full.why lib/why/floats_multi_rounding.why  ; do \
>                 WHYLIB=lib bin/why.opt -tc $f; \
>         done
> coqc -R /usr/local/lib/why3/coq Why3 -R lib/coq Why lib/coq/Jessie_memory_model.v
> File 
> "/home/crissi/frama-c/frama-c-Neon-20140301/why-2.34/lib/coq/Jessie_memory_model.v", 
> line 3, characters 0-23:
> Error: Compiled library Why3.BuiltIn.vo makes inconsistent assumptions 
> over
> library Coq.Program.Tactics
> make: *** [lib/coq/Jessie_memory_model.vo] Error 1

With best regards

Christoph