--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on August 2014 ---
Hello list, 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 Any ideas? configure said: OCaml version : 4.01.0 OCaml library path : /usr/lib/ocaml OcamlGraph lib : found by ocamlfind Verbose make : no Inference of annotations : no Why3 support : yes Version : 0.83 Frama-C plugin : yes Frama-C version : Neon-20140301 GWhy : yes Coq support : yes Version : v8.1 (8.4pl4) Lib : /usr/local/lib/coq FP lib (Flocq) : no (Coq library Flocq/Core/Fcore.vo not found) FP lib (Float) : no (Coq library AllFloat.vo not found) PVS support : no Mizar support : no Other provers support : at run-time (use why-config to configure) With best regards Christoph