{"bugs":[{"bugid":839102,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/coq-serapi-0.15.0-r1 - :(.text+): undefined reference to camlCmdliner_entry"},{"bugid":892235,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/coq-serapi-0.16.2-r1 fails to compile"},{"bugid":909444,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/coq-serapi-0.17.0 - Error: Unbound module Stdlib.List"},{"bugid":917066,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/coq-serapi-0.18.1 - Failed to run command: dune build @install --display=short --profile release -j 4"}],"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":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"f6ae4af46707e6bc4e80bd6a48425ed7dc44e447","committime":"2024-11-19T19:46:08","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: drop old 0.19.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"193b9d756dd486ff587377107b28e9a7966c7d39","committime":"2024-09-09T00:18:50","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"386549b58a587865bc578138a50d3158e6d066a0","committime":"2024-09-08T23:38:03","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: bump to 0.20.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"54658f1c9105f4f246be05f1ebba6bd31092b897","committime":"2024-03-04T22:04:02","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"01872ba01f3aaefe3e951ebaedeaa3364db42ae0","committime":"2024-03-04T18:54:26","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: drop old 0.18.1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"0d9a90760f6e360481b43ae31092d9c5f1ebc320","committime":"2024-02-05T11:33:13","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"f341ccb06a0a80151bb81e544986d4c7e42e3625","committime":"2024-02-04T19:29:32","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: bump to 0.19.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"e7b55509858b599b2be09a27d3829055a8aeed34","committime":"2024-01-15T21:33:16","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"7da37463eb3bf098fc760b1d1faecb48e2351229","committime":"2024-01-15T19:19:53","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: drop old 0.17.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"238fc46918c14698e86a3f14395ae9459c079834","committime":"2023-10-23T20:46:54","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"3f7751adfbf87dc0d59ba8d60dd0ce604c0a3a17","committime":"2023-10-23T20:17:28","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: bump to 0.18.1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"3bb1911b194b46a11dec2ab18c8e2e05ba47dec7","committime":"2023-07-15T22:31:50","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"c47d637abc18174ac81f3dd2cbd0d53b2d0dc225","committime":"2023-07-15T21:55:56","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: drop old 0.16.3"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"ed12505a109bd632f5836e18d282746cb9225594","committime":"2023-07-15T21:55:45","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: drop old 0.16.2-r1"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"abbb7f41bc9912de890db2cfc8eff0f41ded3850","committime":"2023-07-15T21:55:33","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: drop old 0.16.1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"59df7486cb30ec87792462ae1aeb009069501222","committime":"2023-04-10T19:01:54","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"d11706013713929a25850c2afe7544d13633fd92","committime":"2023-04-10T17:47:59","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: bump to 0.17.0"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"b9dda4f82433fcab98bdb4c5870320e7a1948817","committime":"2023-04-10T16:41:22","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: fix SRC_URI"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"613c723745c241dea5c99b2f89359d739364eb5d","committime":"2023-03-15T01:31:59","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"aaa95b088ca9506c9634f68c62fa1ec0af7fd89e","committime":"2023-03-14T23:54:31","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: introduce COQ_MIN_V"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"d7d52fa85521f19ecb6e659b8625ad34f5fcfee4","committime":"2023-02-17T01:46:50","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"256bbdf201fa87180d36af5d6ada9ac36ca116fe","committime":"2023-02-17T00:52:16","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: drop old 0.16.0-r1"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"9ff81ed4382bff314e98719044d5bd489c730495","committime":"2023-02-17T00:49:21","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: bump to 0.16.3"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"b8601001db80047a0056614fe468fb697ed0318a","committime":"2023-01-27T13:16:53","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"f82a0ccd1ec627e46d64547495ec328895456dc5","committime":"2023-01-27T11:26:26","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: remove ppx_sexp_conv restriction"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"4bd0b915aa5578e5fb6a3940c4638354433cba99","committime":"2023-01-12T01:32:00","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"561aaf46a67201c35a083921576d2af2a38e9e70","committime":"2023-01-12T00:14:37","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: drop old 0.15.0-r3"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"185fe2f36d6aa2df299937218aed7b40ca05fcd5","committime":"2023-01-11T23:59:39","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: bump to 0.16.2"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"2a77e89713b992d0dfd414fa8b66b116ae4b5dbb","committime":"2022-10-31T03:46:43","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"4b55615587fff8d0a6f297929cd3e101676f59ea","committime":"2022-10-31T03:40:06","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: bump to 0.16.1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"6806974d2366d07c7bb0dd018e10fc8662f1d7da","committime":"2022-10-26T22:16:46","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"57e2f456368e0651bd4211f1ace49d35497cb0d6","committime":"2022-10-26T21:52:29","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: remove seq dependency"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"0eb80db511e33ce759f11bf73f268ff54914a5d2","committime":"2022-10-01T23:46:40","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"384078eb058ca2044290bff23dcf9b409867e0fc","committime":"2022-10-01T22:15:08","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: bump to 0.16.0"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/873604\nSigned-off-by: Maciej Barć ","commitid":"4069d63856f17a2765b5c24a17449dbf161d9ab1","committime":"2022-10-01T20:59:38","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: restrict coq version"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"693167ded5dbbf629fb1a99a88c4e2533b49523f","committime":"2022-04-19T22:53:41","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"cb7871f4b3699944a992cf4e62afc7a7515d542f","committime":"2022-04-19T22:30:38","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: fix elisp libraries installation"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"8792d35c58099d74c89c22d9541e3ddf72310273","committime":"2022-04-16T17:38:49","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"1aeb41df7cda12870e550f0ba1f171e5f9dc8d06","committime":"2022-04-16T17:14:19","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: add ppx_sexp_conv version constraints"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"c95c84853ff511213817b94002bd925c9602054c","committime":"2022-03-05T04:51:45","packageid":74529,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Package-Manager: Portage-3.0.30, Repoman-3.0.3\nSigned-off-by: Maciej Barć ","commitid":"f6f7c1b270ceb94292a91628505bdfe5b6cebcb4","committime":"2022-03-05T02:38:53","packageid":74529,"repoid":1,"summary":"sci-mathematics\/coq-serapi: new package; add 0.15.0"}],"dependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[837451,837451],"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":314,"description":"Library for automated conversion of OCaml-values to and from S-expressions","ebuildids":[837451],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"sexplib","packageid":49507},{"block":false,"categoryid":450,"description":"Programming language supporting functional, imperative & object-oriented styles","ebuildids":[837451],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":314,"description":"Declarative definition of command line interfaces for OCaml","ebuildids":[837451],"firstseen":"2014-10-29T14:38:07.804099","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"cmdliner","packageid":62739},{"block":false,"categoryid":314,"description":"JSON parsing and pretty-printing library for OCaml","ebuildids":[837451],"firstseen":"2015-02-15T14:38:09.385452","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"yojson","packageid":63076},{"block":false,"categoryid":314,"description":"Generation of comparison functions from types","ebuildids":[837451],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_compare","packageid":64950},{"block":false,"categoryid":314,"description":"Type-driven code generation for OCaml","ebuildids":[837451],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_deriving","packageid":64953},{"block":false,"categoryid":314,"description":"Support Library for type-driven code generators","ebuildids":[837451],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_sexp_conv","packageid":64965},{"block":false,"categoryid":314,"description":"PPX rewriter that generates hash functions from type expressions and definitions","ebuildids":[837451],"firstseen":"2017-04-02T13:36:30.774148","name":"ppx_hash","packageid":66716},{"block":false,"categoryid":314,"description":"A composable build system for OCaml","ebuildids":[837451],"firstseen":"2019-07-25T19:34:21.841979","name":"dune","packageid":69971},{"block":false,"categoryid":314,"description":"JSON codec generator for OCaml","ebuildids":[837451],"firstseen":"2021-12-03T03:24:56.758232","name":"ppx_deriving_yojson","packageid":73696},{"block":false,"categoryid":314,"description":"A syntax extension for importing declarations from interface files","ebuildids":[837451],"firstseen":"2022-03-05T04:57:32.030109","name":"ppx_import","packageid":74526}],"depending":[],"ebuilds":[{"archs":["~amd64"],"ebuildid":837451,"firstseen":"2024-09-09T01:30:06.120421","license":"GPL-3+","moddate":"2026-03-29T19:42:48","packageid":74529,"repoid":1,"slot":"0\/0.20.0","uses":["emacs","ocamlopt","test"],"version":"0.20.0"}],"masks":[],"package":{"categoryid":317,"description":"Serialization library and protocol for interaction with the Coq proof assistant","firstseen":"2022-03-05T04:57:32.030109","name":"coq-serapi","packageid":74529,"summary":"SerAPI is a library for machine-to-machine interaction with the Coq proof assistant, with particular emphasis on applications in IDEs, code analysis tools, and machine learning. SerAPI provides automatic serialization of Coq's internal OCaml datatypes from\/to JSON or S-expressions (sexps). SerAPI is a proof-of-concept and should be considered alpha-quality."},"rdependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[837451,837451],"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":314,"description":"Library for automated conversion of OCaml-values to and from S-expressions","ebuildids":[837451],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"sexplib","packageid":49507},{"block":false,"categoryid":450,"description":"Programming language supporting functional, imperative & object-oriented styles","ebuildids":[837451],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":314,"description":"Declarative definition of command line interfaces for OCaml","ebuildids":[837451],"firstseen":"2014-10-29T14:38:07.804099","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"cmdliner","packageid":62739},{"block":false,"categoryid":314,"description":"JSON parsing and pretty-printing library for OCaml","ebuildids":[837451],"firstseen":"2015-02-15T14:38:09.385452","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"yojson","packageid":63076},{"block":false,"categoryid":314,"description":"Generation of comparison functions from types","ebuildids":[837451],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_compare","packageid":64950},{"block":false,"categoryid":314,"description":"Type-driven code generation for OCaml","ebuildids":[837451],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_deriving","packageid":64953},{"block":false,"categoryid":314,"description":"Support Library for type-driven code generators","ebuildids":[837451],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_sexp_conv","packageid":64965},{"block":false,"categoryid":314,"description":"PPX rewriter that generates hash functions from type expressions and definitions","ebuildids":[837451],"firstseen":"2017-04-02T13:36:30.774148","name":"ppx_hash","packageid":66716},{"block":false,"categoryid":314,"description":"A composable build system for OCaml","ebuildids":[837451],"firstseen":"2019-07-25T19:34:21.841979","name":"dune","packageid":69971},{"block":false,"categoryid":314,"description":"JSON codec generator for OCaml","ebuildids":[837451],"firstseen":"2021-12-03T03:24:56.758232","name":"ppx_deriving_yojson","packageid":73696},{"block":false,"categoryid":314,"description":"A syntax extension for importing declarations from interface files","ebuildids":[837451],"firstseen":"2022-03-05T04:57:32.030109","name":"ppx_import","packageid":74526}],"repos":[{"branch":"master","lastcommit":"0f9eef1364b18d709a5961f55b8888db47e5201e","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["https:\/\/github.com\/ejgallego\/coq-serapi\/"],"uses":[{"description":"Add support for GNU Emacs","isdefault":false,"use":"emacs"},{"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"},{"description":"Enable dependencies and\/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)","isdefault":false,"use":"test"}]}