{"bugs":[{"bugid":259477,"firstseen":"2016-06-16T16:08:01.789616","severity":"enhancement","status":"CONFIRMED","summary":"[science overlay] sci-mathematics\/gappalib-coq"}],"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":"59df7486cb30ec87792462ae1aeb009069501222","committime":"2023-04-10T19:01:54","packageid":75713,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"9570e800fac85b2b29020ddcf5867e43ac2b638e","committime":"2023-04-10T17:40:29","packageid":75713,"repoid":1,"summary":"sci-mathematics\/gappalib-coq: bump to 1.5.3"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"5e6e5593474bb863dfd4fc3e00ebc1905a6b1fe9","committime":"2023-02-16T12:02:14","packageid":75713,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/894746\nSigned-off-by: Maciej Barć ","commitid":"a067191668da35890eb2cd748e83849fbaf0c905","committime":"2023-02-16T11:35:07","packageid":75713,"repoid":1,"summary":"sci-mathematics\/gappalib-coq: fix deps; add ocamlopt"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"6e288cd66e2a6decf926f97186f12f9082581588","committime":"2022-12-24T22:32:58","packageid":75713,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"dd5837f89259971fd9e1fa05d402c1595b1f4ac4","committime":"2022-12-24T22:08:37","packageid":75713,"repoid":1,"summary":"sci-mathematics\/gappalib-coq: new package; add 1.5.2"}],"dependencies":[{"block":false,"categoryid":317,"description":"Proof assistant written in O'Caml","ebuildids":[778210,783789],"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":[778210,783789],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":317,"description":"Formalization of floating-point arithmetic for the Coq proof assistant","ebuildids":[778210,783789],"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."},{"block":false,"categoryid":317,"description":"Tool for verifying floating-point or fixed-point arithmetic","ebuildids":[778210,783789],"firstseen":"2022-12-24T22:51:22.910451","name":"gappa","packageid":75712,"summary":"Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques -- automatic proof generation of arithmetic properties) is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic."}],"depending":[],"ebuilds":[{"archs":["~amd64","~x86"],"ebuildid":783789,"firstseen":"2023-04-10T20:20:18.023620","license":"LGPL-3+","moddate":"2024-10-08T16:04:52","packageid":75713,"repoid":1,"slot":"0","uses":["ocamlopt"],"version":"1.5.3"},{"archs":["~amd64","~x86"],"ebuildid":778210,"firstseen":"2023-02-16T12:19:02.918399","license":"LGPL-3+","moddate":"2024-10-08T16:04:52","packageid":75713,"repoid":1,"slot":"0","uses":["ocamlopt"],"version":"1.5.2-r1"}],"masks":[],"package":{"categoryid":317,"description":"Allows the certificates Gappa generates to be imported by the Coq","firstseen":"2022-12-24T22:51:22.910451","name":"gappalib-coq","packageid":75713},"rdependencies":[{"block":false,"categoryid":317,"description":"Proof assistant written in O'Caml","ebuildids":[778210,783789],"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":[778210,783789],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":317,"description":"Formalization of floating-point arithmetic for the Coq proof assistant","ebuildids":[778210,783789],"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."},{"block":false,"categoryid":317,"description":"Tool for verifying floating-point or fixed-point arithmetic","ebuildids":[778210,783789],"firstseen":"2022-12-24T22:51:22.910451","name":"gappa","packageid":75712,"summary":"Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques -- automatic proof generation of arithmetic properties) is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic."}],"repos":[{"branch":"master","lastcommit":"1dac680b842417cd17ad308600a5833b89534839","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["https:\/\/gappa.gitlabpages.inria.fr\/","https:\/\/gitlab.inria.fr\/gappa\/coq\/"],"uses":[{"description":"Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable\/enable it at a global scale)","isdefault":false,"use":"ocamlopt"}]}