{"bugs":[{"bugid":914278,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/flocq-4.1.1 - Error: The variable Z_div_mod_eq was not found in the current environment."},{"bugid":940621,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/flocq-4.1.1 - [ncurses-6.5] [libtool] [gcc-15] checking for coqc... .\/configure:line : which: command not found"}],"categories":[{"categoryid":450,"name":"dev-lang","summary":"The dev-lang category contains various programming language implementations and related tools."},{"categoryid":317,"name":"sci-mathematics","summary":"The sci-mathematics category contains mathematical software."}],"changelog":[{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"bb807a3820eaa72357661c2e2e61f325b0af3e41","committime":"2025-03-24T00:35:11","packageid":75711,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/951919\nSigned-off-by: Maciej Barć ","commitid":"fb7aaa7ec643e2dc44a226b79f93294253402463","committime":"2025-03-23T23:12:55","packageid":75711,"repoid":1,"summary":"sci-mathematics\/flocq: drop old 4.1.1"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"002bdcb161f918dc70e27c47825eecf0f7878e6b","committime":"2025-03-23T23:07:38","packageid":75711,"repoid":1,"summary":"sci-mathematics\/flocq: drop old 4.1.0-r1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"339a0ad8228444a7438329b0a9658941c922f46f","committime":"2025-02-16T22:48:30","packageid":75711,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"bde3b54c68682c78ef13c10baf2e42b16606c926","committime":"2025-02-16T21:56:50","packageid":75711,"repoid":1,"summary":"sci-mathematics\/flocq: bump to 4.2.1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"6d742e07bfa722d2fd567f02a2e44185a49df042","committime":"2023-04-11T14:33:51","packageid":75711,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/904156\nSigned-off-by: Maciej Barć ","commitid":"66e46e9f808925425d9ba22f89d0794ce3fafa87","committime":"2023-04-11T12:02:16","packageid":75711,"repoid":1,"summary":"sci-mathematics\/flocq: ignore CFLAGS for ML\/Coq code"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"64bb5f74af3bc6dd3396d6f48a5f9a5e4ce4e8bc","committime":"2023-04-01T23:01:53","packageid":75711,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"63e7f70de010945b04f0666c2f18704d552c2b6e","committime":"2023-04-01T21:48:45","packageid":75711,"repoid":1,"summary":"sci-mathematics\/flocq: bump to 4.1.1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"5e6e5593474bb863dfd4fc3e00ebc1905a6b1fe9","committime":"2023-02-16T12:02:14","packageid":75711,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"f0fa8cbb62c755c347fca77a212d6f0ceb1d89ba","committime":"2023-02-16T11:51:11","packageid":75711,"repoid":1,"summary":"sci-mathematics\/flocq: fix deps"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"6e288cd66e2a6decf926f97186f12f9082581588","committime":"2022-12-24T22:32:58","packageid":75711,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"889a3cff4fa58c3b06643479ec34656758c52315","committime":"2022-12-24T21:28:46","packageid":75711,"repoid":1,"summary":"sci-mathematics\/flocq: new package; add 4.1.0"}],"dependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[854229],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"coq","packageid":42174,"summary":"Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: * the definition of functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to check these proofs by a small certification \"kernel\". Coq is based on a logical framework called \"Calculus of Inductive Constructions\" extended by a modular development system for theories."},{"block":false,"categoryid":450,"description":"Programming language supporting functional, imperative & object-oriented styles","ebuildids":[854229],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590}],"depending":[{"block":false,"categoryid":317,"description":"Platform for deductive program verification","ebuildids":[854230,854230,869907,869907,877153,877153],"firstseen":"2021-12-12T02:08:52.137547","name":"why3","packageid":73747,"summary":"Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs."},{"block":false,"categoryid":317,"description":"Allows the certificates Gappa generates to be imported by the Coq","ebuildids":[778210,778210,783789,783789],"firstseen":"2022-12-24T22:51:22.910451","name":"gappalib-coq","packageid":75713}],"ebuilds":[{"archs":["~amd64","~x86"],"ebuildid":854229,"firstseen":"2025-02-16T22:50:58.717736","license":"LGPL-3","moddate":"2026-03-28T18:04:21","packageid":75711,"repoid":1,"slot":"0","uses":[],"version":"4.2.1"}],"masks":[],"package":{"categoryid":317,"description":"Formalization of floating-point arithmetic for the Coq proof assistant","firstseen":"2022-12-24T22:51:22.910451","name":"flocq","packageid":75711,"summary":"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."},"rdependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[854229],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"coq","packageid":42174,"summary":"Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: * the definition of functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to check these proofs by a small certification \"kernel\". Coq is based on a logical framework called \"Calculus of Inductive Constructions\" extended by a modular development system for theories."},{"block":false,"categoryid":450,"description":"Programming language supporting functional, imperative & object-oriented styles","ebuildids":[854229],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590}],"repos":[{"branch":"master","lastcommit":"52197549fd3431fa256b8edbafdcd3702dd0e134","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["http:\/\/flocq.gforge.inria.fr\/","https:\/\/gitlab.inria.fr\/flocq\/flocq\/"],"uses":[]}