Index index by Group index by Distribution index by Vendor index by creation date index by Name Mirrors Help Search

flocq-4.2.0-1.2 RPM for aarch64

From OpenSuSE Ports Tumbleweed for aarch64

Name: flocq Distribution: openSUSE Tumbleweed
Version: 4.2.0 Vendor: openSUSE
Release: 1.2 Build date: Thu Jul 25 09:00:59 2024
Group: Productivity/Scientific/Math Build host: reproducible
Size: 11265522 Source RPM: flocq-4.2.0-1.2.src.rpm
Packager: http://bugs.opensuse.org
Url: https://flocq.gitlabpages.inria.fr/
Summary: Formalization of floating point numbers for Coq
 
Flocq (Floats for Coq) is a floating-point formalization for the Coq
system.  It provides a comprehensive library of theorems on a
multi-radix multi-precision arithmetic.  It also supports efficient
numerical computations inside Coq.

Provides

Requires

License

LGPL-3.0-or-later

Changelog

* Thu Jul 25 2024 Frantisek Simorda <frantisek.simorda@suse.com>
  - Update to version 4.2.0.
    * Added SF2B' as a proof-free variant of SF2B.
    * Fixed installation of Pff2Flocq.
    * Ensured compatibility from Coq 8.12 to 8.20.
* Sun Jan 28 2024 Aaron Puchert <aaronpuchert@alice-dsl.net>
  - Update to version 4.1.4.
    * Ensured compatibility from Coq 8.12 to 8.19.
* Sun Sep 17 2023 Aaron Puchert <aaronpuchert@alice-dsl.net>
  - Update to version 4.1.2.
    * Ensured compatibility from Coq 8.12 to 8.18.
  - Update to version 4.1.3.
    * Avoided breaking users of `IEEE754.PrimFloat`.
* Wed Mar 29 2023 Aaron Puchert <aaronpuchert@alice-dsl.net>
  - Update to version 4.1.1.
    * Ensured compatibility from Coq 8.12 to 8.17.
* Thu Jan 26 2023 Aaron Puchert <aaronpuchert@alice-dsl.net> 
  - Build with ocaml-rpm-macros to get proper Requires and Provides
    for flocq-devel. This should prevent incompatibilities with other
    Ocaml libraries when building native objects against flocq-devel.
* Thu Jun 30 2022 Bernhard Wiedemann <bwiedemann@suse.com>
  - Add Git-Clone URL
* Thu Jun 02 2022 Aaron Puchert <aaronpuchert@alice-dsl.net>
  - Update to version 4.1.0.
    * Added `Bnearbyint` and `Btrunc` in `IEEE754`.
    * Ensured compatibility from Coq 8.12 to 8.16.
  - Fix patching of coqdoc invocation, make it more robust.
  - Patch up coqdoc invocation also for older Coq versions since they
    don't understand --coqlib_url.
* Fri Apr 15 2022 Aaron Puchert <aaronpuchert@alice-dsl.net>
  - Update to version 4.0.0.
    * Made Coq 8.12 the minimal version and removed the
      `IEEE754.SpecFloatCompat` layer
    * Removed automatic export of `ZArith` and `Reals` from
      `Core.Raux` and `Core.Core`
    * Proved a close/far-path adder in `Calc.Plus`.
    * Made `IEEE754.Binary` a wrapper around
      `IEEE754.BinarySingleNaN`.
  - Put development files into separate package.
  - Let documentation point to coq-doc.
* Wed Feb 05 2020 Peter Trommler <ptrommler@icloud.com>
  - update to 3.2.0
    * compatibility with coq 8.10
* Thu Oct 11 2018 ptrommler@icloud.com
  - update to 3.0.0
    * compatibility with coq 8.8

Files

/usr/lib64/coq/user-contrib/Flocq
/usr/lib64/coq/user-contrib/Flocq/.coq-native
/usr/lib64/coq/user-contrib/Flocq/.coq-native/NFlocq_Version.cmxs
/usr/lib64/coq/user-contrib/Flocq/Calc
/usr/lib64/coq/user-contrib/Flocq/Calc/.coq-native
/usr/lib64/coq/user-contrib/Flocq/Calc/.coq-native/NFlocq_Calc_Bracket.cmxs
/usr/lib64/coq/user-contrib/Flocq/Calc/.coq-native/NFlocq_Calc_Div.cmxs
/usr/lib64/coq/user-contrib/Flocq/Calc/.coq-native/NFlocq_Calc_Operations.cmxs
/usr/lib64/coq/user-contrib/Flocq/Calc/.coq-native/NFlocq_Calc_Plus.cmxs
/usr/lib64/coq/user-contrib/Flocq/Calc/.coq-native/NFlocq_Calc_Round.cmxs
/usr/lib64/coq/user-contrib/Flocq/Calc/.coq-native/NFlocq_Calc_Sqrt.cmxs
/usr/lib64/coq/user-contrib/Flocq/Calc/Bracket.vo
/usr/lib64/coq/user-contrib/Flocq/Calc/Div.vo
/usr/lib64/coq/user-contrib/Flocq/Calc/Operations.vo
/usr/lib64/coq/user-contrib/Flocq/Calc/Plus.vo
/usr/lib64/coq/user-contrib/Flocq/Calc/Round.vo
/usr/lib64/coq/user-contrib/Flocq/Calc/Sqrt.vo
/usr/lib64/coq/user-contrib/Flocq/Core
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_Core.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_Defs.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_Digits.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_FIX.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_FLT.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_FLX.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_FTZ.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_Float_prop.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_Generic_fmt.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_Raux.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_Round_NE.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_Round_pred.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_Ulp.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/.coq-native/NFlocq_Core_Zaux.cmxs
/usr/lib64/coq/user-contrib/Flocq/Core/Core.vo
/usr/lib64/coq/user-contrib/Flocq/Core/Defs.vo
/usr/lib64/coq/user-contrib/Flocq/Core/Digits.vo
/usr/lib64/coq/user-contrib/Flocq/Core/FIX.vo
/usr/lib64/coq/user-contrib/Flocq/Core/FLT.vo
/usr/lib64/coq/user-contrib/Flocq/Core/FLX.vo
/usr/lib64/coq/user-contrib/Flocq/Core/FTZ.vo
/usr/lib64/coq/user-contrib/Flocq/Core/Float_prop.vo
/usr/lib64/coq/user-contrib/Flocq/Core/Generic_fmt.vo
/usr/lib64/coq/user-contrib/Flocq/Core/Raux.vo
/usr/lib64/coq/user-contrib/Flocq/Core/Round_NE.vo
/usr/lib64/coq/user-contrib/Flocq/Core/Round_pred.vo
/usr/lib64/coq/user-contrib/Flocq/Core/Ulp.vo
/usr/lib64/coq/user-contrib/Flocq/Core/Zaux.vo
/usr/lib64/coq/user-contrib/Flocq/IEEE754
/usr/lib64/coq/user-contrib/Flocq/IEEE754/.coq-native
/usr/lib64/coq/user-contrib/Flocq/IEEE754/.coq-native/NFlocq_IEEE754_Binary.cmxs
/usr/lib64/coq/user-contrib/Flocq/IEEE754/.coq-native/NFlocq_IEEE754_BinarySingleNaN.cmxs
/usr/lib64/coq/user-contrib/Flocq/IEEE754/.coq-native/NFlocq_IEEE754_Bits.cmxs
/usr/lib64/coq/user-contrib/Flocq/IEEE754/.coq-native/NFlocq_IEEE754_Int63Compat.cmxs
/usr/lib64/coq/user-contrib/Flocq/IEEE754/.coq-native/NFlocq_IEEE754_Int63Copy.cmxs
/usr/lib64/coq/user-contrib/Flocq/IEEE754/.coq-native/NFlocq_IEEE754_PrimFloat.cmxs
/usr/lib64/coq/user-contrib/Flocq/IEEE754/Binary.vo
/usr/lib64/coq/user-contrib/Flocq/IEEE754/BinarySingleNaN.vo
/usr/lib64/coq/user-contrib/Flocq/IEEE754/Bits.vo
/usr/lib64/coq/user-contrib/Flocq/IEEE754/Int63Compat.vo
/usr/lib64/coq/user-contrib/Flocq/IEEE754/Int63Copy.vo
/usr/lib64/coq/user-contrib/Flocq/IEEE754/PrimFloat.vo
/usr/lib64/coq/user-contrib/Flocq/Pff
/usr/lib64/coq/user-contrib/Flocq/Pff/.coq-native
/usr/lib64/coq/user-contrib/Flocq/Pff/.coq-native/NFlocq_Pff_Nat2Z_compat.cmxs
/usr/lib64/coq/user-contrib/Flocq/Pff/.coq-native/NFlocq_Pff_Pff.cmxs
/usr/lib64/coq/user-contrib/Flocq/Pff/.coq-native/NFlocq_Pff_Pff2Flocq.cmxs
/usr/lib64/coq/user-contrib/Flocq/Pff/.coq-native/NFlocq_Pff_Pff2FlocqAux.cmxs
/usr/lib64/coq/user-contrib/Flocq/Pff/Nat2Z_compat.vo
/usr/lib64/coq/user-contrib/Flocq/Pff/Pff.vo
/usr/lib64/coq/user-contrib/Flocq/Pff/Pff2Flocq.vo
/usr/lib64/coq/user-contrib/Flocq/Pff/Pff2FlocqAux.vo
/usr/lib64/coq/user-contrib/Flocq/Prop
/usr/lib64/coq/user-contrib/Flocq/Prop/.coq-native
/usr/lib64/coq/user-contrib/Flocq/Prop/.coq-native/NFlocq_Prop_Div_sqrt_error.cmxs
/usr/lib64/coq/user-contrib/Flocq/Prop/.coq-native/NFlocq_Prop_Double_rounding.cmxs
/usr/lib64/coq/user-contrib/Flocq/Prop/.coq-native/NFlocq_Prop_Mult_error.cmxs
/usr/lib64/coq/user-contrib/Flocq/Prop/.coq-native/NFlocq_Prop_Plus_error.cmxs
/usr/lib64/coq/user-contrib/Flocq/Prop/.coq-native/NFlocq_Prop_Relative.cmxs
/usr/lib64/coq/user-contrib/Flocq/Prop/.coq-native/NFlocq_Prop_Round_odd.cmxs
/usr/lib64/coq/user-contrib/Flocq/Prop/.coq-native/NFlocq_Prop_Sterbenz.cmxs
/usr/lib64/coq/user-contrib/Flocq/Prop/Div_sqrt_error.vo
/usr/lib64/coq/user-contrib/Flocq/Prop/Double_rounding.vo
/usr/lib64/coq/user-contrib/Flocq/Prop/Mult_error.vo
/usr/lib64/coq/user-contrib/Flocq/Prop/Plus_error.vo
/usr/lib64/coq/user-contrib/Flocq/Prop/Relative.vo
/usr/lib64/coq/user-contrib/Flocq/Prop/Round_odd.vo
/usr/lib64/coq/user-contrib/Flocq/Prop/Sterbenz.vo
/usr/lib64/coq/user-contrib/Flocq/Version.vo
/usr/share/doc/packages/flocq
/usr/share/doc/packages/flocq/NEWS.md
/usr/share/doc/packages/flocq/README.md
/usr/share/licenses/flocq
/usr/share/licenses/flocq/AUTHORS
/usr/share/licenses/flocq/COPYING

Generated by rpm2html 1.8.1

Fabrice Bellet, Sat Nov 9 01:51:09 2024