[why] Patch to work with flocq 2.0.0.
Jerry James
jjames at fedoraproject.org
Wed Jan 11 22:48:04 UTC 2012
commit 690799dc3f6c4bcd1176445c056a91da5d69eaf7
Author: Jerry James <loganjerry at gmail.com>
Date: Wed Jan 11 15:47:54 2012 -0700
Patch to work with flocq 2.0.0.
why-flocq2.patch | 510 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
why.spec | 11 +-
2 files changed, 519 insertions(+), 2 deletions(-)
---
diff --git a/why-flocq2.patch b/why-flocq2.patch
new file mode 100644
index 0000000..27dda9f
--- /dev/null
+++ b/why-flocq2.patch
@@ -0,0 +1,510 @@
+--- ./lib/coq/WhyFloats.v.orig 2011-10-24 09:21:06.000000000 -0600
++++ ./lib/coq/WhyFloats.v 2012-01-11 15:41:08.873131034 -0700
+@@ -19,17 +19,13 @@ Let emin := (3 - emax - prec)%Z.
+ Let fexp := FLT_exp emin prec.
+ Lemma Hprec': (0 < prec)%Z. revert Hprec. now case Zlt_bool_spec. Qed.
+ Lemma Hemax': (prec < emax)%Z. revert Hemax. now case Zlt_bool_spec. Qed.
+-Let binary_round_correct := binary_round_sign_shl_correct prec emax Hprec' Hemax'.
++Lemma fexp': Valid_exp fexp. apply FLT_exp_valid. apply Hprec'. Qed.
+
+ Definition r_to_sd rnd x : binary_float prec emax :=
+ let r := round radix2 fexp (round_mode rnd) x in
+ let m := Ztrunc (scaled_mantissa radix2 fexp r) in
+- let e := canonic_exponent radix2 fexp r in
+- match m with
+- | Z0 => B754_zero prec emax false
+- | Zpos m => FF2B _ _ _ (proj1 (binary_round_correct rnd false m e))
+- | Zneg m => FF2B _ _ _ (proj1 (binary_round_correct rnd true m e))
+- end.
++ let e := canonic_exp radix2 fexp r in
++ binary_normalize prec emax Hprec' Hemax' rnd m e false.
+
+ Lemma is_finite_FF2B :
+ forall f H,
+@@ -49,59 +45,19 @@ Theorem r_to_sd_correct :
+ (Rabs r < bpow radix2 emax)%R ->
+ is_finite prec emax (r_to_sd rnd x) = true /\
+ r_to_sd rnd x = r :>R.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros rnd x r Bx.
+ unfold r_to_sd. fold r.
+-assert (Gx: generic_format radix2 fexp r).
+-apply generic_format_round.
+-apply FLT_exp_correct.
+-exact Hprec'.
+-assert (Hr: Z2R (Ztrunc (scaled_mantissa radix2 fexp r)) = scaled_mantissa radix2 fexp r).
+-apply sym_eq.
+-now apply scaled_mantissa_generic.
+-revert Hr.
+-case_eq (Ztrunc (scaled_mantissa radix2 fexp r)).
+-(* *)
+-intros _ Hx.
+-repeat split.
+-apply Rmult_eq_reg_r with (bpow radix2 (- canonic_exponent radix2 fexp r)).
+-now rewrite Rmult_0_l.
+-apply Rgt_not_eq.
+-apply bpow_gt_0.
+-(* *)
+-intros p Hp Hx.
+-case binary_round_correct ; intros Hv.
+-unfold F2R, Fnum, Fexp, cond_Zopp.
+-rewrite Hx, scaled_mantissa_bpow.
+-rewrite round_generic with (1 := Gx).
+-rewrite Rlt_bool_true with (1 := Bx).
+-intros H.
+-split.
+-rewrite is_finite_FF2B.
+-revert H.
+-assert (0 <> r)%R.
+-intros H.
+-rewrite <- H, scaled_mantissa_0 in Hx.
+-now apply (Z2R_neq 0 (Zpos p)).
+-now case binary_round_sign_shl.
+-now rewrite B2R_FF2B.
+-(* *)
+-intros p Hp Hx.
+-case binary_round_correct ; intros Hv.
+-unfold F2R, Fnum, Fexp, cond_Zopp, Zopp.
+-rewrite Hx, scaled_mantissa_bpow.
+-rewrite round_generic with (1 := Gx).
++generalize (binary_normalize_correct prec emax Hprec' Hemax' rnd (Ztrunc (scaled_mantissa radix2 fexp r)) (canonic_exp radix2 fexp r) false).
++unfold r.
++elim generic_format_round...
++fold emin r.
++rewrite round_generic...
+ rewrite Rlt_bool_true with (1 := Bx).
+-intros H.
+-split.
+-rewrite is_finite_FF2B.
+-revert H.
+-assert (0 <> r)%R.
+-intros H.
+-rewrite <- H, scaled_mantissa_0 in Hx.
+-now apply (Z2R_neq 0 (Zneg p)).
+-now case binary_round_sign_shl.
+-now rewrite B2R_FF2B.
++now split.
++apply generic_format_round...
++apply fexp'.
++apply fexp'.
+ Qed.
+
+ Theorem r_to_sd_format :
+@@ -109,15 +65,14 @@ Theorem r_to_sd_format :
+ FLT_format radix2 emin prec x ->
+ (Rabs x < bpow radix2 emax)%R ->
+ r_to_sd rnd x = x :>R.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros rnd x Fx Bx.
+ assert (Gx: generic_format radix2 fexp x).
+-apply -> FLT_format_generic.
++apply generic_format_FLT.
+ apply Fx.
+-exact Hprec'.
+-pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (1 := Gx).
++pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (2 := Gx)...
+ refine (proj2 (r_to_sd_correct _ _ _)).
+-now rewrite round_generic with (1 := Gx).
++rewrite round_generic...
+ Qed.
+
+ End r_to_sd.
+@@ -152,10 +107,10 @@ rewrite <- Zsucc_pred.
+ generalize (Zeq_bool_eq _ _ H1). clear.
+ rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
+ intros H.
+-apply (Fcalc_digits.Zpower_gt_digits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
++apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) (Zpos m)).
+ revert H.
+ unfold FLT_exp.
+-generalize (Fcalc_digits.digits Fcalc_digits.radix2 (Zpos m)).
++generalize (Fcore_digits.Zdigits Fcalc_digits.radix2 (Zpos m)).
+ intros ; zify ; omega.
+ apply bpow_le.
+ now apply Zle_bool_imp_le.
+@@ -172,6 +127,23 @@ Definition rnd_of_mode (m:mode) :=
+
+ (** Single precision *)
+
++Definition binary32 := binary_float 24 128.
++
++Let Hprec32 : (0 < 24)%Z.
++apply refl_equal.
++Qed.
++
++Let Hprec32_emax : (24 < 128)%Z.
++apply refl_equal.
++Qed.
++
++Definition b32_opp := Bopp 24 128.
++Definition b32_plus := Bplus _ _ Hprec32 Hprec32_emax.
++Definition b32_minus := Bminus _ _ Hprec32 Hprec32_emax.
++Definition b32_mult := Bmult _ _ Hprec32 Hprec32_emax.
++Definition b32_div := Bdiv _ _ Hprec32 Hprec32_emax.
++Definition b32_sqrt := Bsqrt _ _ Hprec32 Hprec32_emax.
++
+ Record single : Set := mk_single {
+ single_float : binary32;
+ single_value := (single_float : R);
+@@ -229,12 +201,12 @@ Theorem bounded_real_no_overflow_single
+ forall m x,
+ (Rabs x <= max_single)%R ->
+ no_overflow_single m x.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m x Hx.
+ apply Rabs_le.
+ assert (generic_format radix2 (FLT_exp (-149) 24) max_single).
+-apply generic_format_canonic_exponent.
+-unfold canonic_exponent.
++apply generic_format_F2R.
++unfold canonic_exp.
+ rewrite ln_beta_F2R. 2: easy.
+ rewrite (ln_beta_unique _ _ 24).
+ easy.
+@@ -245,31 +217,40 @@ now apply Z2R_lt.
+ generalize (Rabs_le_inv _ _ Hx).
+ split.
+ erewrite <- round_generic with (x := Ropp max_single).
+-apply round_monotone with (2 := proj1 H0).
+-now apply FLT_exp_correct.
++unfold round_single.
++apply round_le...
++apply FLT_exp_valid. easy.
++easy.
++apply valid_rnd_round_mode.
+ now apply generic_format_opp.
+-rewrite <- round_generic with (rnd := round_mode (rnd_of_mode m)) (1 := H).
+-apply round_monotone with (2 := proj2 H0).
+-now apply FLT_exp_correct.
++unfold round_single.
++apply round_le_generic...
++apply FLT_exp_valid.
++apply Hprec'...
++easy.
+ Qed.
+
+ Theorem round_single_monotonic :
+ forall m x y, (x <= y)%R ->
+ (round_single m x <= round_single m y)%R.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m x y Hxy.
+-apply round_monotone with (2 := Hxy).
+-now apply FLT_exp_correct.
++unfold round_single.
++apply round_le...
++apply FLT_exp_valid.
++apply Hprec'...
+ Qed.
+
+ Theorem round_single_idempotent :
+ forall m1 m2 x,
+ round_single m1 (round_single m2 x) = round_single m2 x.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m1 m2 x.
+ apply round_generic.
+-apply generic_format_round.
+-now apply FLT_exp_correct.
++apply valid_rnd_round_mode.
++apply generic_format_round...
++apply FLT_exp_valid.
++apply Hprec'...
+ Qed.
+
+ Theorem round_down_single_neg :
+@@ -295,8 +276,9 @@ Theorem round_single_down_le :
+ (round_single down x <= x)%R.
+ Proof.
+ intros x.
+-eapply round_DN_pt.
+-now apply FLT_exp_correct.
++eapply round_DN_pt...
++apply FLT_exp_valid.
++apply Hprec'. easy.
+ Qed.
+
+ Theorem round_up_single_ge :
+@@ -305,12 +287,30 @@ Theorem round_up_single_ge :
+ Proof.
+ intros x.
+ apply Rle_ge.
+-eapply round_UP_pt.
+-now apply FLT_exp_correct.
++eapply round_UP_pt...
++apply FLT_exp_valid.
++apply Hprec'. easy.
+ Qed.
+
+ (** Double precision *)
+
++Definition binary64 := binary_float 53 1024.
++
++Let Hprec64 : (0 < 53)%Z.
++apply refl_equal.
++Qed.
++
++Let Hprec64_emax : (53 < 1024)%Z.
++apply refl_equal.
++Qed.
++
++Definition b64_opp := Bopp 53 1024.
++Definition b64_plus := Bplus _ _ Hprec64 Hprec64_emax.
++Definition b64_minus := Bminus _ _ Hprec64 Hprec64_emax.
++Definition b64_mult := Bmult _ _ Hprec64 Hprec64_emax.
++Definition b64_div := Bdiv _ _ Hprec64 Hprec64_emax.
++Definition b64_sqrt := Bsqrt _ _ Hprec64 Hprec64_emax.
++
+ Record double : Set := mk_double {
+ double_float : binary64;
+ double_value := (double_float : R);
+@@ -368,12 +368,12 @@ Theorem bounded_real_no_overflow_double
+ forall m x,
+ (Rabs x <= max_double)%R ->
+ no_overflow_double m x.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m x Hx.
+ apply Rabs_le.
+ assert (generic_format radix2 (FLT_exp (-1074) 53) max_double).
+-apply generic_format_canonic_exponent.
+-unfold canonic_exponent.
++apply generic_format_F2R.
++unfold canonic_exp.
+ rewrite ln_beta_F2R. 2: easy.
+ rewrite (ln_beta_unique _ _ 53).
+ easy.
+@@ -384,31 +384,40 @@ now apply Z2R_lt.
+ generalize (Rabs_le_inv _ _ Hx).
+ split.
+ erewrite <- round_generic with (x := Ropp max_double).
+-apply round_monotone with (2 := proj1 H0).
+-now apply FLT_exp_correct.
++unfold round_double.
++apply round_le...
++apply FLT_exp_valid. easy.
++easy.
++apply valid_rnd_round_mode.
+ now apply generic_format_opp.
+-rewrite <- round_generic with (rnd := round_mode (rnd_of_mode m)) (1 := H).
+-apply round_monotone with (2 := proj2 H0).
+-now apply FLT_exp_correct.
++unfold round_double.
++apply round_le_generic...
++apply FLT_exp_valid.
++apply Hprec'...
++easy.
+ Qed.
+
+ Theorem round_double_monotonic :
+ forall m x y, (x <= y)%R ->
+ (round_double m x <= round_double m y)%R.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m x y Hxy.
+-apply round_monotone with (2 := Hxy).
+-now apply FLT_exp_correct.
++unfold round_double.
++apply round_le...
++apply FLT_exp_valid.
++apply Hprec'...
+ Qed.
+
+ Theorem round_double_idempotent :
+ forall m1 m2 x,
+ round_double m1 (round_double m2 x) = round_double m2 x.
+-Proof.
++Proof with auto with typeclass_instances.
+ intros m1 m2 x.
+ apply round_generic.
+-apply generic_format_round.
+-now apply FLT_exp_correct.
++apply valid_rnd_round_mode.
++apply generic_format_round...
++apply FLT_exp_valid.
++apply Hprec'...
+ Qed.
+
+ Theorem round_down_double_neg :
+@@ -434,8 +443,9 @@ Theorem round_double_down_le :
+ (round_double down x <= x)%R.
+ Proof.
+ intros x.
+-eapply round_DN_pt.
+-now apply FLT_exp_correct.
++eapply round_DN_pt...
++apply FLT_exp_valid.
++apply Hprec'. easy.
+ Qed.
+
+ Theorem round_up_double_ge :
+@@ -444,8 +454,9 @@ Theorem round_up_double_ge :
+ Proof.
+ intros x.
+ apply Rle_ge.
+-eapply round_UP_pt.
+-now apply FLT_exp_correct.
++eapply round_UP_pt...
++apply FLT_exp_valid.
++apply Hprec'. easy.
+ Qed.
+
+ (** Quad precision *)
+@@ -566,8 +577,8 @@ unfold F2R. simpl.
+ split.
+ now rewrite Rmult_1_r.
+ now split.
+-apply <- FLT_format_generic.
+-2: easy.
++apply FLT_format_generic.
++apply Hprec'. easy.
+ change 2%Z with (radix_val radix2) in Bz.
+ destruct z as [|z|z] ; unfold Zabs in Bz.
+ apply generic_format_0.
+--- ./lib/coq/WhyFloatsStrict.v.orig 2011-10-24 09:21:06.000000000 -0600
++++ ./lib/coq/WhyFloatsStrict.v 2012-01-11 15:42:11.453663887 -0700
+@@ -155,30 +155,13 @@ repeat split.
+ exact H2.
+ Qed.
+
+-Axiom Bplus_correct : (* the statement from Flocq 1.4 is not strong enough;
+- the axiom can be removed once the library is converted to Flocq 2.0 *)
+- forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
+- (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
+- is_finite prec emax x = true ->
+- is_finite prec emax y = true ->
+- if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
+- (B2R prec emax x + B2R prec emax y))) (bpow radix2 emax)
+- then
+- B2R prec emax (Bplus prec emax Hprec Hmax m x y) =
+- round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x + B2R prec emax y) /\
+- is_finite prec emax (Bplus prec emax Hprec Hmax m x y) = true
+- else
+- B2FF prec emax (Bplus prec emax Hprec Hmax m x y) =
+- binary_overflow prec emax m (Bsign prec emax x) /\
+- Bsign prec emax x = Bsign prec emax y.
+-
+ Lemma add_single_specification :
+ forall m (x y : single),
+ no_overflow_single m (single_value x + single_value y) ->
+ exists z, add_single_post m x y z.
+ Proof.
+ intros m x y Br.
+-refine (_ (Bplus_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y)
++refine (_ (Bplus_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y)
+ (single_finite x) (single_finite y))).
+ rewrite Rlt_bool_true.
+ 2: now apply no_overflow_single_bounded.
+@@ -189,27 +172,13 @@ repeat split.
+ exact H1.
+ Qed.
+
+-Axiom Bmult_correct : (* the statement from Flocq 1.4 is not strong enough;
+- the axiom can be removed once the library is converted to Flocq 2.0 *)
+- forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
+- (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
+- if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
+- (B2R prec emax x * B2R prec emax y))) (bpow radix2 emax)
+- then
+- B2R prec emax (Bmult prec emax Hprec Hmax m x y) =
+- round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x * B2R prec emax y) /\
+- is_finite prec emax (Bmult prec emax Hprec Hmax m x y) = andb (is_finite prec emax x) (is_finite prec emax y)
+- else
+- B2FF prec emax (Bmult prec emax Hprec Hmax m x y) =
+- binary_overflow prec emax m (xorb (Bsign prec emax x) (Bsign prec emax y)).
+-
+ Lemma mul_single_specification :
+ forall m (x y : single),
+ no_overflow_single m (single_value x * single_value y) ->
+ exists z, mul_single_post m x y z.
+ Proof.
+ intros m x y Br.
+-refine (_ (Bmult_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y))).
++refine (_ (Bmult_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y))).
+ rewrite Rlt_bool_true.
+ 2: now apply no_overflow_single_bounded.
+ fold b32_mult.
+@@ -220,28 +189,13 @@ repeat split.
+ exact H1.
+ Qed.
+
+-Axiom Bdiv_correct : (* the statement from Flocq 1.4 is not strong enough;
+- the axiom can be removed once the library is converted to Flocq 2.0 *)
+- forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
+- (m : Fappli_IEEE.mode) (x y : binary_float prec emax),
+- B2R prec emax y <> 0%R ->
+- if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m)
+- (B2R prec emax x / B2R prec emax y))) (bpow radix2 emax)
+- then
+- B2R prec emax (Bdiv prec emax Hprec Hmax m x y) =
+- round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (B2R prec emax x / B2R prec emax y) /\
+- is_finite prec emax (Bdiv prec emax Hprec Hmax m x y) = is_finite prec emax x
+- else
+- B2FF prec emax (Bdiv prec emax Hprec Hmax m x y) =
+- binary_overflow prec emax m (xorb (Bsign prec emax x) (Bsign prec emax y)).
+-
+ Lemma div_single_specification :
+ forall m (x y : single), single_value y <> R0 ->
+ no_overflow_single m (single_value x / single_value y) ->
+ exists z, div_single_post m x y z.
+ Proof.
+ intros m x y Zy Br.
+-refine (_ (Bdiv_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x) (single_float y) Zy)).
++refine (_ (Bdiv_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x) (single_float y) Zy)).
+ rewrite Rlt_bool_true.
+ 2: now apply no_overflow_single_bounded.
+ fold b32_div.
+@@ -252,20 +206,12 @@ repeat split.
+ exact H1.
+ Qed.
+
+-Axiom Bsqrt_correct : (* the statement from Flocq 1.4 is not strong enough;
+- the axiom can be removed once the library is converted to Flocq 2.0 *)
+- forall (prec emax : Z) (Hprec : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
+- (m : Fappli_IEEE.mode) (x : binary_float prec emax),
+- B2R prec emax (Bsqrt prec emax Hprec Hmax m x) =
+- round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode m) (sqrt (B2R prec emax x)) /\
+- is_finite prec emax (Bsqrt prec emax Hprec Hmax m x) = match x with B754_zero _ => true | B754_finite false _ _ _ => true | _ => false end.
+-
+ Lemma sqrt_single_specification :
+ forall m (x : single), Rle 0 (single_value x) ->
+ exists z, sqrt_single_post m x z.
+ Proof.
+ intros m x Zx.
+-refine (_ (Bsqrt_correct 24 128 (refl_equal Lt) (refl_equal Lt) (rnd_of_mode m) (single_float x))).
++refine (_ (Bsqrt_correct 24 128 Hprec32 Hprec32_emax (rnd_of_mode m) (single_float x))).
+ fold b32_sqrt.
+ intros (H1, H2).
+ assert (is_finite 24 128 (b32_sqrt (rnd_of_mode m) (single_float x)) = true).
+--- ./lib/coq/JessieGappa.v.orig 2011-10-24 09:21:06.000000000 -0600
++++ ./lib/coq/JessieGappa.v 2012-01-11 15:41:08.874131235 -0700
+@@ -571,7 +571,7 @@ unfold min_gen_float, min_float2.
+ case F ; apply bpow_gt_0.
+ rewrite <- round_of_min_gen with F m.
+ revert Bx1.
+-case F ; apply round_monotone ; now apply FLT_exp_correct.
++case F ; apply round_le...
+ Save.
+
+ Lemma negative_constant : forall f m x,
+@@ -592,7 +592,7 @@ case F ; apply bpow_ge_0.
+ apply Rle_lt_trans with (- min_gen_float F)%R.
+ rewrite <- round_of_opp_min_gen with F m.
+ revert Bx2.
+-case F ; apply round_monotone ; now apply FLT_exp_correct.
++case F ; apply round_le...
+ apply Ropp_lt_gt_0_contravar.
+ unfold min_gen_float, min_float2.
+ case F ; apply bpow_gt_0.
+@@ -602,7 +602,7 @@ Lemma round_increasing: forall f m x y,
+ (x <= y)%R -> (round_float f m x <= round_float f m y)%R.
+ Proof.
+ intros F m x y.
+-case F ; apply round_monotone ; now apply FLT_exp_correct.
++case F ; apply round_le...
+ Save.
+
+ Lemma round_greater_min: forall f m x,
diff --git a/why.spec b/why.spec
index be67c73..1ff7d47 100644
--- a/why.spec
+++ b/why.spec
@@ -20,7 +20,7 @@
Name: why
Version: 2.30
-Release: 4%{?dist}
+Release: 5%{?dist}
Summary: Software verification platform
Group: Applications/Engineering
@@ -55,9 +55,12 @@ Patch0: gwhy-2.26.patch
Patch1: why-2.30-Makefile.in.patch
# This patch fixes some mildly bitrotted APRON support code.
-# It will be sent upstream.
+# Applied upstream.
Patch2: why-apron.patch
+# This patch updates the flocq usage for flocq 2.0.0. It will be sent upstream.
+Patch3: why-flocq2.patch
+
BuildRequires: auto-destdir
BuildRequires: cvc3
BuildRequires: desktop-file-utils
@@ -216,6 +219,7 @@ based on Why, including various automated and interactive provers.
%patch0
%patch1
%patch2
+%patch3
cp -p %SOURCE1 %SOURCE2 %SOURCE6 %SOURCE7 ./
@@ -434,6 +438,9 @@ diff -u min.why min_why.why.result # Show differences from correct result.
%changelog
+* Wed Jan 11 2012 Jerry James <loganjerry at gmail.com> - 2.30-5
+- Patch to work with flocq 2.0.0
+
* Tue Dec 27 2011 Jerry James <loganjerry at gmail.com> - 2.30-4
- Rebuild for coq 8.3pl3
More information about the scm-commits
mailing list