{"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":[{"block":false,"categoryid":317,"description":"Toolkit for literate programming in Coq","ebuildids":[824610,824610],"firstseen":"2022-03-05T04:57:32.030109","name":"alectryon","packageid":74527,"summary":"A library to process Coq and Lean snippets embedded in text documents, showing goals and messages for each input sentence. Also a literate programming toolkit. The goal of Alectryon is to make it easy to write textbooks, blog posts, and other documents that mix interactive proofs and prose. Alectryon originally supported Coq only. Support for Lean is preliminary and restricted to Lean 3."}],"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":"43a4988e0fa15f038220ebd74aa888ace0c9b303","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"}]}