Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
Name: flocq | Distribution: openSUSE Tumbleweed |
Version: 4.2.0 | Vendor: openSUSE |
Release: 1.1 | Build date: Thu Jul 25 09:00:59 2024 |
Group: Productivity/Scientific/Math | Build host: reproducible |
Size: 12328594 | Source RPM: flocq-4.2.0-1.1.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.
LGPL-3.0-or-later
* 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
/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, Fri Aug 30 03:38:08 2024