From 42c0da6a668a33653427f8b8ff93073a189819c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois-Xavier=20Carton?= <fx.carton91@gmail.com>
Date: Tue, 30 Mar 2021 21:32:21 +0200
Subject: [PATCH] sci-mathematics/why3: bump to 1.4.0
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: François-Xavier Carton <fx.carton91@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(+)
 create mode 100644 sci-mathematics/why3/why3-1.4.0.ebuild

diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index 20a390e40b..9987a255a7 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 444f26b5b6..008bf60307 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.
 		<flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag>
 		<flag name="gtk">Build the IDE <pkg>x11-libs/gtk+</pkg></flag>
 		<flag name="re">Use Re (<pkg>dev-ml/re</pkg>) instead of Str for regular expressions</flag>
+		<flag name="sexp">Add support for outputting S-expressions with <pkg>dev-ml/ppx_sexp_conv</pkg></flag>
 		<flag name="zarith">Use Zarith (<pkg>dev-ml/zarith</pkg>) instead of Nums (<pkg>dev-ml/num</pkg>) for computations</flag>
 		<flag name="zip">Enable compression of session files</flag>
 	</use>
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 0000000000..d85c95cfc6
--- /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
+}