{"bugs":[],"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":"37dbdcae477009dd50af8883b26556ad1accdd78","committime":"2025-03-16T21:19:01","packageid":74528,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"3a77bece10ca6cbbc69bffed2e22cd0e6324a03e","committime":"2025-03-16T20:45:21","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: add coq max version pin"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"54658f1c9105f4f246be05f1ebba6bd31092b897","committime":"2024-03-04T22:04:02","packageid":74528,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"3ab6c9b10d3304bb07f5d73b686af424f56afa94","committime":"2024-03-04T18:56:13","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: drop old 1.17.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"e7b55509858b599b2be09a27d3829055a8aeed34","committime":"2024-01-15T21:33:16","packageid":74528,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"d742b9c269831aa6dd549a8d060dbbcb905a9504","committime":"2024-01-15T19:32:03","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: bump to 1.19.0"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"07b6a44a3601a510c1026df4ee79f5611e36e441","committime":"2024-01-15T19:20:40","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: drop old 1.16.0-r1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"a27f8106bba33713e5c160257801567757583deb","committime":"2023-10-24T12:46:46","packageid":74528,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"57f9a61d58baa1724b28298750768db0c60a1eb3","committime":"2023-10-24T12:30:24","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: bump to 1.17.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"3bb1911b194b46a11dec2ab18c8e2e05ba47dec7","committime":"2023-07-15T22:31:50","packageid":74528,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"7793b4607f07619cd0aab0db63f792d1d566d7c3","committime":"2023-07-15T21:56:23","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: drop old 1.15.0-r1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"6d742e07bfa722d2fd567f02a2e44185a49df042","committime":"2023-04-11T14:33:51","packageid":74528,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"1692957583e25a4b5559363222722938a592445a","committime":"2023-04-11T12:48:07","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: drop old 1.14.0-r2"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/904155\nSigned-off-by: Maciej Barć ","commitid":"23ddd3215b20cec819a0edda598720c81dc8aa4b","committime":"2023-04-11T12:03:01","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: ignore CFLAGS for ML\/Coq code"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"613c723745c241dea5c99b2f89359d739364eb5d","committime":"2023-03-15T01:31:59","packageid":74528,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"5845e37ea1bc6cb1e9d2e80642c63b52a09c1f87","committime":"2023-03-14T23:53:27","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: introduce COQ_MIN_V"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"5e6e5593474bb863dfd4fc3e00ebc1905a6b1fe9","committime":"2023-02-16T12:02:14","packageid":74528,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"27e2f507566c78663293013fdb87f61d82c0a122","committime":"2023-02-16T11:53:46","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: fix deps"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"f50a37262f310e43bf8f8713e17e856e7e57f5b5","committime":"2023-02-02T11:01:56","packageid":74528,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"1748e659f003a6e8850e8fb21d29ec43dd8d978f","committime":"2023-02-01T16:41:42","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: bump to 1.16.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"20b92364caea0107c8a4ff8b6404e2782ecc238b","committime":"2022-09-07T12:55:19","packageid":74528,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"5e1932c167586e62fa5274da5436c21a8e9b0d15","committime":"2022-09-07T12:08:31","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: bump to 1.15.0"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/869053\nSigned-off-by: Maciej Barć ","commitid":"10130c0f4c9b16f6eebcb4d44319e7035937891e","committime":"2022-09-07T11:56:59","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: constraint coq version to <8.16.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"c95c84853ff511213817b94002bd925c9602054c","committime":"2022-03-05T04:51:45","packageid":74528,"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":"39c72c3ccecb73de2596a51af9c126a814e39977","committime":"2022-03-05T01:51:49","packageid":74528,"repoid":1,"summary":"sci-mathematics\/coq-mathcomp: new package; add 1.14.0"}],"dependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[857711,857711],"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":[857711],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590}],"depending":[],"ebuilds":[{"archs":["~amd64"],"ebuildid":857711,"firstseen":"2025-03-16T21:36:59.045185","license":"CeCILL-B","moddate":"2025-03-16T21:36:58","packageid":74528,"repoid":1,"slot":"0\/1.19.0","uses":[],"version":"1.19.0-r1"}],"masks":[],"package":{"categoryid":317,"description":"Mathematical Components for the Coq proof assistant","firstseen":"2022-03-05T04:57:32.030109","name":"coq-mathcomp","packageid":74528},"rdependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[857711,857711],"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":[857711],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590}],"repos":[{"branch":"master","lastcommit":"e8caad39d3b154c1a0421bb9baa8619654bff6e9","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["https:\/\/github.com\/math-comp\/math-comp\/"],"uses":[]}