[gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/why3/

2021-12-15 Thread Andrew Ammerlaan 
commit: d6f443bcf23ca2f4f6e583bd02a79fadcb1c1875
Author: Andrew Ammerlaan  gentoo  org>
AuthorDate: Wed Dec 15 10:32:13 2021 +
Commit: Andrew Ammerlaan  gentoo  org>
CommitDate: Wed Dec 15 10:35:02 2021 +
URL:https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=d6f443bc

sci-mathematics/why3: moved to ::gentoo

Signed-off-by: Andrew Ammerlaan  gentoo.org>

 sci-mathematics/why3/Manifest  |  2 -
 sci-mathematics/why3/metadata.xml  | 28 ---
 sci-mathematics/why3/why3-1.3.3.ebuild | 83 
 sci-mathematics/why3/why3-1.4.0.ebuild | 86 --
 4 files changed, 199 deletions(-)

diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
deleted file mode 100644
index 9987a255a..0
--- a/sci-mathematics/why3/Manifest
+++ /dev/null
@@ -1,2 +0,0 @@
-DIST why3-1.3.3.tar.gz 5807572 BLAKE2B 
b1a04e78010f841e217b9a81c096cadfa0cddabadbe81ef55c310a104668feb1e46cd50576a965a58c74658903d6d08f9fd348bd2064a79ac3b176548927bcbe
 SHA512 
a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce
-DIST why3-1.4.0.tar.gz 6306524 BLAKE2B 
ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5
 SHA512 
b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a

diff --git a/sci-mathematics/why3/metadata.xml 
b/sci-mathematics/why3/metadata.xml
deleted file mode 100644
index d64bca822..0
--- a/sci-mathematics/why3/metadata.xml
+++ /dev/null
@@ -1,28 +0,0 @@
-
-http://www.gentoo.org/dtd/metadata.dtd;>
-
-   
-   François-Xavier Carton
-   fx.carto...@gmail.com
-   
-   
-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.
-
-   
-   Add sci-mathematics/coq 
support
-   Build the IDE x11-libs/gtk+
-   Use Re (dev-ml/re) instead of Str 
for regular expressions
-   Add support for outputting S-expressions with 
dev-ml/ppx_sexp_conv
-   Use Zarith (dev-ml/zarith) 
instead of Nums (dev-ml/num) for computations
-   Enable compression of session files
-   
-

diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild 
b/sci-mathematics/why3/why3-1.3.3.ebuild
deleted file mode 100644
index 89ff253ff..0
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ /dev/null
@@ -1,83 +0,0 @@
-# Copyright 1999-2020 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/;
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz;
-
-LICENSE="LGPL-2"
-SLOT="0"
-KEYWORDS="~amd64"
-IUSE="coq emacs gtk +ocamlopt re +zarith zip"
-
-DEPEND=">=dev-lang/ocaml-4.05.0[ocamlopt?]
-   >=dev-ml/menhir-20151112
-   dev-ml/num
-   coq? ( >=sci-mathematics/coq-8.6 )
-   emacs? ( app-editors/emacs:* )
-   gtk? ( dev-ml/lablgtk:*[sourceview,ocamlopt?] )
-   re? ( dev-ml/re dev-ml/seq )
-   zarith? ( dev-ml/zarith )
-   zip? ( dev-ml/camlzip )"
-RDEPEND="${DEPEND}"
-
-# doc needs sphinxcontrib-bibtex which is currently not packaged
-#  doc? (
-#  dev-python/sphinx
-#  dev-python/sphinxcontrib-bibtex
-#  || ( dev-texlive/texlive-latex dev-tex/latexmk 
dev-tex/rubber )
-#  )
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
-   mv doc/why.1 doc/why3.1 || die
-   mv configure.in configure.ac || die
-   sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
-   sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
-   -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
-   -i Makefile.in || die
-   eautoreconf
-   eapply_user
-}
-
-src_configure() {
-   econf \
-   --disable-hypothesis-selection \
-   --disable-pvs-libs \
-   --disable-isabelle-libs \
-   --disable-frama-c \
-   --disable-web-ide \
-   --disable-doc \

[gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/why3/

2021-10-01 Thread Francois-Xavier Carton 
commit: 4962103953030be5b8f12c33f6ff110952fb6e06
Author: François-Xavier Carton  gmail  com>
AuthorDate: Fri Oct  1 13:07:43 2021 +
Commit: Francois-Xavier Carton  gmail  com>
CommitDate: Fri Oct  1 13:07:43 2021 +
URL:https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=49621039

sci-mathematics/why3: update SRC_URI

Signed-off-by: François-Xavier Carton  gmail.com>

 sci-mathematics/why3/why3-1.3.3.ebuild | 2 +-
 sci-mathematics/why3/why3-1.4.0.ebuild | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild 
b/sci-mathematics/why3/why3-1.3.3.ebuild
index 75f796891..89ff253ff 100644
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -7,7 +7,7 @@ inherit autotools findlib
 
 DESCRIPTION="Platform for deductive program verification"
 HOMEPAGE="http://why3.lri.fr/;
-SRC_URI="https://gforge.inria.fr/frs/download.php/file/38367/${P}.tar.gz;
+SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz;
 
 LICENSE="LGPL-2"
 SLOT="0"

diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild 
b/sci-mathematics/why3/why3-1.4.0.ebuild
index 9174013f3..cce31164b 100644
--- a/sci-mathematics/why3/why3-1.4.0.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0.ebuild
@@ -7,7 +7,7 @@ inherit autotools findlib
 
 DESCRIPTION="Platform for deductive program verification"
 HOMEPAGE="http://why3.lri.fr/;
-SRC_URI="https://gforge.inria.fr/frs/download.php/file/38425/${P}.tar.gz;
+SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz;
 
 LICENSE="LGPL-2"
 SLOT="0"

[gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/why3/

2021-09-04 Thread Francois-Xavier Carton 
commit: 6bd2366827c2e9dbd72d601651bb8348bdb7b04c
Author: François-Xavier Carton  gmail  com>
AuthorDate: Sat Sep  4 12:53:29 2021 +
Commit: Francois-Xavier Carton  gmail  com>
CommitDate: Sat Sep  4 13:07:40 2021 +
URL:https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=6bd23668

sci-mathematics/why3: no need to die with emake

Signed-off-by: François-Xavier Carton  gmail.com>

 sci-mathematics/why3/why3-1.3.3.ebuild | 2 +-
 sci-mathematics/why3/why3-1.4.0.ebuild | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild 
b/sci-mathematics/why3/why3-1.3.3.ebuild
index efe7c0d1a..75f796891 100644
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -70,7 +70,7 @@ src_compile() {
 
 src_install(){
findlib_src_preinst
-   emake install install-lib DESTDIR="${ED}" || die "make failed"
+   emake install install-lib DESTDIR="${ED}"
 
doman doc/why3.1
einstalldocs

diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild 
b/sci-mathematics/why3/why3-1.4.0.ebuild
index 0c41a284e..9174013f3 100644
--- a/sci-mathematics/why3/why3-1.4.0.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0.ebuild
@@ -74,7 +74,7 @@ src_compile() {
 
 src_install(){
findlib_src_preinst
-   emake install install-lib DESTDIR="${ED}" || die "make failed"
+   emake install install-lib DESTDIR="${ED}"
 
einstalldocs
docompress -x /usr/share/doc/${PF}/examples

[gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/why3/, sci-mathematics/frama-c/

2021-05-02 Thread Anna Vyalkova 
commit: 673dc2eb7385a3583a72f665bbf26298fbdc0649
Author: Anna Vyalkova  sysrq  in>
AuthorDate: Sun May  2 01:14:55 2021 +
Commit: Anna Vyalkova  sysrq  in>
CommitDate: Sun May  2 02:19:40 2021 +
URL:https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=673dc2eb

sci-mathematics/*: inherit findlib eclass

Closes: https://bugs.gentoo.org/784677
Closes: https://bugs.gentoo.org/784671
Signed-off-by: Anna Vyalkova  sysrq.in>

 sci-mathematics/frama-c/frama-c-22.0.ebuild | 7 +--
 sci-mathematics/why3/why3-1.3.3.ebuild  | 6 +++---
 sci-mathematics/why3/why3-1.4.0.ebuild  | 6 +++---
 3 files changed, 7 insertions(+), 12 deletions(-)

diff --git a/sci-mathematics/frama-c/frama-c-22.0.ebuild 
b/sci-mathematics/frama-c/frama-c-22.0.ebuild
index da4cb7ef4..cb0c8334c 100644
--- a/sci-mathematics/frama-c/frama-c-22.0.ebuild
+++ b/sci-mathematics/frama-c/frama-c-22.0.ebuild
@@ -3,7 +3,7 @@
 
 EAPI=7
 
-inherit autotools
+inherit autotools findlib
 
 DESCRIPTION="Framework for analysis of source codes written in C"
 HOMEPAGE="https://frama-c.com;
@@ -26,7 +26,6 @@ RDEPEND="
gtk? ( >=dev-ml/lablgtk-2.14:2=[sourceview,gnomecanvas,ocamlopt?] )
wp? ( ~sci-mathematics/why3-1.3.3 )"
 DEPEND="${RDEPEND}
-   dev-ml/findlib
media-gfx/graphviz"
 
 REQUIRED_USE="
@@ -97,7 +96,3 @@ src_configure() {
$(use_enable wp) \
--disable-wp-coq
 }
-
-src_install() {
-   emake install DESTDIR="${ED}"
-}

diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild 
b/sci-mathematics/why3/why3-1.3.3.ebuild
index b710f8a1a..efe7c0d1a 100644
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -3,7 +3,7 @@
 
 EAPI=7
 
-inherit autotools
+inherit autotools findlib
 
 DESCRIPTION="Platform for deductive program verification"
 HOMEPAGE="http://why3.lri.fr/;
@@ -16,7 +16,6 @@ IUSE="coq emacs gtk +ocamlopt re +zarith zip"
 
 DEPEND=">=dev-lang/ocaml-4.05.0[ocamlopt?]
>=dev-ml/menhir-20151112
-   dev-ml/findlib
dev-ml/num
coq? ( >=sci-mathematics/coq-8.6 )
emacs? ( app-editors/emacs:* )
@@ -70,7 +69,8 @@ src_compile() {
 }
 
 src_install(){
-   emake install install-lib DESTDIR="${ED}"
+   findlib_src_preinst
+   emake install install-lib DESTDIR="${ED}" || die "make failed"
 
doman doc/why3.1
einstalldocs

diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild 
b/sci-mathematics/why3/why3-1.4.0.ebuild
index 7a1ab9ca4..0c41a284e 100644
--- a/sci-mathematics/why3/why3-1.4.0.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0.ebuild
@@ -3,7 +3,7 @@
 
 EAPI=7
 
-inherit autotools
+inherit autotools findlib
 
 DESCRIPTION="Platform for deductive program verification"
 HOMEPAGE="http://why3.lri.fr/;
@@ -16,7 +16,6 @@ IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
 
 DEPEND=">=dev-lang/ocaml-4.05.0[ocamlopt?]
>=dev-ml/menhir-20151112
-   dev-ml/findlib
dev-ml/num
coq? ( >=sci-mathematics/coq-8.6 )
doc? (
@@ -74,7 +73,8 @@ src_compile() {
 }
 
 src_install(){
-   emake install install-lib DESTDIR="${ED}"
+   findlib_src_preinst
+   emake install install-lib DESTDIR="${ED}" || die "make failed"
 
einstalldocs
docompress -x /usr/share/doc/${PF}/examples

[gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/why3/

2021-04-18 Thread Francois-Xavier Carton 
commit: 556d223d1e4531cb91e44a21bba602ac92f2a25d
Author: François-Xavier Carton  gmail  com>
AuthorDate: Mon Apr 19 01:03:43 2021 +
Commit: Francois-Xavier Carton  gmail  com>
CommitDate: Mon Apr 19 01:15:31 2021 +
URL:https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=556d223d

sci-mathematics/why3: respect CFLAGS & LDFLAGS

Closes: https://bugs.gentoo.org/781650
Signed-off-by: François-Xavier Carton  gmail.com>

 sci-mathematics/why3/why3-1.3.3.ebuild | 3 +++
 sci-mathematics/why3/why3-1.4.0.ebuild | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild 
b/sci-mathematics/why3/why3-1.3.3.ebuild
index b5665dc3a..b710f8a1a 100644
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -39,6 +39,9 @@ src_prepare() {
mv doc/why.1 doc/why3.1 || die
mv configure.in configure.ac || die
sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+   sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
+   -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+   -i Makefile.in || die
eautoreconf
eapply_user
 }

diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild 
b/sci-mathematics/why3/why3-1.4.0.ebuild
index d85c95cfc..7a1ab9ca4 100644
--- a/sci-mathematics/why3/why3-1.4.0.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0.ebuild
@@ -41,6 +41,9 @@ DOCS=( CHANGES.md README.md )
 src_prepare() {
mv configure.in configure.ac || die
sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+   sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
+   -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+   -i Makefile.in || die
eautoreconf
eapply_user
 }

[gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/why3/

2021-03-30 Thread Francois-Xavier Carton 
commit: 42c0da6a668a33653427f8b8ff93073a189819c7
Author: François-Xavier Carton  gmail  com>
AuthorDate: Tue Mar 30 19:32:21 2021 +
Commit: Francois-Xavier Carton  gmail  com>
CommitDate: Tue Mar 30 19:32:21 2021 +
URL:https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=42c0da6a

sci-mathematics/why3: bump to 1.4.0

Signed-off-by: François-Xavier Carton  gmail.com>

 sci-mathematics/why3/Manifest  |  1 +
 sci-mathematics/why3/metadata.xml  |  1 +
 sci-mathematics/why3/why3-1.4.0.ebuild | 83 ++
 3 files changed, 85 insertions(+)

diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index 20a390e40..9987a255a 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1 +1,2 @@
 DIST why3-1.3.3.tar.gz 5807572 BLAKE2B 
b1a04e78010f841e217b9a81c096cadfa0cddabadbe81ef55c310a104668feb1e46cd50576a965a58c74658903d6d08f9fd348bd2064a79ac3b176548927bcbe
 SHA512 
a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce
+DIST why3-1.4.0.tar.gz 6306524 BLAKE2B 
ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5
 SHA512 
b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a

diff --git a/sci-mathematics/why3/metadata.xml 
b/sci-mathematics/why3/metadata.xml
index 444f26b5b..008bf6030 100644
--- a/sci-mathematics/why3/metadata.xml
+++ b/sci-mathematics/why3/metadata.xml
@@ -21,6 +21,7 @@ language for the verification of C, Java, or Ada programs.
Add sci-mathematics/coq 
support
Build the IDE x11-libs/gtk+
Use Re (dev-ml/re) instead of Str 
for regular expressions
+   Add support for outputting S-expressions with 
dev-ml/ppx_sexp_conv
Use Zarith (dev-ml/zarith) 
instead of Nums (dev-ml/num) for computations
Enable compression of session files


diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild 
b/sci-mathematics/why3/why3-1.4.0.ebuild
new file mode 100644
index 0..d85c95cfc
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.4.0.ebuild
@@ -0,0 +1,83 @@
+# Copyright 1999-2020 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+inherit autotools
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/;
+SRC_URI="https://gforge.inria.fr/frs/download.php/file/38425/${P}.tar.gz;
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64"
+IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
+
+DEPEND=">=dev-lang/ocaml-4.05.0[ocamlopt?]
+   >=dev-ml/menhir-20151112
+   dev-ml/findlib
+   dev-ml/num
+   coq? ( >=sci-mathematics/coq-8.6 )
+   doc? (
+   dev-python/sphinx
+   dev-python/sphinxcontrib-bibtex
+   || ( dev-texlive/texlive-latex dev-tex/latexmk 
dev-tex/rubber )
+   )
+   emacs? ( app-editors/emacs:* )
+   gtk? ( dev-ml/lablgtk:*[sourceview,ocamlopt?] )
+   re? ( dev-ml/re dev-ml/seq )
+   sexp? (
+   dev-ml/ppx_deriving[ocamlopt?]
+   dev-ml/ppx_sexp_conv[ocamlopt?]
+   dev-ml/sexplib[ocamlopt?]
+   )
+   zarith? ( dev-ml/zarith )
+   zip? ( dev-ml/camlzip )"
+RDEPEND="${DEPEND}"
+
+DOCS=( CHANGES.md README.md )
+
+src_prepare() {
+   mv configure.in configure.ac || die
+   sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+   eautoreconf
+   eapply_user
+}
+
+src_configure() {
+   econf \
+   --disable-hypothesis-selection \
+   --disable-pvs-libs \
+   --disable-isabelle-libs \
+   --disable-frama-c \
+   --disable-infer \
+   --disable-web-ide \
+   $(use_enable coq coq-libs) \
+   $(use_enable doc) \
+   $(use_enable emacs emacs-compilation) \
+   $(use_enable gtk ide) \
+   $(use_enable ocamlopt native-code) \
+   $(use_enable re) \
+   $(use_enable sexp pp-sexp) \
+   $(use_enable zarith) \
+   $(use_enable zip)
+}
+
+src_compile() {
+   emake
+   emake plugins
+   use doc && emake doc
+}
+
+src_install(){
+   emake install install-lib DESTDIR="${ED}"
+
+   einstalldocs
+   docompress -x /usr/share/doc/${PF}/examples
+   dodoc -r examples
+   if use doc; then
+   dodoc doc/latex/manual.pdf
+   dodoc -r doc/html
+   fi
+}

[gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/why3/

2021-01-09 Thread Francois-Xavier Carton 
commit: 8774c3bacb82b878b97365d5c3c9764c1d38ae8a
Author: François-Xavier Carton  gmail  com>
AuthorDate: Fri Nov 27 18:16:28 2020 +
Commit: Francois-Xavier Carton  gmail  com>
CommitDate: Sat Jan  9 16:44:42 2021 +
URL:https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=8774c3ba

sci-mathematics/why3: new package

This is a bump from the version in ::science.

Signed-off-by: François-Xavier Carton  gmail.com>

 sci-mathematics/why3/Manifest  |  1 +
 sci-mathematics/why3/metadata.xml  | 27 
 sci-mathematics/why3/why3-1.3.3.ebuild | 80 ++
 3 files changed, 108 insertions(+)

diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
new file mode 100644
index ..20a390e4
--- /dev/null
+++ b/sci-mathematics/why3/Manifest
@@ -0,0 +1 @@
+DIST why3-1.3.3.tar.gz 5807572 BLAKE2B 
b1a04e78010f841e217b9a81c096cadfa0cddabadbe81ef55c310a104668feb1e46cd50576a965a58c74658903d6d08f9fd348bd2064a79ac3b176548927bcbe
 SHA512 
a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce

diff --git a/sci-mathematics/why3/metadata.xml 
b/sci-mathematics/why3/metadata.xml
new file mode 100644
index ..444f26b5
--- /dev/null
+++ b/sci-mathematics/why3/metadata.xml
@@ -0,0 +1,27 @@
+
+http://www.gentoo.org/dtd/metadata.dtd;>
+
+   
+   François-Xavier Carton
+   fx.carto...@gmail.com
+   
+   
+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.
+
+   
+   Add sci-mathematics/coq 
support
+   Build the IDE x11-libs/gtk+
+   Use Re (dev-ml/re) instead of Str 
for regular expressions
+   Use Zarith (dev-ml/zarith) 
instead of Nums (dev-ml/num) for computations
+   Enable compression of session files
+   
+

diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild 
b/sci-mathematics/why3/why3-1.3.3.ebuild
new file mode 100644
index ..b5665dc3
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -0,0 +1,80 @@
+# Copyright 1999-2020 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+inherit autotools
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/;
+SRC_URI="https://gforge.inria.fr/frs/download.php/file/38367/${P}.tar.gz;
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64"
+IUSE="coq emacs gtk +ocamlopt re +zarith zip"
+
+DEPEND=">=dev-lang/ocaml-4.05.0[ocamlopt?]
+   >=dev-ml/menhir-20151112
+   dev-ml/findlib
+   dev-ml/num
+   coq? ( >=sci-mathematics/coq-8.6 )
+   emacs? ( app-editors/emacs:* )
+   gtk? ( dev-ml/lablgtk:*[sourceview,ocamlopt?] )
+   re? ( dev-ml/re dev-ml/seq )
+   zarith? ( dev-ml/zarith )
+   zip? ( dev-ml/camlzip )"
+RDEPEND="${DEPEND}"
+
+# doc needs sphinxcontrib-bibtex which is currently not packaged
+#  doc? (
+#  dev-python/sphinx
+#  dev-python/sphinxcontrib-bibtex
+#  || ( dev-texlive/texlive-latex dev-tex/latexmk 
dev-tex/rubber )
+#  )
+
+DOCS=( CHANGES.md README.md )
+
+src_prepare() {
+   mv doc/why.1 doc/why3.1 || die
+   mv configure.in configure.ac || die
+   sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+   eautoreconf
+   eapply_user
+}
+
+src_configure() {
+   econf \
+   --disable-hypothesis-selection \
+   --disable-pvs-libs \
+   --disable-isabelle-libs \
+   --disable-frama-c \
+   --disable-web-ide \
+   --disable-doc \
+   $(use_enable coq coq-libs) \
+   $(use_enable emacs emacs-compilation) \
+   $(use_enable gtk ide) \
+   $(use_enable ocamlopt native-code) \
+   $(use_enable re) \
+   $(use_enable zarith) \
+   $(use_enable zip)
+}
+
+src_compile() {
+   emake
+   emake plugins
+   #use doc && emake doc
+}
+
+src_install(){
+   emake install install-lib DESTDIR="${ED}"
+
+   doman doc/why3.1
+   einstalldocs
+   docompress -x /usr/share/doc/${PF}/examples
+   dodoc -r examples
+