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

> > coqc  -R lib/coq Why lib/coq/WhyFloats.v
> > File "/home/crissi/frama-c/why-2.34/lib/coq/WhyFloats.v", line 111,
> > characters 7-37:
> > Error: The reference Fcalc_digits.Zpower_gt_Zdigits was not found
> > in the current environment.
> > make: *** [lib/coq/WhyFloats.vo] Error 1

> You must have flocq 2.3.0.
I have it :)

> You'll need this patch:
> 
> --- lib/coq/WhyFloats.v.orig 2014-03-17 16:01:46.000000000 -0600
> +++ lib/coq/WhyFloats.v 2014-04-21 15:39:55.680771647 -0600
> @@ -108,7 +108,7 @@
>  generalize (Zeq_bool_eq _ _ H1). clear.
>  rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
>  intros H.
> -apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec)
> (Zpos m)).
> +apply (Fcore_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec)
> (Zpos m)).
>  revert H.
>  unfold FLT_exp.
>  generalize (Fcore_digits.Zdigits radix2 (Zpos m)).
Oh nice, that did the trick.


With best regards

Christoph