sci-mathematics / flocq

Formalization of floating-point arithmetic for the Coq proof assistant

Official package sites : http://flocq.gforge.inria.fr/ · https://gitlab.inria.fr/flocq/flocq/ ·

Flocq (Floats for Coq) is a formalization of floating-point arithmetic for the Coq proof assistant. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.

v4.1.1 :: 0 :: gentoo

Modified
License
LGPL-3
Keywords
~amd64 ~x86

v4.1.0-r1 :: 0 :: gentoo

Modified
License
LGPL-3
Keywords
~amd64 ~x86

dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles

sci-mathematics / coq : Proof assistant written in O'Caml

dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles

sci-mathematics / coq : Proof assistant written in O'Caml

sci-mathematics / gappalib-coq : Allows the certificates Gappa generates to be imported by the Coq

914278
sci-mathematics/flocq-4.1.1 - Error: The variable Z_div_mod_eq was not found in the current environment.
940621
sci-mathematics/flocq-4.1.1 - [ncurses-6.5] [libtool] [gcc-15] checking for coqc... ./configure:line <snip>: which: command not found
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/flocq: ignore CFLAGS for ML/Coq code
Closes: https://bugs.gentoo.org/904156 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/flocq: bump to 4.1.1
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/flocq: fix deps
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/flocq: new package; add 4.1.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org>