{"bugs":[{"bugid":914278,"firstseen":"2023-09-16T10:45:58.077090","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":"2024-10-01T18:53:41.971790","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"},{"bugid":941414,"firstseen":"2024-10-12T18:47:55.630604","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/flocq-4.1.1 - [libtool] [gcc-15] Error: The variable plus_0_r was not found in the current environment."}],"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":"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":"Proof assistant written in O'Caml","ebuildids":[778209,782877],"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":[778209,782877],"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":"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":782877,"firstseen":"2023-04-02T00:20:14.321206","license":"LGPL-3","moddate":"2024-10-08T16:04:52","packageid":75711,"repoid":1,"slot":"0","uses":[],"version":"4.1.1"},{"archs":["~amd64","~x86"],"ebuildid":778209,"firstseen":"2023-02-16T12:19:02.918399","license":"LGPL-3","moddate":"2024-10-08T16:04:52","packageid":75711,"repoid":1,"slot":"0","uses":[],"version":"4.1.0-r1"}],"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":"Proof assistant written in O'Caml","ebuildids":[778209,782877],"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":[778209,782877],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590}],"repos":[{"branch":"master","lastcommit":"4f427b63a3d98d2dec3f9eafc993a2cf919cdbaf","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["http:\/\/flocq.gforge.inria.fr\/","https:\/\/gitlab.inria.fr\/flocq\/flocq\/"],"uses":[]}