{"bugs":[{"bugid":906225,"firstseen":"2023-05-12T22:46:18.951171","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":"2024-08-10T16:03:26.816139","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":"2024-12-16T20:47:28.996197","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."}],"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":"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":"Proof assistant written in O'Caml","ebuildids":[782878,845202],"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],"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 extensible, customizable, self-documenting real-time display editor","ebuildids":[782878,845202],"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],"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],"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],"firstseen":"2010-05-04T00:54:45.661860","maintainer":"ml@gentoo.org","maintainername":"Gentoo ML Project","name":"ocaml","packageid":49590},{"block":false,"categoryid":314,"description":"OCaml tool to find\/use non-standard packages","ebuildids":[782878,845202],"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],"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],"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],"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],"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],"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":"Platform for deductive program verification","ebuildids":[782878,845202],"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],"firstseen":"2020-01-07T21:43:34.584399","name":"num","packageid":70574},{"block":false,"categoryid":314,"description":"Regular expression library for OCaml","ebuildids":[782878,845202],"firstseen":"2020-10-13T14:25:05.132759","name":"re","packageid":72119}],"depending":[{"block":false,"categoryid":317,"description":"Computer-Aided Cryptographic Proofs","ebuildids":[831604,831604,840165,840165],"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":845202,"firstseen":"2024-11-19T20:32:25.040327","license":"LGPL-2","moddate":"2024-12-31T17:05:05","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":"2024-12-31T17:05:05","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":"Proof assistant written in O'Caml","ebuildids":[782878,845202],"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],"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 extensible, customizable, self-documenting real-time display editor","ebuildids":[782878,845202],"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],"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],"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,782878,845202,845202],"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],"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],"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],"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],"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],"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":"Platform for deductive program verification","ebuildids":[782878,845202],"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],"firstseen":"2020-01-07T21:43:34.584399","name":"num","packageid":70574},{"block":false,"categoryid":314,"description":"Regular expression library for OCaml","ebuildids":[782878,845202],"firstseen":"2020-10-13T14:25:05.132759","name":"re","packageid":72119}],"repos":[{"branch":"master","lastcommit":"a83e0f67258fb5642780f267a63ba59ea17dcd69","name":"gentoo","path":"\/usr\/portage","repoid":1,"upstream":"origin"}],"tracked":false,"urls":["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"}]}