--- layout: fc_discuss_archives title: Message 7 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,

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