{"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":"40265e5b42396dd568af5054f0ffe2209cf3ac0f","committime":"2024-11-19T20:03:21","packageid":75710,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"6463bc79f49c4f73f648fb510a867faec74c5e0e","committime":"2024-11-19T19:47:00","packageid":75710,"repoid":1,"summary":"dev-ml\/coq-menhirlib: drop old 20231231-r1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"3ce7c49dcb31e83f40bfbff1eaac4fe0da218d15","committime":"2024-09-13T21:03:54","packageid":75710,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/923844\nSigned-off-by: Maciej Barć ","commitid":"0fda007f3702996f499fd6fc554acddb2d1f7dc5","committime":"2024-09-13T15:20:43","packageid":75710,"repoid":1,"summary":"dev-ml\/coq-menhirlib: drop old 20220210"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/939577\nSigned-off-by: Maciej Barć ","commitid":"7d13e0a6f6edaa4630178cdb0ddb39411aa06727","committime":"2024-09-13T15:18:50","packageid":75710,"repoid":1,"summary":"dev-ml\/coq-menhirlib: pin coq <8.20.0 to version 20231231"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"22e21fb0e0bdd2c70006255130a8ded31bacffbe","committime":"2024-09-13T15:16:14","packageid":75710,"repoid":1,"summary":"dev-ml\/coq-menhirlib: bump to 20240715"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"66ba8b192f0c28159b8aaad1850f05067d78b62e","committime":"2024-08-01T13:18:53","packageid":75710,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"07287b99b166a8b660cfadf84a51e7336b66537d","committime":"2024-08-01T11:21:02","packageid":75710,"repoid":1,"summary":"dev-ml\/coq-menhirlib: bump to 20231231"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"0c2a54602cc4b1482bd13fc643fc5ce21b275670","committime":"2022-12-23T23:02:04","packageid":75710,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/888075\nSigned-off-by: Maciej Barć ","commitid":"d9fe66b2052fae9473fa7abc1a00b338b63d8e00","committime":"2022-12-23T22:35:13","packageid":75710,"repoid":1,"summary":"dev-ml\/coq-menhirlib: new package; add 20220210"}],"dependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[838108],"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":[838108],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":314,"description":"LR(1) parser generator for the OCaml language","ebuildids":[838108],"firstseen":"2013-02-08T14:36:53.188287","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"menhir","packageid":60329},{"block":false,"categoryid":314,"description":"A composable build system for OCaml","ebuildids":[838108],"firstseen":"2019-07-25T19:34:21.841979","name":"dune","packageid":69971}],"depending":[],"ebuilds":[{"archs":["~amd64","~x86"],"ebuildid":838108,"firstseen":"2024-09-13T22:18:43.965122","license":"GPL-2 LGPL-2-with-linking-exception","moddate":"2026-03-29T19:42:47","packageid":75710,"repoid":1,"slot":"0\/20240715","uses":["ocamlopt"],"version":"20240715"}],"masks":[],"package":{"categoryid":314,"description":"A support library for verified Coq parsers produced by Menhir","firstseen":"2022-12-23T23:06:16.335529","name":"coq-menhirlib","packageid":75710},"rdependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[838108],"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":[838108],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":314,"description":"LR(1) parser generator for the OCaml language","ebuildids":[838108],"firstseen":"2013-02-08T14:36:53.188287","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"menhir","packageid":60329},{"block":false,"categoryid":314,"description":"A composable build system for OCaml","ebuildids":[838108],"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":["http:\/\/gallium.inria.fr\/~fpottier\/menhir\/"],"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"}]}