{"bugs":[],"categories":[{"categoryid":450,"name":"dev-lang","summary":"The dev-lang category contains various programming language implementations and related tools."},{"categoryid":314,"name":"dev-ml","summary":"The dev-ml category contains libraries and utilities relevant to the ML programming language."},{"categoryid":317,"name":"sci-mathematics","summary":"The sci-mathematics category contains mathematical software."}],"changelog":[{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"54283d53384498ab5c99833c56fb3cc3d16e7bbb","committime":"2026-02-17T22:15:58","packageid":78227,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"9d5e489538031d7f663844aaa18dd1cb69d27928","committime":"2026-02-17T21:19:44","packageid":78227,"repoid":1,"summary":"sci-mathematics\/coq-stdlib: bump to 9.1.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"db73ec035ad311425312a6aee7dfe1730285068f","committime":"2025-11-07T21:45:46","packageid":78227,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"arthurzam@gentoo.org","authorname":"Arthur Zamarin","body":"Signed-off-by: Arthur Zamarin ","commitid":"684cfa82f3b87d30b94e0530bdbb0352415e1369","committime":"2025-11-07T21:36:18","packageid":78227,"repoid":1,"summary":"sci-mathematics\/coq-stdlib: Stabilize 9.0.0-r1 amd64, #965809"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"ff4ac62f58d134dda2d7af8fcf4623d5ed6a300a","committime":"2025-10-07T01:49:13","packageid":78227,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/963863\nSigned-off-by: Maciej Barć ","commitid":"e5ad8c8eb25b4d090ae1e45018166f0649b38f3b","committime":"2025-10-06T20:42:51","packageid":78227,"repoid":1,"summary":"sci-mathematics\/coq-stdlib: depend on coq sub-slot"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"1590ac692de6131ea861dd9602069b32242334f6","committime":"2025-03-16T22:48:36","packageid":78227,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"sam@gentoo.org","authorname":"Sam James","body":"Signed-off-by: Sam James ","commitid":"aced2ffe5ad95bc5b185a7f2f79362c4db4d85ee","committime":"2025-03-16T22:40:22","packageid":78227,"repoid":1,"summary":"sci-mathematics\/coq-stdlib: Keyword 9.0.0 arm64, #951475"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"37dbdcae477009dd50af8883b26556ad1accdd78","committime":"2025-03-16T21:19:01","packageid":78227,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"4889e5bf4461b7b6fd88cf2465f92c4e8ac7bd3a","committime":"2025-03-16T20:44:00","packageid":78227,"repoid":1,"summary":"sci-mathematics\/coq-stdlib: new package; add 9.0.0"}],"dependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[878107,890316],"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":[878107,890316],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":314,"description":"A composable build system for OCaml","ebuildids":[878107,890316],"firstseen":"2019-07-25T19:34:21.841979","name":"dune","packageid":69971}],"depending":[],"ebuilds":[{"archs":["~amd64","~arm64"],"ebuildid":890316,"firstseen":"2026-02-17T22:18:31.068672","license":"LGPL-2.1","moddate":"2026-03-29T19:42:48","packageid":78227,"repoid":1,"slot":"0\/9.1.0","uses":["ocamlopt"],"version":"9.1.0"},{"archs":["amd64","~arm64"],"ebuildid":878107,"firstseen":"2025-10-07T02:51:14.332521","license":"LGPL-2.1","moddate":"2026-03-29T19:42:48","packageid":78227,"repoid":1,"slot":"0\/9.0.0","uses":["ocamlopt"],"version":"9.0.0-r1"}],"masks":[],"package":{"categoryid":317,"description":"Stdlib for the Coq\/Rocq Prover, used to be part of Coq","firstseen":"2025-03-16T21:36:59.045185","name":"coq-stdlib","packageid":78227},"rdependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[878107,890316],"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":[878107,890316],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":314,"description":"A composable build system for OCaml","ebuildids":[878107,890316],"firstseen":"2019-07-25T19:34:21.841979","name":"dune","packageid":69971}],"repos":[{"branch":"master","lastcommit":"52197549fd3431fa256b8edbafdcd3702dd0e134","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["https:\/\/github.com\/coq\/stdlib\/"],"uses":[{"defaultflag":true,"description":"Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable\/enable it at a global scale)","isdefault":true,"use":"ocamlopt"}]}