NEWS 8.51 KB
Newer Older
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1 2 3
Version 2.6.1:
 - ensured compatibility from Coq 8.4 to 8.8

Guillaume Melquiond's avatar
Guillaume Melquiond committed
4 5 6 7 8 9
Version 2.6.0:
 - ensured compatibility from Coq 8.4 to 8.7
 - removed some hypotheses on some lemmas of Fcore_ulp
 - added lemmas to Fprop_plus_error
 - improved examples

Guillaume Melquiond's avatar
Guillaume Melquiond committed
10 11 12
Version 2.5.2:
 - ensured compatibility from Coq 8.4 to 8.6

Guillaume Melquiond's avatar
Guillaume Melquiond committed
13 14 15
Version 2.5.1:
 - ensured compatibility with both Coq 8.4 and 8.5

BOLDO Sylvie's avatar
BOLDO Sylvie committed
16
Version 2.5.0:
Guillaume Melquiond's avatar
Guillaume Melquiond committed
17 18 19 20 21 22
 - ensured compatibility with both Coq 8.4 and 8.5
   (Flocq now provides its own version of iter_pos)
 - redefined ulp, so that ulp(0) is meaningful
 - renamed, generalized, and added lemmas in Fcore_ulp
 - extended predecessor and successor to nonpositive values
   (the previous definition of pred has been renamed pred_pos)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
23
 - removed some hypotheses on lemmas of Fprop_relative
Guillaume Melquiond's avatar
Guillaume Melquiond committed
24 25 26 27 28 29 30
 - added more examples
   . Average: proof on Sterbenz's average and correctly-rounded average
   . Cody_Waite: Cody & Waite's approximation of exponential
   . Compute: effective FP computations with an example of sqrt(sqr(x))
     in radix 5 and precision 3
   . Division_u16: integer division using floating-point FMA
   . Triangle: Kahan's algorithm for the area of a triangle
BOLDO Sylvie's avatar
BOLDO Sylvie committed
31

Guillaume Melquiond's avatar
Guillaume Melquiond committed
32 33 34
Version 2.4.0:
 - moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free
 - added theorems about double rounding being innocuous (Fappli_double_round.v)
35
 - added example about double rounding in odd radix
Guillaume Melquiond's avatar
Guillaume Melquiond committed
36 37
 - improved a bit the efficiency of IEEE-754 arithmetic

Guillaume Melquiond's avatar
Guillaume Melquiond committed
38 39 40 41 42
Version 2.3.0:
 - moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free
 - used the square root from the standard library instead of a custom one
 - added an example about sqrt(sqr(x))

Guillaume Melquiond's avatar
Guillaume Melquiond committed
43 44 45
Version 2.2.2:
 - fixed install target for case-insensitive filesystems

46 47 48
Version 2.2.1:
 - fixed regeneration of Flocq_version.v

Guillaume Melquiond's avatar
Guillaume Melquiond committed
49 50 51 52
Version 2.2.0:
 - added theorems about rounding to odd and double rounding
 - improved handling of special values of IEEE-754 arithmetic

Guillaume Melquiond's avatar
Guillaume Melquiond committed
53 54 55 56 57 58
Version 2.1.0:
 - ensured compatibility with both Coq 8.3 and 8.4
 - improved support for rounding toward and away from zero
 - proved that formats are stable by arbitrary rounding or ulp addition
 - generalized usage of ln_beta

59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
Version 2.0.0:
 - changed rounding modes from records to R -> Z functions as arguments
   to the round function
   . rndDN -> Zfloor
   . rndUP -> Zceil
   . rndZE -> Ztrunc
   . rndNE -> ZnearestE
   . rndNA -> ZnearestA
 - added typeclasses for automatic inference of properties:
   . Valid_exp for Z -> Z functions describing formats
   . Valid_rnd for R -> Z functions describing rounding modes
   . Exp_not_FTZ for Z -> Z functions describing formats with subnormal
   . Monotone_exp for Z -> Z functions describing regular formats
   . Exists_NE for radix/formats supporting rounding to nearest even
 - removed theorems superseded by typeclasses:
   . FIX_exp_correct, FLX_exp_correct, FLT_exp_correct, FTZ_exp_correct
   . FIX_exp_monotone, FLX_exp_monotone, FLT_monotone
   . Rnd_NE_pt_FIX, Rnd_NE_pt_FLX, Rnd_NE_pt_FLT
   . round_NE_pt_FLX, round_NE_pt_FLT
   . Zrnd_opp_le, Zrnd_Z2R_opp
BOLDO Sylvie's avatar
BOLDO Sylvie committed
79
 - removed example file Fappli_sqrt_FLT_ne
80 81 82 83 84 85 86 87 88 89 90 91 92 93
 - split theorems on equivalence between specific and generic formats
   into both directions:
   . FIX_format_generic and generic_format_FIX
   . FLX_format_generic and generic_format_FLX
   . FLT_format_generic and generic_format_FLT
   . FTZ_format_generic and generic_format_FTZ
 - modified correctness theorems for IEEE-754 operators so that they also
   mention finiteness of the results
 - added a Flocq_version.Flocq_version Coq variable for Flocq detection
   and version testing in configure scripts
 - moved parts of some files into other files:
   . Fcore_Raux -> Fcore_Zaux
   . Fcalc_digits -> Fcore_digits
   . Fappli_IEEE -> Fappli_IEEE_bits
94 95 96
 - renamed functions:
   . canonic_exponent -> canonic_exp
   . digits -> Zdigits
BOLDO Sylvie's avatar
BOLDO Sylvie committed
97 98 99 100 101 102
   . bounded_prec -> canonic_mantissa
   . Bsign_FF -> sign_FF
   . shl -> shl_align
   . shl_fexp -> shl_align_fexp
   . binary_round_sign -> binary_round_aux
   . binary_round_sign_shl -> binary_round
103 104 105 106 107
 - renamed theorems more uniformly:
   . Rabs_Rminus_pos -> Rabs_minus_le
   . exp_increasing_weak -> exp_le
   . ln_beta_monotone -> ln_beta_le
   . ln_beta_monotone_abs -> ln_beta_le_abs
108 109
   . abs_F2R -> F2R_Zabs (changed direction)
   . opp_F2R -> F2R_Zopp (changed direction)
110 111 112 113 114 115 116
   . scaled_mantissa_bpow -> scaled_mantissa_mult_bpow
   . round_monotone -> round_le
   . round_monotone_l -> round_ge_generic
   . round_monotone_r -> round_le_generic
   . round_monotone_abs_l -> abs_round_ge_generic
   . round_monotone_abs_r -> abs_round_le_generic
   . generic_format_canonic_exponent -> generic_format_F2R (modified hypothesis)
117
   . canonic_exponent_round -> canonic_exp_round_ge
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
   . generic_N_pt -> round_N_pt
   . round_pred_pos_imp_rnd -> round_pred_ge_0
   . round_pred_rnd_imp_pos -> round_pred_gt_0
   . round_pred_neg_imp_rnd -> round_pred_le_0
   . round_pred_rnd_imp_neg -> round_pred_lt_0
   . ulp_le_pos -> ulp_le_id
   . succ_lt_le -> succ_le_lt
   . ulp_monotone -> ulp_le
   . ulp_DN_pt_eq -> ulp_DN
   . format_pred -> generic_format_pred
   . pred_ulp -> pred_plus_ulp
   . pred_lt -> pred_lt_id
   . FLT_generic_format_FLX -> generic_format_FLT_FLX
   . FLX_generic_format_FLT -> generic_format_FLX_FLT
   . FIX_generic_format_FLT -> generic_format_FIX_FLT
   . FLT_generic_format_FIX -> generic_format_FLT_FIX
   . FLT_round_FLX -> round_FLT_FLX
   . FTZ_round -> round_FTZ_FLX
   . FTZ_round_small -> round_FTZ_small
   . FLT_canonic_FLX -> canonic_exp_FLT_FLX
   . FLT_canonic_FIX -> canonic_exp_FLT_FIX
139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
   . canonic_exponent_opp -> canonic_exp_opp
   . canonic_exponent_abs -> canonic_exp_abs
   . canonic_exponent_fexp -> canonic_exp_fexp
   . canonic_exponent_fexp_pos -> canonic_exp_fexp_pos
   . canonic_exponent_DN -> canonic_exp_DN
   . canonic_exp_ge -> abs_lt_bpow_prec (modified hypotheses)
   . Fopp_F2R -> F2R_opp
   . Fabs_F2R -> F2R_abs
   . plus_F2R -> F2R_plus
   . minus_F2R -> F2R_minus
   . mult_F2R -> F2R_mult
   . digits_abs -> Zdigits_abs
   . digits_ge_0 -> Zdigits_ge_0
   . digits_gt_0 -> Zdigits_gt_0
   . ln_beta_F2R_Zdigits -> ln_beta_F2R_Zdigits
   . digits_shift -> Zdigits_mult_Zpower
   . digits_Zpower -> Zdigits_Zpower
   . digits_le -> Zdigits_le
   . lt_digits -> lt_Zdigits
   . Zpower_le_digits -> Zpower_le_Zdigits
   . digits_le_Zpower -> Zdigits_le_Zpower
   . Zpower_gt_digits -> Zpower_gt_Zdigits
   . digits_gt_Zpower -> Zdigits_gt_Zpower
   . digits_mult_strong -> Zdigits_mult_strong
   . digits_mult -> Zdigits_mult
   . digits_mult_ge -> Zdigits_mult_ge
   . digits_shr -> Zdigits_div_Zpower
   . format_add -> generic_format_plus_prec (modified hypothesis)
   . format_nx -> ex_Fexp_canonic
BOLDO Sylvie's avatar
BOLDO Sylvie committed
168 169 170 171 172 173
   . generic_relative_error -> relative_error
   . generic_relative_error_ex -> relative_error_ex
   . generic_relative_error_F2R -> relative_error_F2R_emin
   . generic_relative_error_F2R_ex -> relative_error_F2R_emin_ex
   . generic_relative_error_2 -> relative_error_round
   . generic_relative_error_F2R_2 -> relative_error_round_F2R_emin
174
   . generic_relative_error_N -> relative_error_N
BOLDO Sylvie's avatar
BOLDO Sylvie committed
175 176 177 178 179 180
   . generic_relative_error_N_ex -> relative_error_N_ex
   . generic_relative_error_N_F2R -> relative_error_N_F2R_emin
   . generic_relative_error_N_F2R_ex -> relative_error_N_F2R_emin_ex
   . generic_relative_error_N_2 -> relative_error_N_round
   . generic_relative_error_N_F2R_2 -> relative_error_N_round_F2R_emin
   . relative_error_FLT_F2R  -> relative_error_FLT_F2R_emin
181
   . relative_error_FLT_F2R_ex -> relative_error_FLT_F2R_emin_ex
BOLDO Sylvie's avatar
BOLDO Sylvie committed
182 183 184 185 186 187
   . relative_error_N_FLT_2 -> relative_error_N_FLT_round
   . relative_error_N_FLT_F2R -> relative_error_N_FLT_F2R_emin
   . relative_error_N_FLT_F2R_ex -> relative_error_N_FLT_F2R_emin_ex
   . relative_error_N_FLT_F2R_2 -> relative_error_N_FLT_round_F2R_emin
   . relative_error_FLX_2 -> relative_error_FLX_round
   . relative_error_N_FLX_2 -> relative_error_N_FLX_round
188
   . canonic_bounded_prec -> canonic_canonic_mantissa
BOLDO Sylvie's avatar
BOLDO Sylvie committed
189 190 191 192 193
   . B2R_lt_emax -> abs_B2R_lt_emax
   . binary_unicity -> B2FF_inj
   . finite_binary_unicity -> B2R_inj
   . binary_round_sign_correct -> binary_round_aux_correct
   . shl_correct -> shl_align_correct
194 195
   . snd_shl -> snd_shl_align
   . shl_fexp_correct -> shl_align_fexp_correct
BOLDO Sylvie's avatar
BOLDO Sylvie committed
196
   . binary_round_sign_shl_correct -> binary_round_correct
197

Guillaume Melquiond's avatar
Guillaume Melquiond committed
198 199 200 201
Version 1.4.0:
 - improved efficiency of IEEE-754 addition
 - fixed compilation with Coq 8.3

Guillaume Melquiond's avatar
Guillaume Melquiond committed
202 203 204
Version 1.3:
 - fixed overflow handling in IEEE-754 formats with directed rounding

Guillaume Melquiond's avatar
Guillaume Melquiond committed
205 206 207
Version 1.2:
 - added IEEE-754 binary32 and 64 formats, including infinities and NaN

208 209 210 211 212 213
Version 1.1:
 - simplified effective rounding for negative reals
 - proved monotonicity of exponent functions for common formats

Version 1.0:
 - initial release