Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package flocq for openSUSE:Factory checked in at 2023-03-29 23:28:36 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/flocq (Old) and /work/SRC/openSUSE:Factory/.flocq.new.31432 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "flocq" Wed Mar 29 23:28:36 2023 rev:5 rq:1075337 version:4.1.1 Changes: -------- --- /work/SRC/openSUSE:Factory/flocq/flocq.changes 2023-01-27 10:27:30.879111268 +0100 +++ /work/SRC/openSUSE:Factory/.flocq.new.31432/flocq.changes 2023-03-29 23:28:40.111927850 +0200 @@ -1,0 +2,6 @@ +Wed Mar 29 18:55:13 UTC 2023 - Aaron Puchert <[email protected]> + +- Update to version 4.1.1. + * Ensured compatibility from Coq 8.12 to 8.17. + +------------------------------------------------------------------- Old: ---- flocq-4.1.0.tar.gz New: ---- flocq-4.1.1.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ flocq.spec ++++++ --- /var/tmp/diff_new_pack.qEijKM/_old 2023-03-29 23:28:40.627930607 +0200 +++ /var/tmp/diff_new_pack.qEijKM/_new 2023-03-29 23:28:40.631930628 +0200 @@ -19,7 +19,7 @@ Name: flocq -Version: 4.1.0 +Version: 4.1.1 Release: 0 Summary: Formalization of floating point numbers for Coq Group: Productivity/Scientific/Math ++++++ flocq-4.1.0.tar.gz -> flocq-4.1.1.tar.gz ++++++ ++++ 2767 lines of diff (skipped) ++++ retrying with extended exclude list diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' --exclude Makefile.in --exclude configure --exclude config.guess --exclude '*.pot' --exclude mkinstalldirs --exclude aclocal.m4 --exclude config.sub --exclude depcomp --exclude install-sh --exclude ltmain.sh old/flocq-4.1.0/NEWS.md new/flocq-4.1.1/NEWS.md --- old/flocq-4.1.0/NEWS.md 2022-04-28 13:47:40.000000000 +0200 +++ new/flocq-4.1.1/NEWS.md 2023-02-24 16:37:25.000000000 +0100 @@ -1,3 +1,8 @@ +Version 4.1.1 +------------- + +* ensured compatibility from Coq 8.12 to 8.17 + Version 4.1.0 ------------- diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' --exclude Makefile.in --exclude configure --exclude config.guess --exclude '*.pot' --exclude mkinstalldirs --exclude aclocal.m4 --exclude config.sub --exclude depcomp --exclude install-sh --exclude ltmain.sh old/flocq-4.1.0/Remakefile.in new/flocq-4.1.1/Remakefile.in --- old/flocq-4.1.0/Remakefile.in 2022-04-28 13:47:40.000000000 +0200 +++ new/flocq-4.1.1/Remakefile.in 2023-02-24 16:37:25.000000000 +0100 @@ -74,11 +74,11 @@ %.vo: %.v | src/IEEE754/Int63Compat.v @COQDEP@ -R src Flocq $< | @REMAKE@ -r $@ - @COQC@ @COQEXTRAFLAGS@ -R src Flocq $< + @COQC@ @COQEXTRAFLAGS@ -q -R src Flocq $< examples/%.vo: examples/%.v @COQDEP@ $(LOCAL) -R examples FlocqEx $< | @REMAKE@ -r $@ - @COQC@ $(LOCAL) -R examples FlocqEx $< + @COQC@ $(LOCAL) -q -R examples FlocqEx $< $(EOBJS): LOCAL = -R src Flocq diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' --exclude Makefile.in --exclude configure --exclude config.guess --exclude '*.pot' --exclude mkinstalldirs --exclude aclocal.m4 --exclude config.sub --exclude depcomp --exclude install-sh --exclude ltmain.sh old/flocq-4.1.0/configure.in new/flocq-4.1.1/configure.in --- old/flocq-4.1.0/configure.in 2022-04-28 13:47:40.000000000 +0200 +++ new/flocq-4.1.1/configure.in 2023-02-24 16:37:25.000000000 +0100 @@ -1,4 +1,4 @@ -AC_INIT([Flocq], [4.1.0], +AC_INIT([Flocq], [4.1.1], [Sylvie Boldo <[email protected]>, Guillaume Melquiond <[email protected]>], [flocq]) diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' --exclude Makefile.in --exclude configure --exclude config.guess --exclude '*.pot' --exclude mkinstalldirs --exclude aclocal.m4 --exclude config.sub --exclude depcomp --exclude install-sh --exclude ltmain.sh old/flocq-4.1.0/examples/Double_rounding_odd_radix.v new/flocq-4.1.1/examples/Double_rounding_odd_radix.v --- old/flocq-4.1.0/examples/Double_rounding_odd_radix.v 2022-04-28 13:47:40.000000000 +0200 +++ new/flocq-4.1.1/examples/Double_rounding_odd_radix.v 2023-02-24 16:37:25.000000000 +0100 @@ -416,7 +416,7 @@ apply (Rmult_lt_reg_r (bpow ex1)); [now apply bpow_gt_0|]; bpow_simplify. assert (H : x <= rx1c); [now apply round_UP_pt|]. destruct H as [H|H]; [exact H|]. - casetype False; apply NF1x. + exfalso; apply NF1x. unfold generic_format, F2R, scaled_mantissa, cexp; simpl; fold ex1. rewrite Ztrunc_floor; [|now apply Rmult_le_pos;[apply Rlt_le|apply bpow_ge_0]]. @@ -667,7 +667,7 @@ apply IZR_le. destruct (Zle_or_lt beta 2) as [Hb2|Hb2]; [|lia]. assert (Hbeta' : beta = 2%Z :> Z); [now apply Zle_antisym|]. - casetype False. + exfalso. rewrite <- Zodd_ex_iff in Obeta. apply (Zodd_not_Zeven _ Obeta). now rewrite Hbeta'. @@ -2173,7 +2173,7 @@ apply IZR_le. destruct (Zle_or_lt beta 2) as [Hb2|Hb2]; [|lia]. assert (Hbeta' : beta = 2%Z :> Z); [now apply Zle_antisym|]. - casetype False. + exfalso. rewrite <- Zodd_ex_iff in Obeta. apply (Zodd_not_Zeven _ Obeta). now rewrite Hbeta'. @@ -2229,7 +2229,7 @@ apply generic_format_opp in Fy. now apply round_round_div_beta_odd_rna_aux. + (* y = 0 *) - now casetype False; apply Nzy. + now exfalso; apply Nzy. + (* y > 0 *) rewrite <- (Ropp_involutive x). rewrite Ropp_div. @@ -2256,7 +2256,7 @@ apply generic_format_opp in Fy. now apply round_round_div_beta_odd_rna_aux. + (* y = 0 *) - now casetype False; apply Nzy. + now exfalso; apply Nzy. + (* y > 0 *) now apply round_round_div_beta_odd_rna_aux. Qed. diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' --exclude Makefile.in --exclude configure --exclude config.guess --exclude '*.pot' --exclude mkinstalldirs --exclude aclocal.m4 --exclude config.sub --exclude depcomp --exclude install-sh --exclude ltmain.sh old/flocq-4.1.0/src/Core/Raux.v new/flocq-4.1.1/src/Core/Raux.v --- old/flocq-4.1.0/src/Core/Raux.v 2022-04-28 13:47:40.000000000 +0200 +++ new/flocq-4.1.1/src/Core/Raux.v 2023-02-24 16:37:25.000000000 +0100 @@ -214,7 +214,7 @@ unfold sqrt. destruct Rcase_abs. + reflexivity. - + casetype False. + + exfalso. now apply Nzx, Rle_antisym; [|apply Rge_le]. Qed. @@ -2355,7 +2355,7 @@ apply archimed. destruct (HP N) as [PN|PN]. now split. -elimtype False. +exfalso. refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _). intros x [y [[Py ->]|[_ ->]]]. destruct (eq_nat_dec y N) as [HyN|HyN]. diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' --exclude Makefile.in --exclude configure --exclude config.guess --exclude '*.pot' --exclude mkinstalldirs --exclude aclocal.m4 --exclude config.sub --exclude depcomp --exclude install-sh --exclude ltmain.sh old/flocq-4.1.0/src/Pff/Pff.v new/flocq-4.1.1/src/Pff/Pff.v --- old/flocq-4.1.0/src/Pff/Pff.v 2022-04-28 13:47:40.000000000 +0200 +++ new/flocq-4.1.1/src/Pff/Pff.v 2023-02-24 16:37:25.000000000 +0100 @@ -1710,6 +1710,7 @@ Theorem FboundedShiftLess : forall (b : Fbound) (f : float) (n m : nat), m <= n -> Fbounded b (Fshift radix n f) -> Fbounded b (Fshift radix m f). +Proof. intros b f n m H' H'0; split; auto. simpl in |- *; auto. apply Z.le_lt_trans with (Z.abs (Fnum (Fshift radix n f))). @@ -1719,10 +1720,8 @@ repeat rewrite Zabs_Zmult; auto. apply Zle_Zmult_comp_l; auto with zarith. apply Zle_Zmult_comp_l; auto with zarith. -repeat rewrite Z.abs_eq; auto with zarith. +rewrite 2!Z.abs_eq by (apply Zpower_NR0; lia). apply Zpower_nat_monotone_le; lia. -apply Zpower_NR0; lia. -apply Zpower_NR0; lia. apply H'0. apply Z.le_trans with (Fexp (Fshift radix n f)); try apply H'0. simpl in |- *; unfold Zminus in |- *; auto with zarith. @@ -13706,6 +13705,7 @@ Lemma Veltkamp_aux_aux: forall v:float, (FtoRradix v=hx) -> Fcanonic radix b' v -> (Rabs (x-v) <= (powerRZ radix (s+Fexp x)) /2)%R -> (powerRZ radix (t-1+Fexp x) <= v)%R. +Proof. intros. case (Rle_or_lt (powerRZ radix (t-1)+(powerRZ radix s)/2)%R (Fnum x)); intros W. fold FtoRradix; apply Rplus_le_reg_l with (-v+x-powerRZ radix (t-1+Fexp x))%R. @@ -13943,7 +13943,7 @@ rewrite Z.abs_eq in H3; [idtac|apply LeR0Fnum with radix; auto with zarith real]. rewrite Zmult_comm with (Fnum x) radix. apply Z.le_trans with (2:=H3); rewrite pGivesBound. -pattern t at 2; replace t with (1+(pred t)); auto with zarith. +pattern t at 2; replace t with (1+(pred t)) by auto with zarith. rewrite Zpower_nat_is_exp. replace ( Zpower_nat radix 1) with radix;[idtac|unfold Zpower_nat; simpl]; auto with zarith. unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; rewrite Zpower_nat_Z_powerRZ. @@ -21657,8 +21657,8 @@ rewrite <- Zabs_Zopp; rewrite Z.abs_eq; auto with zarith. apply Z.lt_le_trans with 3%Z; auto with zarith. apply Z.le_trans with (nNormMin radix precision); auto with zarith. -unfold nNormMin; apply Z.le_trans with (Zpower_nat radix 2); auto with zarith. -simpl; auto with zarith. +unfold nNormMin; apply Z.le_trans with (Zpower_nat radix 2). +easy. apply Zpower_nat_monotone_le; auto with zarith. apply nNrMMimLevNum; auto with zarith. rewrite CanonicFulp; auto with zarith. @@ -25381,11 +25381,9 @@ 2: apply IZR_neq; lia. 2: apply trans_eq with (IZR (3*radix)); auto with real zarith; rewrite mult_IZR; simpl; ring. 2: apply IZR_neq; lia. -apply Rmult_le_compat_r; auto with real zarith. +apply Rmult_le_compat_r. apply powerRZ_le, IZR_lt; lia. -apply Rle_trans with (2+1)%R; auto with real. -apply Rplus_le_compat_l; apply Rle_trans with (/1)%R; auto with real. -right; ring. +lra. apply FcanonicLeastExp with radix bo p; auto with zarith. rewrite FnormalizeCorrect; auto with real zarith. apply FnormalizeCanonic; auto with zarith. diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' --exclude Makefile.in --exclude configure --exclude config.guess --exclude '*.pot' --exclude mkinstalldirs --exclude aclocal.m4 --exclude config.sub --exclude depcomp --exclude install-sh --exclude ltmain.sh old/flocq-4.1.0/src/Prop/Double_rounding.v new/flocq-4.1.1/src/Prop/Double_rounding.v --- old/flocq-4.1.0/src/Prop/Double_rounding.v 2022-04-28 13:47:40.000000000 +0200 +++ new/flocq-4.1.1/src/Prop/Double_rounding.v 2023-02-24 16:37:25.000000000 +0100 @@ -987,7 +987,7 @@ * lia. * simpl; unfold Raux.bpow, Z.pow_pos. now apply Rle_refl. - * casetype False; apply (Z.lt_irrefl 0). + * exfalso; apply (Z.lt_irrefl 0). apply (Z.lt_trans _ _ _ Hk). apply Zlt_neg_0. } rewrite (Zfloor_imp mx). @@ -2859,7 +2859,7 @@ + now apply sqrt_lt_R0. + lia. + lia. - + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid). + + intros Hmid; exfalso; apply (Rle_not_lt _ _ Hmid). apply (round_round_sqrt_aux fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx). Qed. @@ -2978,7 +2978,7 @@ + destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); lia. - + casetype False. + + exfalso. rewrite (Zlt_bool_true _ _ H') in H. lia. Qed. @@ -3240,7 +3240,7 @@ unfold sqrt. destruct Rcase_abs. + reflexivity. - + casetype False; lra. } + + exfalso; lra. } rewrite Hs. rewrite round_0. + reflexivity. @@ -3288,7 +3288,7 @@ + now apply sqrt_lt_R0. + lia. + lia. - + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid). + + intros Hmid; exfalso; apply (Rle_not_lt _ _ Hmid). apply (round_round_sqrt_radix_ge_4_aux Hbeta fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx). Qed. @@ -3412,7 +3412,7 @@ + destruct (Z.ltb_spec (ex - prec') emin'); destruct (Z.ltb_spec (ex - prec) emin); lia. - + casetype False. + + exfalso. rewrite (Zlt_bool_true _ _ H') in H. lia. Qed. @@ -3605,7 +3605,7 @@ rewrite <- (Zmult_1_r beta) at 1. apply Zmult_lt_compat_l; lia. - (* mag x < fexp2 (mag x) *) - casetype False; apply Nzx''. + exfalso; apply Nzx''. now apply (round_N_small_pos beta _ _ _ (mag x)). Qed. @@ -4286,16 +4286,16 @@ - exact Pxy. - apply Hexp. - intros Hf1 Hlxy. - casetype False. + exfalso. now apply (round_round_div_aux0 fexp1 fexp2 _ _ choice1 choice2 Hexp x y). - intros Hf1 Hlxy. - casetype False. + exfalso. now apply (round_round_div_aux1 fexp1 fexp2 _ _ choice1 choice2 Hexp x y). - intro H. apply round_round_eq_mid_beta_even; try assumption. apply Hexp. - intros Hf1 Hlxy. - casetype False. + exfalso. now apply (round_round_div_aux2 fexp1 fexp2 _ _ choice1 choice2 Hexp x y). Qed. @@ -4331,7 +4331,7 @@ apply generic_format_opp in Fy. now apply round_round_div_aux. + (* y = 0 *) - now casetype False; apply Nzy. + now exfalso; apply Nzy. + (* y > 0 *) rewrite <- (Ropp_involutive x). rewrite Ropp_div. @@ -4358,7 +4358,7 @@ apply generic_format_opp in Fy. now apply round_round_div_aux. + (* y = 0 *) - now casetype False; apply Nzy. + now exfalso; apply Nzy. + (* y > 0 *) now apply round_round_div_aux. Qed.
