{"bugs":[{"bugid":906225,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/why3-1.6.0 - Error: Cannot load ppx_sexp_conv: this object file uses unsafe features"},{"bugid":937720,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/why3-1.6.0 - [ncurses-6.5] [icu-75.1] [gcc-15] make inconsistent assumptions over interface Nat"},{"bugid":946556,"firstseen":"2025-07-11T02:48:40.189262","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/why3-1.7.2 - [texlive] [meson] Error: Cannot find a physical path bound to logical path Flocq.Version."},{"bugid":960678,"firstseen":"2025-07-25T16:51:37.018749","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/why3-1.8.1 - [gcc-16] emake failed"},{"bugid":968065,"firstseen":"2025-12-27T14:52:53.478133","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/why3-1.8.2 - [portage-9999] Error: Unbound value Ppxlib.Context_free.Rule.special_function"},{"bugid":969688,"firstseen":"2026-02-08T04:47:19.765604","severity":"normal","status":"CONFIRMED","summary":"sci-mathematics\/why3-1.8.2 - [portage-9999] is not a compiled interface for this version of OCaml."}],"categories":[{"categoryid":395,"name":"app-editors","summary":"The app-editors category contains text editors."},{"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":"aae9881664608ab9a11ddc73c200475c7f1c10fb","committime":"2025-10-08T17:33:43","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"88a4f3c9c582c4ae3578aabeb709e8242f04a70e","committime":"2025-10-08T17:20:42","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: dev-lang\/ocaml dep redundant"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"1457e472abc5b9dd0765d3ee3873a0139b948a9d","committime":"2025-09-27T22:03:35","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"8fec647a40c018c06d26cfd8e99ef9bea48e98d2","committime":"2025-09-27T19:05:42","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: bump to 1.8.2"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"d6f74dbde97dd647759382d108dcb00ac404126d","committime":"2025-07-09T22:07:23","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"8cdcd957839affdad84c14547197c1a786c6ebdd","committime":"2025-07-09T19:56:05","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: bump to 1.8.1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"67ee579bd6a9559b12ac87f2bb24110e00741695","committime":"2025-04-09T20:05:23","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/952926\nSigned-off-by: Alfredo Tupone ","commitid":"1ad8039363dd8397971f0ad9fd5b39f40e20102b","committime":"2025-04-09T19:57:24","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: fix with ocaml-5"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"339a0ad8228444a7438329b0a9658941c922f46f","committime":"2025-02-16T22:48:30","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"bc98757ac5ba4a262c44c5454109ce0424be3542","committime":"2025-02-16T22:13:07","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: bump to 1.8.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"2417548e5eb903a890aadc819a4741d0ed1c799c","committime":"2024-12-31T17:03:23","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"sam@gentoo.org","authorname":"Sam James","body":"Signed-off-by: Sam James ","commitid":"31463d3fe79d6abed444c7d01d11c55f1281eef6","committime":"2024-12-31T16:49:14","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: update HOMEPAGE"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"7e93b7ed5a9adfd9bd98ec4b425da05704995b48","committime":"2024-11-20T22:03:17","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Closes: https:\/\/bugs.gentoo.org\/944186\nSigned-off-by: Alfredo Tupone ","commitid":"4a95491d669ef0a95bc8a8c705aea5149e2f0148","committime":"2024-11-20T21:44:46","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: Fix sa_handler signature"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"c009c5eb4d2fd998fee7df3cf50e801c35197c90","committime":"2024-11-19T20:18:18","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"tupone@gentoo.org","authorname":"Alfredo Tupone","body":"Signed-off-by: Alfredo Tupone ","commitid":"9ed530debc4355d1141b61c2a8fabff35efc55c1","committime":"2024-11-19T20:03:01","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: add 1.7.2"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"3bb1911b194b46a11dec2ab18c8e2e05ba47dec7","committime":"2023-07-15T22:31:50","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"0eb41919c406dc8282d78c71cceb73e7ea1e284d","committime":"2023-07-15T21:52:36","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: drop old 1.5.1"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"8172b96a31be44514df28bdd63c866ce615f9790","committime":"2023-07-15T21:52:19","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: drop old 1.4.1-r1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"64bb5f74af3bc6dd3396d6f48a5f9a5e4ce4e8bc","committime":"2023-04-01T23:01:53","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"55c35b5dfb116b0619f48f6162afb4698b109891","committime":"2023-04-01T21:44:09","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: drop old 1.5.0-r1"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"c369073451a29ba37f806d8429a1e69cdc999745","committime":"2023-04-01T21:43:59","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: drop old 1.4.0-r3"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"ee8a6c729b7e0d802129ac020fba8b7b212c49f0","committime":"2023-04-01T21:43:46","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: bump to 1.6.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"da43512a196829132aee0b36b5c8fff946affc5e","committime":"2022-09-19T19:01:44","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"0e667f1eec8cf52339e41e209591281258574fc7","committime":"2022-09-19T18:44:26","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: bump to 1.5.1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"008b203d88f5dbde8f481606997d206192aef005","committime":"2022-07-26T20:01:41","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"mmk@levelnine.at","authorname":"Michael Mair-Keimberger","body":"Signed-off-by: Michael Mair-Keimberger \nPortage 3.0.34 \/ pkgdev 0.2.1 \/ pkgcheck 0.10.11\nSigned-off-by: Alfredo Tupone ","commitid":"5c16384ca80bcca7f7bf0b7d5926e8ef5d3867d9","committime":"2022-07-26T19:38:11","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: use https"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"80092c67228eadcee514719c3008aa9d05a143f6","committime":"2022-07-23T00:16:50","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Signed-off-by: Maciej Barć ","commitid":"28fa4c56bba04fe751e45cff07af6e2285bca741","committime":"2022-07-22T22:23:52","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: remove unnecessary seq dependency"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"0969191eb393098af56b89858d896357eabf3156","committime":"2022-05-07T17:03:02","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"fx.carton91@gmail.com","authorname":"François-Xavier Carton","body":"Signed-off-by: François-Xavier Carton \nCloses: https:\/\/github.com\/gentoo\/gentoo\/pull\/25372\nSigned-off-by: Maciej Barć ","commitid":"7a4a24d0168c9092f69cafa35ca1872d7e77e0de","committime":"2022-05-07T16:15:12","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: bump to 1.5.0"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"8536c68c8c7ef9e6ed44dd1703c4dc9d19bcdf8d","committime":"2022-04-16T21:38:44","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"this is a very minor change to keep it in sync with\nhttps:\/\/opam.ocaml.org\/packages\/why3\nalso, no bump is needed since 20170418 version\nis long gone from ::gentoo\n\nSigned-off-by: Maciej Barć ","commitid":"e0300e30cdf32fdb0d0ca67c9eb6c3e5e53e5bf3","committime":"2022-04-16T21:24:31","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: increase required menhir version"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"24bec2839d0a3c0eb611743b026001bddd949ef8","committime":"2022-03-04T11:21:58","packageid":73747,"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":"da140912911bef67070defaa18676a365f269cf2","committime":"2022-03-04T11:02:09","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: bump to 1.4.1"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"ffd67eca06a0d66cac36277865ac6575098befd1","committime":"2022-01-15T06:21:41","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"fx.carton91@gmail.com","authorname":"François-Xavier Carton","body":"\"make doc\" uses sphinx to build both latex and html documentation. Both\nsphinx rules in the makefile include \"-d doc\/.doctrees\", ie. the same\npath for \"the cached environment and doctree files\". In a parallel make\nbuild, the rules are called simulateously, which means the cached files\ncould be read by one process while they are still being written by the\nother.\n\nCloses: https:\/\/bugs.gentoo.org\/831168\nSigned-off-by: François-Xavier Carton \nCloses: https:\/\/github.com\/gentoo\/gentoo\/pull\/23802\nSigned-off-by: Maciej Barć ","commitid":"5377b0ede6969e3ce4b0c0b2b019b3835f5a7c62","committime":"2022-01-15T02:20:22","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: fix race condition in parallel make doc"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"17159f79bd15ad97af651d9ff72e76cbc585efc3","committime":"2022-01-13T16:51:42","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"fx.carton91@gmail.com","authorname":"François-Xavier Carton","body":"Closes: https:\/\/bugs.gentoo.org\/828997\nCloses: https:\/\/github.com\/gentoo\/gentoo\/pull\/23774\nSigned-off-by: François-Xavier Carton \nSigned-off-by: Maciej Barć ","commitid":"c87b6eaca316012d6da22935421b4279bd91b128","committime":"2022-01-12T22:34:35","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: add missing latex dependencies"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"af7ace6972ee6dd94fd40f5537452e3942410e48","committime":"2021-12-12T12:21:33","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Closes: https:\/\/bugs.gentoo.org\/828974\nPackage-Manager: Portage-3.0.28, Repoman-3.0.3\nSigned-off-by: Maciej Barć ","commitid":"61686012dfc33cda5b87f4726ffce518c68897dc","committime":"2021-12-12T12:13:18","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: fix *DEPEND"},{"authoremail":"repomirrorci@gentoo.org","authorname":"Repository mirror & CI","commitid":"9e642b2fe6a9ce63661616b43e40340ce24efc2d","committime":"2021-12-12T02:05:45","packageid":73747,"repoid":1,"summary":"Merge updates from master"},{"authoremail":"xgqt@gentoo.org","authorname":"Maciej Barć","body":"Move from ::guru to ::gentoo,\nadd François-Xavier Carton as a co-maintainer.\n\nPackage-Manager: Portage-3.0.28, Repoman-3.0.3\nSigned-off-by: Maciej Barć ","commitid":"afa23b7e71a8114ea0919675d3d4029f6d6b6176","committime":"2021-12-12T00:56:49","packageid":73747,"repoid":1,"summary":"sci-mathematics\/why3: new package; add version 1.4.0"}],"dependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[782878,845202,854230,869907,877153],"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":"OCaml bindings to GTK-3","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"lablgtk","packageid":43080},{"block":false,"categoryid":395,"description":"The advanced, extensible, customizable, self-documenting editor","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"gnu-emacs@gentoo.org","maintainername":"Gentoo GNU Emacs project","name":"emacs","packageid":45775,"summary":"GNU Emacs is an extensible, customizable text editor - and more. At its core is an interpreter for Emacs Lisp, a dialect of the Lisp programming language with extensions to support text editing. The features of GNU Emacs include: * Content-sensitive editing modes, including syntax coloring, for a variety of file types including plain text, source code, and HTML. * Complete built-in documentation, including a tutorial for new users. * Full Unicode support for nearly all human languages and their scripts. * Highly customizable, using Emacs Lisp code or a graphical interface. * A large number of extensions that add other functionality, including a project planner, mail and news reader, debugger interface, calendar, and more. Many of these extensions are distributed with GNU Emacs; others are available separately."},{"block":false,"categoryid":314,"description":"Compressed file access ML library (ZIP, GZIP and JAR)","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"camlzip","packageid":47766},{"block":false,"categoryid":314,"description":"Library for automated conversion of OCaml-values to and from S-expressions","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"sexplib","packageid":49507},{"block":false,"categoryid":314,"description":"OCaml tool to find\/use non-standard packages","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"findlib","packageid":51288},{"block":false,"categoryid":314,"description":"O'Caml Graph library","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocamlgraph","packageid":52838},{"block":false,"categoryid":314,"description":"LR(1) parser generator for the OCaml language","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2013-02-08T14:36:53.188287","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"menhir","packageid":60329},{"block":false,"categoryid":314,"description":"Arithmetic and logic operations over arbitrary-precision integers","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2015-09-20T13:38:44.780852","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"zarith","packageid":64116},{"block":false,"categoryid":314,"description":"Type-driven code generation for OCaml","ebuildids":[782878,845202,854230,869907,877153],"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":[782878,845202,854230,869907,877153],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_sexp_conv","packageid":64965},{"block":true,"categoryid":317,"description":"SPARK 2014 repository for the Why3 verification platform","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2017-10-19T20:17:41.724443","name":"why3-for-spark","packageid":68094,"summary":"Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs."},{"block":false,"categoryid":314,"description":"Library for arbitrary-precision integer and rational arithmetic","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2020-01-07T21:43:34.584399","name":"num","packageid":70574},{"block":false,"categoryid":314,"description":"Regular expression library for OCaml","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2020-10-13T14:25:05.132759","name":"re","packageid":72119},{"block":false,"categoryid":317,"description":"Formalization of floating-point arithmetic for the Coq proof assistant","ebuildids":[854230,869907,877153],"firstseen":"2022-12-24T22:51:22.910451","name":"flocq","packageid":75711,"summary":"Flocq (Floats for Coq) is a formalization of floating-point arithmetic for the Coq proof assistant. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq."}],"depending":[{"block":false,"categoryid":317,"description":"Computer-Aided Cryptographic Proofs","ebuildids":[878108,878108,882277,882277,893517,893517],"firstseen":"2021-12-12T02:08:52.137547","name":"easycrypt","packageid":73746,"summary":"EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs."}],"ebuilds":[{"archs":["~amd64"],"ebuildid":877153,"firstseen":"2025-09-27T23:11:00.142559","license":"LGPL-2","moddate":"2026-03-22T20:20:57","packageid":73747,"repoid":1,"slot":"0\/1.8.2","uses":["coq","doc","emacs","gtk","ocamlopt","re","sexp","stackify","zip"],"version":"1.8.2"},{"archs":["~amd64"],"ebuildid":869907,"firstseen":"2025-07-09T23:20:47.558299","license":"LGPL-2","moddate":"2026-03-22T20:20:57","packageid":73747,"repoid":1,"slot":"0\/1.8.1","uses":["coq","doc","emacs","gtk","ocamlopt","re","sexp","stackify","zip"],"version":"1.8.1"},{"archs":["~amd64"],"ebuildid":854230,"firstseen":"2025-02-16T22:50:58.717736","license":"LGPL-2","moddate":"2026-03-22T20:20:57","packageid":73747,"repoid":1,"slot":"0\/1.8.0","uses":["coq","doc","emacs","gtk","ocamlopt","re","sexp","stackify","zip"],"version":"1.8.0"},{"archs":["~amd64"],"ebuildid":845202,"firstseen":"2024-11-19T20:32:25.040327","license":"LGPL-2","moddate":"2026-03-22T20:20:57","packageid":73747,"repoid":1,"slot":"0\/1.7.2","uses":["coq","doc","emacs","gtk","ocamlopt","re","sexp","stackify","zarith","zip"],"version":"1.7.2"},{"archs":["~amd64"],"ebuildid":782878,"firstseen":"2023-04-02T00:20:14.321206","license":"LGPL-2","moddate":"2026-03-22T20:20:57","packageid":73747,"repoid":1,"slot":"0\/1.6.0","uses":["coq","doc","emacs","gtk","ocamlopt","re","sexp","stackify","zarith","zip"],"version":"1.6.0"}],"masks":[],"package":{"categoryid":317,"description":"Platform for deductive program verification","firstseen":"2021-12-12T02:08:52.137547","name":"why3","packageid":73747,"summary":"Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs."},"rdependencies":[{"block":false,"categoryid":317,"description":"Coq\/Rocq is a proof assistant written in O'Caml","ebuildids":[782878,845202,854230,869907,877153],"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":"OCaml bindings to GTK-3","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"lablgtk","packageid":43080},{"block":false,"categoryid":395,"description":"The advanced, extensible, customizable, self-documenting editor","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"gnu-emacs@gentoo.org","maintainername":"Gentoo GNU Emacs project","name":"emacs","packageid":45775,"summary":"GNU Emacs is an extensible, customizable text editor - and more. At its core is an interpreter for Emacs Lisp, a dialect of the Lisp programming language with extensions to support text editing. The features of GNU Emacs include: * Content-sensitive editing modes, including syntax coloring, for a variety of file types including plain text, source code, and HTML. * Complete built-in documentation, including a tutorial for new users. * Full Unicode support for nearly all human languages and their scripts. * Highly customizable, using Emacs Lisp code or a graphical interface. * A large number of extensions that add other functionality, including a project planner, mail and news reader, debugger interface, calendar, and more. Many of these extensions are distributed with GNU Emacs; others are available separately."},{"block":false,"categoryid":314,"description":"Compressed file access ML library (ZIP, GZIP and JAR)","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"camlzip","packageid":47766},{"block":false,"categoryid":314,"description":"Library for automated conversion of OCaml-values to and from S-expressions","ebuildids":[782878,845202,854230,869907,877153],"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":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":314,"description":"O'Caml Graph library","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocamlgraph","packageid":52838},{"block":false,"categoryid":314,"description":"LR(1) parser generator for the OCaml language","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2013-02-08T14:36:53.188287","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"menhir","packageid":60329},{"block":false,"categoryid":314,"description":"Arithmetic and logic operations over arbitrary-precision integers","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2015-09-20T13:38:44.780852","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"zarith","packageid":64116},{"block":false,"categoryid":314,"description":"Type-driven code generation for OCaml","ebuildids":[782878,845202,854230,869907,877153],"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":[782878,845202,854230,869907,877153],"firstseen":"2016-02-06T14:40:36.761342","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ppx_sexp_conv","packageid":64965},{"block":true,"categoryid":317,"description":"SPARK 2014 repository for the Why3 verification platform","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2017-10-19T20:17:41.724443","name":"why3-for-spark","packageid":68094,"summary":"Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs."},{"block":false,"categoryid":314,"description":"Library for arbitrary-precision integer and rational arithmetic","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2020-01-07T21:43:34.584399","name":"num","packageid":70574},{"block":false,"categoryid":314,"description":"Regular expression library for OCaml","ebuildids":[782878,845202,854230,869907,877153],"firstseen":"2020-10-13T14:25:05.132759","name":"re","packageid":72119},{"block":false,"categoryid":317,"description":"Formalization of floating-point arithmetic for the Coq proof assistant","ebuildids":[854230,869907,877153],"firstseen":"2022-12-24T22:51:22.910451","name":"flocq","packageid":75711,"summary":"Flocq (Floats for Coq) is a formalization of floating-point arithmetic for the Coq proof assistant. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq."}],"repos":[{"branch":"master","lastcommit":"43a4988e0fa15f038220ebd74aa888ace0c9b303","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["https:\/\/gitlab.inria.fr\/why3\/why3\/","https:\/\/www.why3.org\/"],"uses":[{"description":"Add sci-mathematics\/coq support","isdefault":false,"packageid":73747,"use":"coq"},{"description":"Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally","isdefault":false,"use":"doc"},{"description":"Add support for GNU Emacs","isdefault":false,"use":"emacs"},{"description":"Build the IDE x11-libs\/gtk+","isdefault":false,"packageid":73747,"use":"gtk"},{"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":"Use Re (dev-ml\/re) instead of Str for regular expressions","isdefault":false,"packageid":73747,"use":"re"},{"description":"Add support for outputting S-expressions with dev-ml\/ppx_sexp_conv","isdefault":false,"packageid":73747,"use":"sexp"},{"description":"Enable structure reconstruction algorithm for MLCFG","isdefault":false,"packageid":73747,"use":"stackify"},{"defaultflag":true,"description":"Use Zarith (dev-ml\/zarith) instead of Nums (dev-ml\/num) for computations","isdefault":true,"packageid":73747,"use":"zarith"},{"description":"Enable compression of session files","isdefault":false,"packageid":73747,"use":"zip"}]}