--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2014 ---
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