[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     132e6e560929e0b0f4df7d56fbc7d1fc223ac64a
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Sat Nov 26 13:44:45 2022 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Sat Nov 26 13:46:56 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=132e6e56

sci-mathematics/why3-for-spark: stop using <sci-mathematics/coq-8.12

Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild | 5 ++---
 sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild    | 8 ++------
 2 files changed, 4 insertions(+), 9 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
index bc975bd21a6b..f83359f0ee7e 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
@@ -13,14 +13,13 @@ SRC_URI="http://mirrors.cdn.adacore.com/art/5cdf915d31e87a8f1c967d54
 LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="amd64"
-IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt zarith zip"
+IUSE="doc emacs gtk html hypothesis-selection +ocamlopt zarith zip"
 RESTRICT="strip"
 
 DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=]
 	>=dev-ml/ocamlbuild-0.14.0
 	<=dev-ml/menhir-20190924:=
 	dev-ml/num:=
-	coq? ( >=sci-mathematics/coq-8.9.1 )
 	doc? ( dev-tex/rubber )
 	gtk? ( >=dev-ml/lablgtk-2.18.8:=[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
@@ -73,7 +72,7 @@ src_configure() {
 		--disable-pvs-libs \
 		--disable-isabelle-libs \
 		--enable-verbose-make \
-		$(use_enable coq coq-libs) \
+		--disable-coq-libs \
 		$(use_enable doc) \
 		$(use_enable emacs emacs-compilation) \
 		$(use_enable gtk ide) \

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
index 9075ebf3e9da..66a760496a92 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
@@ -14,7 +14,7 @@ SRC_URI="https://community.download.adacore.com/v1/8bb5801e17b8b23453262da69c981
 LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk html +ocamlopt zarith zip"
+IUSE="doc emacs gtk html +ocamlopt zarith zip"
 RESTRICT="strip"
 
 DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=]
@@ -22,10 +22,6 @@ DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=]
 	dev-ml/menhir:=
 	<dev-ml/num-1.4:=
 	dev-ml/yojson:=
-	coq? (
-		>=sci-mathematics/coq-8.9.1
-		<sci-mathematics/coq-8.12
-	)
 	doc? (
 		dev-tex/rubber
 		dev-python/sphinx
@@ -80,7 +76,7 @@ src_configure() {
 		--disable-pvs-libs \
 		--disable-isabelle-libs \
 		--enable-verbose-make \
-		$(use_enable coq coq-libs) \
+		--disable-coq-libs \
 		$(use_enable doc) \
 		$(use_enable emacs emacs-compilation) \
 		$(use_enable gtk ide) \

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     d58c273f2681691ec5eaf8101e35730a2b9bc2e8
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Fri Dec 29 22:42:59 2023 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Fri Dec 29 22:43:55 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=d58c273f

sci-mathematics/why3-for-spark: require ocamlopt

Closes: https://bugs.gentoo.org/913497
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
index 4204da3000b6..84d6fc56c009 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
@@ -21,8 +21,8 @@ RESTRICT="strip"
 
 RDEPEND="
 	>=dev-lang/ocaml-4.11:=[ocamlopt?]
-	dev-ml/menhir:=
-	dev-ml/num:=
+	dev-ml/menhir:=[ocamlopt?]
+	dev-ml/num:=[ocamlopt?]
 	dev-ml/yojson:=
 	coq? ( sci-mathematics/coq )
 	emacs? ( app-editors/emacs:* )
@@ -34,8 +34,8 @@ RDEPEND="
 		dev-ml/ppx_sexp_conv:=[ocamlopt?]
 		dev-ml/sexplib:=[ocamlopt?]
 	)
-	zarith? ( dev-ml/zarith:= )
-	zip? ( dev-ml/camlzip:= )
+	zarith? ( dev-ml/zarith:=[ocamlopt?] )
+	zip? ( dev-ml/camlzip:=[ocamlopt?] )
 "
 DEPEND="${RDEPEND}"
 BDEPEND="
@@ -69,7 +69,8 @@ QA_FLAGS_IGNORED=(
 	/usr/bin/why3ide.cmxs
 )
 
-REQUIRED_USE="html? ( doc )"
+# Forcing native for bug #913497
+REQUIRED_USE="html? ( doc ) ocamlopt"
 
 src_prepare() {
 	find examples -name \*gz | xargs gunzip

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     2dd73ad05b6f04585994edc2ff4b79638ab28850
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Sun Apr  2 13:20:59 2023 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Sun Apr  2 13:21:16 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2dd73ad0

sci-mathematics/why3-for-spark: stabilize 2021-r1 for amd64

Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
index 0801160e66e9..10f8a95c8393 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
@@ -15,7 +15,7 @@ SRC_URI="${ADAMIRROR}/${ID}?filename=${MYP}.tar.gz -> ${MYP}.tar.gz"
 
 LICENSE="GPL-3"
 SLOT="0"
-KEYWORDS="~amd64"
+KEYWORDS="amd64"
 IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt sexp zarith zip"
 RESTRICT="strip"
 

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     e3e8e816e8945f661507f1235fd1779fe7039d35
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Sun Apr  2 11:24:42 2023 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Sun Apr  2 11:25:32 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e3e8e816

sci-mathematics/why3-for-spark: stabilize 2020 for amd64

Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
index 66a760496a92..201e90379c72 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
@@ -13,7 +13,7 @@ SRC_URI="https://community.download.adacore.com/v1/8bb5801e17b8b23453262da69c981
 
 LICENSE="GPL-3"
 SLOT="0"
-KEYWORDS="~amd64"
+KEYWORDS="amd64"
 IUSE="doc emacs gtk html +ocamlopt zarith zip"
 RESTRICT="strip"
 

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     e361aafd702c08c1f382bcfe2006331603d6f526
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Fri Mar 31 13:12:01 2023 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Fri Mar 31 13:12:44 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e361aafd

sci-mathematics/why3-for-spark: require lablgtk-2

Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 .../{why3-for-spark-2019-r2.ebuild => why3-for-spark-2019-r3.ebuild}  | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r3.ebuild
similarity index 97%
rename from sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
rename to sci-mathematics/why3-for-spark/why3-for-spark-2019-r3.ebuild
index f83359f0ee7e..3747497af8a1 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r3.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
@@ -21,7 +21,7 @@ DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=]
 	<=dev-ml/menhir-20190924:=
 	dev-ml/num:=
 	doc? ( dev-tex/rubber )
-	gtk? ( >=dev-ml/lablgtk-2.18.8:=[sourceview] )
+	gtk? ( dev-ml/lablgtk:2=[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
 	html? ( dev-tex/hevea:= )
 	hypothesis-selection? ( dev-ml/ocamlgraph:= )

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     e6e9b60f9793c4d9b0d56f5a72d8edf5a286bf6b
Author:     Michael Mair-Keimberger <mmk <AT> levelnine <DOT> at>
AuthorDate: Tue Jul 26 19:39:39 2022 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Tue Jul 26 19:54:20 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e6e9b60f

sci-mathematics/why3-for-spark: use https

Signed-off-by: Michael Mair-Keimberger <mmk <AT> levelnine.at>
Portage 3.0.34 / pkgdev 0.2.1 / pkgcheck 0.10.11
Closes: https://github.com/gentoo/gentoo/pull/26610
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild | 2 +-
 sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild    | 2 +-
 sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
index f0597604b01e..bc975bd21a6b 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
@@ -6,7 +6,7 @@ EAPI=7
 MYP=why3-${PV}-20190517-197BB-src
 
 DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
+HOMEPAGE="https://why3.lri.fr/"
 SRC_URI="http://mirrors.cdn.adacore.com/art/5cdf915d31e87a8f1c967d54
 	-> ${MYP}.tar.gz"
 

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
index 7988788f83af..9075ebf3e9da 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
@@ -8,7 +8,7 @@ inherit autotools
 MYP=why3-${PV}-20200429-199EF-src
 
 DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
+HOMEPAGE="https://why3.lri.fr/"
 SRC_URI="https://community.download.adacore.com/v1/8bb5801e17b8b23453262da69c981c091959eec7?filename=${MYP}.tar.gz"
 
 LICENSE="GPL-3"

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
index fd2397eb1b04..0801160e66e9 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
@@ -10,7 +10,7 @@ ID=dd74ae7ecfd7d56aff7b17cee7a35559384a600f
 MYP=why3-${PV}-20210519-19ADF-src
 
 DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
+HOMEPAGE="https://why3.lri.fr/"
 SRC_URI="${ADAMIRROR}/${ID}?filename=${MYP}.tar.gz -> ${MYP}.tar.gz"
 
 LICENSE="GPL-3"

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     57ec03f6bdbbbb51b2909aa42a8d93f8acd0c544
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Mon Jun 27 08:47:05 2022 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Mon Jun 27 08:47:05 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=57ec03f6

sci-mathematics/why3-for-spark: refix QA_FLAGS

Closes: https://bugs.gentoo.org/854555
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
index 13fef502cfe3..fd2397eb1b04 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
@@ -56,9 +56,9 @@ PATCHES=(
 )
 
 QA_FLAGS_IGNORED=(
-	'/usr/lib*/why3/commands/*.cmxs'
-	'/usr/lib*/why3/plugins/*.cmxs'
-	'/usr/lib*/ocaml/why3/why3*.cmxs'
+	'/usr/lib.*/why3/commands/.*cmxs'
+	'/usr/lib.*/why3/plugins/.*cmxs'
+	'/usr/lib.*/ocaml/why3/.*cmxs'
 	/usr/bin/why3
 	/usr/bin/why3config.cmxs
 	/usr/bin/why3session.cmxs

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     641255d69acd7ef55105d2032ffb42d889ed5902
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Mon Jun 27 06:19:33 2022 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Mon Jun 27 06:19:33 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=641255d6

sci-mathematics/why3-for-spark: ignore some QA warnings

Closes: https://bugs.gentoo.org/837278
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 .../why3-for-spark/why3-for-spark-2021-r1.ebuild         | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
index 986e7bf497fd..13fef502cfe3 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
@@ -56,19 +56,9 @@ PATCHES=(
 )
 
 QA_FLAGS_IGNORED=(
-	/usr/lib64/why3/commands/why3shell.cmxs
-	/usr/lib64/why3/commands/why3extract.cmxs
-	/usr/lib64/why3/commands/why3execute.cmxs
-	/usr/lib64/why3/commands/why3prove.cmxs
-	/usr/lib64/why3/commands/why3wc.cmxs
-	/usr/lib64/why3/commands/why3doc.cmxs
-	/usr/lib64/why3/commands/why3replay.cmxs
-	/usr/lib64/why3/commands/why3webserver.cmxs
-	/usr/lib64/why3/commands/why3pp.cmxs
-	/usr/lib64/why3/commands/why3show.cmxs
-	/usr/lib64/why3/plugins/'.*'.cmxs
-	/usr/lib64/ocaml/why3/why3.cmxs
-	/usr/lib64/ocaml/why3/why3extract.cmxs
+	'/usr/lib*/why3/commands/*.cmxs'
+	'/usr/lib*/why3/plugins/*.cmxs'
+	'/usr/lib*/ocaml/why3/why3*.cmxs'
 	/usr/bin/why3
 	/usr/bin/why3config.cmxs
 	/usr/bin/why3session.cmxs

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     ed2328c4b86578b7b8f53c2c4a372718635f26f6
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Fri Mar 11 21:00:38 2022 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Fri Mar 11 21:01:12 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ed2328c4

sci-mathematics/why3-for-spark: add USE to select sexp

Closes: https://bugs.gentoo.org/834881
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/metadata.xml        |  3 +-
 ...k-2021.ebuild => why3-for-spark-2021-r1.ebuild} | 65 +++++++++++++---------
 2 files changed, 40 insertions(+), 28 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/metadata.xml b/sci-mathematics/why3-for-spark/metadata.xml
index edf687ae15b9..9b2196685bde 100644
--- a/sci-mathematics/why3-for-spark/metadata.xml
+++ b/sci-mathematics/why3-for-spark/metadata.xml
@@ -21,7 +21,8 @@
 		<flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag>
 		<flag name="html">Build HTML documentation</flag>
 		<flag name="hypothesis-selection">Enable hypothesis selection</flag>
-		<flag name="zarith">Use <pkg>dev-ml/zarith</pkg></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>
 </pkgmetadata>

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
similarity index 77%
rename from sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
rename to sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
index fb9acf5c9a31..986e7bf497fd 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
@@ -3,7 +3,7 @@
 
 EAPI=7
 
-inherit autotools
+inherit autotools findlib
 
 ADAMIRROR=https://community.download.adacore.com/v1
 ID=dd74ae7ecfd7d56aff7b17cee7a35559384a600f
@@ -16,29 +16,36 @@ SRC_URI="${ADAMIRROR}/${ID}?filename=${MYP}.tar.gz -> ${MYP}.tar.gz"
 LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt zarith zip"
+IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt sexp zarith zip"
 RESTRICT="strip"
 
-DEPEND=">=dev-lang/ocaml-4.11:=[ocamlopt?]
+RDEPEND="
+	>=dev-lang/ocaml-4.11:=[ocamlopt?]
 	dev-ml/menhir:=
 	dev-ml/num:=
 	dev-ml/yojson:=
-	coq? (
-		sci-mathematics/coq
+	coq? ( sci-mathematics/coq )
+	emacs? ( app-editors/emacs:* )
+	gtk? ( dev-ml/lablgtk:=[sourceview] )
+	html? ( dev-tex/hevea:= )
+	hypothesis-selection? ( dev-ml/ocamlgraph:= )
+	sexp? (
+		dev-ml/ppx_deriving:=[ocamlopt?]
+		dev-ml/ppx_sexp_conv:=[ocamlopt?]
+		dev-ml/sexplib:=[ocamlopt?]
 	)
+	zarith? ( dev-ml/zarith:= )
+	zip? ( dev-ml/camlzip:= )
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
 	doc? (
-		dev-tex/rubber
 		dev-python/sphinx
-		media-gfx/graphviz
 		dev-python/sphinxcontrib-bibtex
+		dev-tex/rubber
+		media-gfx/graphviz
 	)
-	gtk? ( dev-ml/lablgtk:=[sourceview] )
-	emacs? ( app-editors/emacs:* )
-	html? ( dev-tex/hevea:= )
-	hypothesis-selection? ( dev-ml/ocamlgraph:= )
-	zarith? ( dev-ml/zarith:= )
-	zip? ( dev-ml/camlzip:= )"
-RDEPEND="${DEPEND}"
+"
 
 S="${WORKDIR}"/${MYP}
 
@@ -68,30 +75,34 @@ QA_FLAGS_IGNORED=(
 	/usr/bin/gnat_server
 	/usr/bin/gnatwhy3
 	/usr/bin/why3realize.cmxs
+	/usr/bin/why3ide.cmxs
 )
 
 REQUIRED_USE="html? ( doc )"
 
 src_prepare() {
 	find examples -name \*gz | xargs gunzip
-	default
 	eautoreconf
+	default
 }
 
 src_configure() {
-	econf \
-		--disable-pvs-libs \
-		--disable-isabelle-libs \
-		--enable-verbose-make \
-		$(use_enable coq coq-libs) \
-		$(use_enable doc) \
-		$(use_enable emacs emacs-compilation) \
-		$(use_enable gtk ide) \
-		$(use_enable html html-pdf) \
-		$(use_enable hypothesis-selection) \
-		$(use_enable ocamlopt native-code) \
-		$(use_enable zarith) \
+	local myconf=(
+		--disable-pvs-libs
+		--disable-isabelle-libs
+		--enable-verbose-make
+		$(use_enable coq coq-libs)
+		$(use_enable doc)
+		$(use_enable emacs emacs-compilation)
+		$(use_enable gtk ide)
+		$(use_enable html html-pdf)
+		$(use_enable hypothesis-selection)
+		$(use_enable ocamlopt native-code)
+		$(use_enable sexp pp-sexp)
+		$(use_enable zarith)
 		$(use_enable zip)
+	)
+	econf "${myconf[@]}"
 }
 
 src_compile() {

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     ddc4457e1404d8eafbb724d1fc77656f5c049d6e
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Mon Feb  7 21:48:12 2022 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Mon Feb  7 21:48:12 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ddc4457e

sci-mathematics/why3-for-spark: ignore CFLAGS

Closes: https://bugs.gentoo.org/799245
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 .../why3-for-spark/why3-for-spark-2021.ebuild      | 26 ++++++++++++----------
 1 file changed, 14 insertions(+), 12 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
index 2e831ddd9739..fb9acf5c9a31 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
@@ -49,23 +49,25 @@ PATCHES=(
 )
 
 QA_FLAGS_IGNORED=(
-	/usr/lib64/why3/commands/why3shell
-	/usr/lib64/why3/commands/why3extract
-	/usr/lib64/why3/commands/why3execute
-	/usr/lib64/why3/commands/why3prove
-	/usr/lib64/why3/commands/why3wc
-	/usr/lib64/why3/commands/why3doc
-	/usr/lib64/why3/commands/why3replay
-	/usr/lib64/why3/commands/why3webserver
+	/usr/lib64/why3/commands/why3shell.cmxs
+	/usr/lib64/why3/commands/why3extract.cmxs
+	/usr/lib64/why3/commands/why3execute.cmxs
+	/usr/lib64/why3/commands/why3prove.cmxs
+	/usr/lib64/why3/commands/why3wc.cmxs
+	/usr/lib64/why3/commands/why3doc.cmxs
+	/usr/lib64/why3/commands/why3replay.cmxs
+	/usr/lib64/why3/commands/why3webserver.cmxs
+	/usr/lib64/why3/commands/why3pp.cmxs
+	/usr/lib64/why3/commands/why3show.cmxs
 	/usr/lib64/why3/plugins/'.*'.cmxs
 	/usr/lib64/ocaml/why3/why3.cmxs
 	/usr/lib64/ocaml/why3/why3extract.cmxs
 	/usr/bin/why3
-	/usr/bin/why3config
-	/usr/bin/why3session
+	/usr/bin/why3config.cmxs
+	/usr/bin/why3session.cmxs
 	/usr/bin/gnat_server
 	/usr/bin/gnatwhy3
-	/usr/bin/why3realize
+	/usr/bin/why3realize.cmxs
 )
 
 REQUIRED_USE="html? ( doc )"
@@ -107,7 +109,7 @@ src_install() {
 	local cmdPath=/usr/$(get_libdir)/why3/commands
 	dosym ../why3server ${cmdPath}/why3server
 	# Remove duplicated files
-	for filename in config ide realize server session; do
+	for filename in config.cmxs ide.cmxs realize.cmxs server session.cmxs; do
 		if [[ -e "${D}"${cmdPath}/why3${filename} ]]; then
 			rm "${D}"${cmdPath}/why3${filename}
 			dosym ../../../bin/why3${filename} ${cmdPath}/why3${filename}

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     0dad6929d837bb643f4e260f9eb1ca16b6b6c0ba
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Mon Feb  7 12:50:40 2022 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Mon Feb  7 12:50:40 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0dad6929

sci-mathematics/why3-for-spark: works with new ocaml too

Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
index b851107a4c41..2e831ddd9739 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
@@ -19,7 +19,7 @@ KEYWORDS="~amd64"
 IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt zarith zip"
 RESTRICT="strip"
 
-DEPEND="dev-lang/ocaml:0/4.11[ocamlopt?]
+DEPEND=">=dev-lang/ocaml-4.11:=[ocamlopt?]
 	dev-ml/menhir:=
 	dev-ml/num:=
 	dev-ml/yojson:=

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     ee9179423d62240ec33f0bb32d24c640169afbf3
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Mon Feb  7 09:57:19 2022 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Mon Feb  7 09:57:19 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ee917942

sci-mathematics/why3-for-spark: duplicate deps

Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild | 1 -
 1 file changed, 1 deletion(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
index 7b43ab3763ab..7988788f83af 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
@@ -29,7 +29,6 @@ DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=]
 	doc? (
 		dev-tex/rubber
 		dev-python/sphinx
-		dev-python/sphinxcontrib-bibtex
 		media-gfx/graphviz
 		dev-python/sphinxcontrib-bibtex
 	)

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     c4284123349e1f898877a81d497bbaf1569cccfa
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Mon Feb  7 09:54:50 2022 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Mon Feb  7 09:55:25 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c4284123

sci-mathematics/why3-for-spark: fix doc deps

Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
index 8fd579c6c8d4..7b43ab3763ab 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
@@ -29,6 +29,7 @@ DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=]
 	doc? (
 		dev-tex/rubber
 		dev-python/sphinx
+		dev-python/sphinxcontrib-bibtex
 		media-gfx/graphviz
 		dev-python/sphinxcontrib-bibtex
 	)

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     6e412177eb38dfea270e9c6c8cf60375cc9ddd81
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Sun Feb  6 15:52:17 2022 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Sun Feb  6 17:41:30 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=6e412177

sci-mathematics/why3-for-spark: drop old version

Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/Manifest            |  1 -
 sci-mathematics/why3-for-spark/metadata.xml        |  1 -
 .../why3-for-spark/why3-for-spark-2018.ebuild      | 73 ----------------------
 .../why3-for-spark/why3-for-spark-2019-r2.ebuild   |  6 +-
 4 files changed, 3 insertions(+), 78 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest
index a15aa4d6feb9..afc57cb3d37d 100644
--- a/sci-mathematics/why3-for-spark/Manifest
+++ b/sci-mathematics/why3-for-spark/Manifest
@@ -1,4 +1,3 @@
 DIST 8bb5801e17b8b23453262da69c981c091959eec7?filename=why3-2020-20200429-199EF-src.tar.gz 9739066 BLAKE2B c7c11a92d4926f90be9ffa94d74e65ad78423953b53ee617565ccfcea4a5a60b251367b0712c30d170ab717d5868f7d95d62694f38c3d2f52805a28a6522ab8a SHA512 61cd5509957230ff81186d2507b9749b182cdc44698f6658337ce294d210742e57164d25d7c0eb3eb5ea0c53f5f46dea099e6a0769fadcb709a5a8557ed3cae3
 DIST why3-2019-20190517-197BB-src.tar.gz 9439414 BLAKE2B 68072064e8ee9152528c90afc948047a1f4d58b960ac05b276761fdca5ba1204100c75f33db7bb0ea1a8a646b734e62892ed41bd875b954354f52b8f9d498d4a SHA512 9169a4ff9ee994a19f9f04b689d1b9c679f5340bcd631d7d49b4c55064f505bd5a6ca8149077e5d24d36f5365f0cab58587094e86f352a9105fc46f10c0746ba
 DIST why3-2021-20210519-19ADF-src.tar.gz 10386938 BLAKE2B 93b6323c562126244f5cccef34088a521fe3dc1cec07c966e94472503ec8492707b20a641936449307f0439e711a82260d36679cbc69f53df8e7886a1d3673c3 SHA512 65e3c1430001962f2c7cce786f3e30f14b5295cff89c4087d95c1545e81743723319ba0309dbe15c4c46552110b25ff57addc3ee085dade02ea59a2273b127db
-DIST why3-for-spark-gpl-2018-src.tar.gz 7682767 BLAKE2B 0b0272ca4d5519ca402990b234d0847378bcd2a0949fea78ea10e355233a16aebe79b938cdf8e4daadabb909171cab83b9d6ccacf9f2dc1c0b57bb6da6fd1fe0 SHA512 fc798acf343484fd8e70f470a318753c9a0e9967ff579f20ec185bf3c2a75e7a4a556388fc86a378610ce4a467f3e722c6f610da34d4c33bc3d6b10551731f07

diff --git a/sci-mathematics/why3-for-spark/metadata.xml b/sci-mathematics/why3-for-spark/metadata.xml
index 6581985ad1d8..edf687ae15b9 100644
--- a/sci-mathematics/why3-for-spark/metadata.xml
+++ b/sci-mathematics/why3-for-spark/metadata.xml
@@ -21,7 +21,6 @@
 		<flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag>
 		<flag name="html">Build HTML documentation</flag>
 		<flag name="hypothesis-selection">Enable hypothesis selection</flag>
-		<flag name="profiling">Enable profiling</flag>
 		<flag name="zarith">Use <pkg>dev-ml/zarith</pkg></flag>
 		<flag name="zip">Enable compression of session files</flag>
 	</use>

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
deleted file mode 100644
index 48d190220579..000000000000
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
+++ /dev/null
@@ -1,73 +0,0 @@
-# Copyright 1999-2021 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=6
-
-MYP=${PN}-gpl-${PV}-src
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="http://mirrors.cdn.adacore.com/art/5b0819dec7a447df26c27a43
-	-> ${MYP}.tar.gz"
-
-LICENSE="GPL-3"
-SLOT="0"
-KEYWORDS="amd64"
-IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
-RESTRICT="strip"
-
-DEPEND=">=dev-lang/ocaml-4.02.3:=[ocamlopt=]
-	dev-ml/menhir:=
-	coq? ( sci-mathematics/coq )
-	doc? ( dev-tex/rubber )
-	gtk? ( dev-ml/lablgtk:2=[sourceview] )
-	emacs? ( >=app-editors/emacs-23.1:* )
-	html? ( dev-tex/hevea:= )
-	hypothesis-selection? ( dev-ml/ocamlgraph:= )
-	zarith? ( dev-ml/zarith:= )
-	zip? ( >=dev-ml/camlzip-1.07:= )"
-RDEPEND="${DEPEND}"
-
-S="${WORKDIR}"/${MYP}
-
-PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
-
-REQUIRED_USE="html? ( doc )"
-
-src_configure() {
-	econf \
-		--disable-pvs-libs \
-		--disable-isabelle-libs \
-		$(use_enable coq coq-libs) \
-		$(use_enable coq coq-tactic) \
-		$(use_enable doc) \
-		$(use_enable emacs emacs-compilation) \
-		$(use_enable gtk ide) \
-		$(use_enable html html-doc) \
-		$(use_enable hypothesis-selection) \
-		$(use_enable ocamlopt native-code) \
-		$(use_enable profiling) \
-		$(use_enable zarith) \
-		$(use_enable zip)
-}
-
-src_compile() {
-	emake -j1
-	if use ocamlopt; then
-		emake byte
-	fi
-	use doc && emake doc
-}
-
-src_install() {
-	emake DESTDIR="${D}" -j1 install
-	emake DESTDIR="${D}" -j1 install-lib
-	emake DESTDIR="${D}" install_spark2014_dev
-	einstalldocs
-	docompress -x /usr/share/doc/${PF}/examples
-	dodoc -r examples
-	if use doc; then
-		dodoc doc/manual.pdf
-		use html && dodoc -r doc/html
-	fi
-}

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
index 9fa713b6baaa..f0597604b01e 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
@@ -12,13 +12,13 @@ SRC_URI="http://mirrors.cdn.adacore.com/art/5cdf915d31e87a8f1c967d54
 
 LICENSE="GPL-3"
 SLOT="0"
-KEYWORDS="~amd64"
+KEYWORDS="amd64"
 IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt zarith zip"
 RESTRICT="strip"
 
 DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=]
 	>=dev-ml/ocamlbuild-0.14.0
-	dev-ml/menhir:=
+	<=dev-ml/menhir-20190924:=
 	dev-ml/num:=
 	coq? ( >=sci-mathematics/coq-8.9.1 )
 	doc? ( dev-tex/rubber )

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     cf52b47b1c4d265eadbfbfa9c0352a0c5bd4d5c8
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Sat Sep 18 16:48:56 2021 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Sat Sep 18 16:51:25 2021 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=cf52b47b

sci-mathematics/why3-for-spark: UnusedInherits

Package-Manager: Portage-3.0.20, Repoman-3.0.3
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild | 2 --
 1 file changed, 2 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
index bb7093a5b79..48d19022057 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
@@ -3,8 +3,6 @@
 
 EAPI=6
 
-inherit autotools
-
 MYP=${PN}-gpl-${PV}-src
 
 DESCRIPTION="Platform for deductive program verification"

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     3daf7a4558c0902de667621d1b3c3224418a5007
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Tue Jun 29 14:16:08 2021 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Tue Jun 29 14:16:08 2021 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=3daf7a45

sci-mathematics/why3-for-spark: disable hypothesis-selection

Closes: https://bugs.gentoo.org/799173
Package-Manager: Portage-3.0.20, Repoman-3.0.2
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild | 1 +
 1 file changed, 1 insertion(+)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
index 04dd0ae9fcb..06a68247055 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
@@ -80,6 +80,7 @@ src_configure() {
 		--disable-pvs-libs \
 		--disable-isabelle-libs \
 		--enable-verbose-make \
+		--disable-hypothesis-selection \
 		$(use_enable coq coq-libs) \
 		$(use_enable doc) \
 		$(use_enable emacs emacs-compilation) \

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     5aff1bfa73f6a17a8f9d6952315f80b2f84e9667
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Wed Feb 10 17:25:02 2021 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Wed Feb 10 17:25:02 2021 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=5aff1bfa

sci-mathematics/why3-for-spark: fix dep

Closes: https://bugs.gentoo.org/769845
Package-Manager: Portage-3.0.13, Repoman-3.0.2
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
index a7fe3230408..8fd579c6c8d 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2020.ebuild
@@ -20,7 +20,7 @@ RESTRICT="strip"
 DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=]
 	>=dev-ml/ocamlbuild-0.14.0
 	dev-ml/menhir:=
-	dev-ml/num:=
+	<dev-ml/num-1.4:=
 	dev-ml/yojson:=
 	coq? (
 		>=sci-mathematics/coq-8.9.1

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Sam James]

commit:     8095292e91a60900fb257d373295d0052f883f46
Author:     Sam James <sam <AT> gentoo <DOT> org>
AuthorDate: Sun Jan 17 03:59:40 2021 +0000
Commit:     Sam James <sam <AT> gentoo <DOT> org>
CommitDate: Sun Jan 17 04:10:27 2021 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=8095292e

sci-mathematics/why3-for-spark: supports both lablgtk:2, :3 for most versions

See: https://gitlab.inria.fr/why3/why3/-/blob/master/CHANGES.md#version-121-october-28-2019
Package-Manager: Portage-3.0.12.0.2-prefix, Repoman-3.0.2
Signed-off-by: Sam James <sam <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild    | 4 ++--
 sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild | 4 ++--
 sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild | 4 ++--
 sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild    | 4 ++--
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
index 2335a61928f..6314df13e4b 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2019 Gentoo Authors
+# Copyright 1999-2021 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=6
@@ -22,7 +22,7 @@ DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
 	dev-ml/menhir
 	coq? ( sci-mathematics/coq )
 	doc? ( dev-tex/rubber )
-	gtk? ( dev-ml/lablgtk[sourceview] )
+	gtk? ( dev-ml/lablgtk:2[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
 	html? ( dev-tex/hevea )
 	hypothesis-selection? ( dev-ml/ocamlgraph )

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
index c19ce6114c3..4ff38ed0330 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2020 Gentoo Authors
+# Copyright 1999-2021 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=6
@@ -24,7 +24,7 @@ DEPEND=">=dev-lang/ocaml-4.09.0[ocamlopt?]
 	dev-ml/num
 	coq? ( >=sci-mathematics/coq-8.9.1 )
 	doc? ( dev-tex/rubber )
-	gtk? ( >=dev-ml/lablgtk-2.18.8[sourceview] )
+	gtk? ( >=dev-ml/lablgtk-2.18.8:=[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
 	html? ( dev-tex/hevea )
 	hypothesis-selection? ( dev-ml/ocamlgraph )

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
index 7b658828da4..738641a2375 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2020 Gentoo Authors
+# Copyright 1999-2021 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=7
@@ -22,7 +22,7 @@ DEPEND=">=dev-lang/ocaml-4.09.0[ocamlopt?]
 	dev-ml/num
 	coq? ( >=sci-mathematics/coq-8.9.1 )
 	doc? ( dev-tex/rubber )
-	gtk? ( >=dev-ml/lablgtk-2.18.8[sourceview] )
+	gtk? ( >=dev-ml/lablgtk-2.18.8:=[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
 	html? ( dev-tex/hevea )
 	hypothesis-selection? ( dev-ml/ocamlgraph )

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild
index 409bfc36cda..5ad16322b0a 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2019 Gentoo Authors
+# Copyright 1999-2021 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=6
@@ -22,7 +22,7 @@ DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
 	dev-ml/menhir
 	coq? ( sci-mathematics/coq )
 	doc? ( dev-tex/rubber )
-	gtk? ( dev-ml/lablgtk[sourceview] )
+	gtk? ( dev-ml/lablgtk:=[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
 	html? ( dev-tex/hevea )
 	hypothesis-selection? ( dev-ml/ocamlgraph )

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Sam James]

commit:     13795972d83aa1591561d7e60c220c623538b5e2
Author:     Sam James <sam <AT> gentoo <DOT> org>
AuthorDate: Sun Jan 17 04:03:17 2021 +0000
Commit:     Sam James <sam <AT> gentoo <DOT> org>
CommitDate: Sun Jan 17 04:10:28 2021 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=13795972

sci-mathematics/why3-for-spark: update OCaml deps

* We need := for OCaml deps to ensure we're rebuilt
  when they update for consistency, to prevent
  strange issues.

* Use ocamlopt= rather than ocamlopt? in the
  dev-lang/ocaml dependency to ensure ocamlopt
  is consistently on/off throughout the system.

Package-Manager: Portage-3.0.12.0.2-prefix, Repoman-3.0.2
Signed-off-by: Sam James <sam <AT> gentoo.org>

 .../why3-for-spark/why3-for-spark-2018.ebuild            | 16 ++++++++--------
 .../why3-for-spark/why3-for-spark-2019-r1.ebuild         | 14 +++++++-------
 .../why3-for-spark/why3-for-spark-2019-r2.ebuild         | 16 ++++++++--------
 .../why3-for-spark/why3-for-spark-2019.ebuild            | 14 +++++++-------
 4 files changed, 30 insertions(+), 30 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
index 6314df13e4b..bb7093a5b79 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
@@ -16,18 +16,18 @@ LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="amd64"
 IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
-RESTRICT=strip
+RESTRICT="strip"
 
-DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
-	dev-ml/menhir
+DEPEND=">=dev-lang/ocaml-4.02.3:=[ocamlopt=]
+	dev-ml/menhir:=
 	coq? ( sci-mathematics/coq )
 	doc? ( dev-tex/rubber )
-	gtk? ( dev-ml/lablgtk:2[sourceview] )
+	gtk? ( dev-ml/lablgtk:2=[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
-	html? ( dev-tex/hevea )
-	hypothesis-selection? ( dev-ml/ocamlgraph )
-	zarith? ( dev-ml/zarith )
-	zip? ( >=dev-ml/camlzip-1.07 )"
+	html? ( dev-tex/hevea:= )
+	hypothesis-selection? ( dev-ml/ocamlgraph:= )
+	zarith? ( dev-ml/zarith:= )
+	zip? ( >=dev-ml/camlzip-1.07:= )"
 RDEPEND="${DEPEND}"
 
 S="${WORKDIR}"/${MYP}

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
index 4ff38ed0330..e4953adc3ce 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
@@ -18,18 +18,18 @@ KEYWORDS="~amd64"
 IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt zarith zip"
 RESTRICT=strip
 
-DEPEND=">=dev-lang/ocaml-4.09.0[ocamlopt?]
+DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=]
 	>=dev-ml/ocamlbuild-0.14.0
-	dev-ml/menhir
-	dev-ml/num
+	dev-ml/menhir:=
+	dev-ml/num:=
 	coq? ( >=sci-mathematics/coq-8.9.1 )
 	doc? ( dev-tex/rubber )
 	gtk? ( >=dev-ml/lablgtk-2.18.8:=[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
-	html? ( dev-tex/hevea )
-	hypothesis-selection? ( dev-ml/ocamlgraph )
-	zarith? ( dev-ml/zarith )
-	zip? ( >=dev-ml/camlzip-1.07 )"
+	html? ( dev-tex/hevea:= )
+	hypothesis-selection? ( dev-ml/ocamlgraph:= )
+	zarith? ( dev-ml/zarith:= )
+	zip? ( >=dev-ml/camlzip-1.07:= )"
 RDEPEND="${DEPEND}"
 
 S="${WORKDIR}"/${MYP}

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
index 738641a2375..9fa713b6baa 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
@@ -14,20 +14,20 @@ LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="~amd64"
 IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt zarith zip"
-RESTRICT=strip
+RESTRICT="strip"
 
-DEPEND=">=dev-lang/ocaml-4.09.0[ocamlopt?]
+DEPEND=">=dev-lang/ocaml-4.09.0:=[ocamlopt=]
 	>=dev-ml/ocamlbuild-0.14.0
-	dev-ml/menhir
-	dev-ml/num
+	dev-ml/menhir:=
+	dev-ml/num:=
 	coq? ( >=sci-mathematics/coq-8.9.1 )
 	doc? ( dev-tex/rubber )
 	gtk? ( >=dev-ml/lablgtk-2.18.8:=[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
-	html? ( dev-tex/hevea )
-	hypothesis-selection? ( dev-ml/ocamlgraph )
-	zarith? ( dev-ml/zarith )
-	zip? ( >=dev-ml/camlzip-1.07 )"
+	html? ( dev-tex/hevea:= )
+	hypothesis-selection? ( dev-ml/ocamlgraph:= )
+	zarith? ( dev-ml/zarith:= )
+	zip? ( >=dev-ml/camlzip-1.07:= )"
 RDEPEND="${DEPEND}"
 
 S="${WORKDIR}"/${MYP}

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild
index 5ad16322b0a..72c43f3fc8c 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild
@@ -16,18 +16,18 @@ LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="~amd64"
 IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
-RESTRICT=strip
+RESTRICT="strip"
 
-DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
-	dev-ml/menhir
+DEPEND=">=dev-lang/ocaml-4.02.3:=[ocamlopt=]
+	dev-ml/menhir:=
 	coq? ( sci-mathematics/coq )
 	doc? ( dev-tex/rubber )
 	gtk? ( dev-ml/lablgtk:=[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
-	html? ( dev-tex/hevea )
-	hypothesis-selection? ( dev-ml/ocamlgraph )
-	zarith? ( dev-ml/zarith )
-	zip? ( >=dev-ml/camlzip-1.07 )"
+	html? ( dev-tex/hevea:= )
+	hypothesis-selection? ( dev-ml/ocamlgraph:= )
+	zarith? ( dev-ml/zarith:= )
+	zip? ( >=dev-ml/camlzip-1.07:= )"
 RDEPEND="${DEPEND}"
 
 S="${WORKDIR}"/${MYP}

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     0959f5c012916f832872f2d864fb06552e1d16d5
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Mon Jun 15 17:19:49 2020 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Mon Jun 15 17:19:49 2020 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0959f5c0

sci-mathematics/why3-for-spark: fix broken links

Closes: https://bugs.gentoo.org/728334
Package-Manager: Portage-2.3.99, Repoman-2.3.22
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
index 8f82a9c4bb8..7b658828da4 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
@@ -100,8 +100,10 @@ src_install() {
 	dosym ../why3server ${cmdPath}/why3server
 	# Remove duplicated files
 	for filename in config ide realize server session; do
-		rm "${D}"${cmdPath}/why3${filename}
-		dosym ../../../bin/why3${filename} ${cmdPath}/why3${filename}
+		if [[ -e "${D}"${cmdPath}/why3${filename} ]]; then
+			rm "${D}"${cmdPath}/why3${filename}
+			dosym ../../../bin/why3${filename} ${cmdPath}/why3${filename}
+		fi
 	done
 	rm "${D}"/usr/$(get_libdir)/why3/why3cpulimit
 	dosym ../../bin/why3cpulimit /usr/$(get_libdir)/why3/why3cpulimit

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     74292be3bc80e701d8edc741daf55e7053583ced
Author:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
AuthorDate: Sun Jun 14 11:49:16 2020 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Sun Jun 14 11:49:16 2020 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=74292be3

sci-mathematics/why3-for-spark: fix broken symlink

Closes: https://bugs.gentoo.org/728176
Package-Manager: Portage-2.3.99, Repoman-2.3.22
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
index e27b1427040..8f82a9c4bb8 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r2.ebuild
@@ -104,7 +104,7 @@ src_install() {
 		dosym ../../../bin/why3${filename} ${cmdPath}/why3${filename}
 	done
 	rm "${D}"/usr/$(get_libdir)/why3/why3cpulimit
-	dosym ../../../bin/why3cpulimit /usr/$(get_libdir)/why3/why3cpulimit
+	dosym ../../bin/why3cpulimit /usr/$(get_libdir)/why3/why3cpulimit
 
 	einstalldocs
 	docompress -x /usr/share/doc/${PF}/examples

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     15f19de474ea4871f4284684f26b152ed2eff792
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Fri Jan 17 10:41:07 2020 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Fri Jan 17 10:41:07 2020 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=15f19de4

sci-mathematics/why3-for-spark: profiling is not more supported by newer ocaml

Package-Manager: Portage-2.3.79, Repoman-2.3.16
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
index bbdfc469293..c19ce6114c3 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
@@ -15,7 +15,7 @@ SRC_URI="http://mirrors.cdn.adacore.com/art/5cdf915d31e87a8f1c967d54
 LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
+IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt zarith zip"
 RESTRICT=strip
 
 DEPEND=">=dev-lang/ocaml-4.09.0[ocamlopt?]
@@ -50,7 +50,6 @@ src_configure() {
 		$(use_enable html html-doc) \
 		$(use_enable hypothesis-selection) \
 		$(use_enable ocamlopt native-code) \
-		$(use_enable profiling) \
 		$(use_enable zarith) \
 		$(use_enable zip)
 }

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     47cce5e3baa22474f4e67467d0a320adee35c8ad
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Thu Jan 16 10:09:16 2020 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Thu Jan 16 10:09:16 2020 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=47cce5e3

sci-mathematics/why3-for-spark: depend on a newer dev-ml/lablgtk

Package-Manager: Portage-2.3.79, Repoman-2.3.16
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
index 8d152264c06..bbdfc469293 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
@@ -24,7 +24,7 @@ DEPEND=">=dev-lang/ocaml-4.09.0[ocamlopt?]
 	dev-ml/num
 	coq? ( >=sci-mathematics/coq-8.9.1 )
 	doc? ( dev-tex/rubber )
-	gtk? ( dev-ml/lablgtk[sourceview] )
+	gtk? ( >=dev-ml/lablgtk-2.18.8[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )
 	html? ( dev-tex/hevea )
 	hypothesis-selection? ( dev-ml/ocamlgraph )

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     9e87df67d81653262595c6e816aea5326ec015e6
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Wed Jan 15 08:18:52 2020 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Wed Jan 15 08:18:52 2020 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=9e87df67

sci-mathematics/why3-for-spark: Needs a newer coq version

Package-Manager: Portage-2.3.79, Repoman-2.3.16
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
index 6df32dd7409..8d152264c06 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
@@ -22,7 +22,7 @@ DEPEND=">=dev-lang/ocaml-4.09.0[ocamlopt?]
 	>=dev-ml/ocamlbuild-0.14.0
 	dev-ml/menhir
 	dev-ml/num
-	coq? ( sci-mathematics/coq )
+	coq? ( >=sci-mathematics/coq-8.9.1 )
 	doc? ( dev-tex/rubber )
 	gtk? ( dev-ml/lablgtk[sourceview] )
 	emacs? ( >=app-editors/emacs-23.1:* )

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     d53b71f85b0a0eac777c476cb523c7bc30d3e5da
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Tue Jan 14 07:51:42 2020 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Tue Jan 14 07:51:42 2020 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=d53b71f8

sci-mathematics/why3-for-spark: use ocaml-4.09

Closes: https://bugs.gentoo.org/705072
Package-Manager: Portage-2.3.79, Repoman-2.3.16
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>

 .../why3-for-spark/why3-for-spark-2019-r1.ebuild   | 78 ++++++++++++++++++++++
 1 file changed, 78 insertions(+)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
new file mode 100644
index 00000000000..6df32dd7409
--- /dev/null
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild
@@ -0,0 +1,78 @@
+# Copyright 1999-2020 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=6
+
+inherit autotools
+
+MYP=why3-${PV}-20190517-197BB-src
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/"
+SRC_URI="http://mirrors.cdn.adacore.com/art/5cdf915d31e87a8f1c967d54
+	-> ${MYP}.tar.gz"
+
+LICENSE="GPL-3"
+SLOT="0"
+KEYWORDS="~amd64"
+IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
+RESTRICT=strip
+
+DEPEND=">=dev-lang/ocaml-4.09.0[ocamlopt?]
+	>=dev-ml/ocamlbuild-0.14.0
+	dev-ml/menhir
+	dev-ml/num
+	coq? ( sci-mathematics/coq )
+	doc? ( dev-tex/rubber )
+	gtk? ( dev-ml/lablgtk[sourceview] )
+	emacs? ( >=app-editors/emacs-23.1:* )
+	html? ( dev-tex/hevea )
+	hypothesis-selection? ( dev-ml/ocamlgraph )
+	zarith? ( dev-ml/zarith )
+	zip? ( >=dev-ml/camlzip-1.07 )"
+RDEPEND="${DEPEND}"
+
+S="${WORKDIR}"/${MYP}
+
+PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
+
+REQUIRED_USE="html? ( doc )"
+
+src_configure() {
+	econf \
+		--disable-pvs-libs \
+		--disable-isabelle-libs \
+		--enable-verbose-make \
+		$(use_enable coq coq-libs) \
+		$(use_enable doc) \
+		$(use_enable emacs emacs-compilation) \
+		$(use_enable gtk ide) \
+		$(use_enable html html-doc) \
+		$(use_enable hypothesis-selection) \
+		$(use_enable ocamlopt native-code) \
+		$(use_enable profiling) \
+		$(use_enable zarith) \
+		$(use_enable zip)
+}
+
+src_compile() {
+	emake -j1
+	if use ocamlopt; then
+		emake byte
+	fi
+	use doc && emake doc
+}
+
+src_install() {
+	emake DESTDIR="${D}" -j1 install
+	emake DESTDIR="${D}" -j1 install-lib
+	emake DESTDIR="${D}" install_spark2014_dev
+	dosym ../why3server /usr/$(get_libdir)/why3/commands/why3server
+	einstalldocs
+	docompress -x /usr/share/doc/${PF}/examples
+	dodoc -r examples
+	if use doc; then
+		dodoc doc/manual.pdf
+		use html && dodoc -r doc/html
+	fi
+}

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Ulrich Müller]

commit:     6c532ec926058d96e6d584075b63a32e4fb2c300
Author:     Ulrich Müller <ulm <AT> gentoo <DOT> org>
AuthorDate: Fri Dec 20 16:31:12 2019 +0000
Commit:     Ulrich Müller <ulm <AT> gentoo <DOT> org>
CommitDate: Fri Dec 20 22:48:52 2019 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=6c532ec9

sci-mathematics/why3-for-spark: Update virtual/emacs dependency.

The virtual is deprecated, depend on app-editors/emacs instead.

Package-Manager: Portage-2.3.82, Repoman-2.3.20
Signed-off-by: Ulrich Müller <ulm <AT> gentoo.org>

 sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild | 2 +-
 sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
index 5400b37276c..2335a61928f 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
@@ -23,7 +23,7 @@ DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
 	coq? ( sci-mathematics/coq )
 	doc? ( dev-tex/rubber )
 	gtk? ( dev-ml/lablgtk[sourceview] )
-	emacs? ( virtual/emacs )
+	emacs? ( >=app-editors/emacs-23.1:* )
 	html? ( dev-tex/hevea )
 	hypothesis-selection? ( dev-ml/ocamlgraph )
 	zarith? ( dev-ml/zarith )

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild
index a0caa7b6cf6..409bfc36cda 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild
@@ -23,7 +23,7 @@ DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
 	coq? ( sci-mathematics/coq )
 	doc? ( dev-tex/rubber )
 	gtk? ( dev-ml/lablgtk[sourceview] )
-	emacs? ( virtual/emacs )
+	emacs? ( >=app-editors/emacs-23.1:* )
 	html? ( dev-tex/hevea )
 	hypothesis-selection? ( dev-ml/ocamlgraph )
 	zarith? ( dev-ml/zarith )

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     f0437170eb42e30839073788456e18d5e695665b
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Fri Mar 15 07:24:05 2019 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Fri Mar 15 07:24:59 2019 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=f0437170

sci-mathematics/why3-for-spark: use virtual/emacs on dependency

Closes: https://bugs.gentoo.org/680312
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>
Package-Manager: Portage-2.3.51, Repoman-2.3.11

 sci-mathematics/why3-for-spark/Manifest            |  1 -
 .../why3-for-spark/why3-for-spark-2017.ebuild      | 83 ----------------------
 .../why3-for-spark/why3-for-spark-2018.ebuild      |  4 +-
 3 files changed, 2 insertions(+), 86 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest
index e6505ed60c7..8f9c5c3c62d 100644
--- a/sci-mathematics/why3-for-spark/Manifest
+++ b/sci-mathematics/why3-for-spark/Manifest
@@ -1,2 +1 @@
-DIST why3-for-spark-gpl-2017-src.tar.gz 9248235 BLAKE2B d9eb7201dfd5962c88ac8995e3cd800bf318f575a5e6ff7d0219941c0f0c9052e6b2c95c7c16fcd81b90cac647d503041bf16560bd44b58e7e0ced1ef2314bd2 SHA512 8f444402f6c1744cd7c565117732935791b1ae7996a94314c40a66d125eae8a81f2257314246c94fd29d3cd16abcff6a50a152a1191a4aae39a2c8a8d7c3b9e1
 DIST why3-for-spark-gpl-2018-src.tar.gz 7682767 BLAKE2B 0b0272ca4d5519ca402990b234d0847378bcd2a0949fea78ea10e355233a16aebe79b938cdf8e4daadabb909171cab83b9d6ccacf9f2dc1c0b57bb6da6fd1fe0 SHA512 fc798acf343484fd8e70f470a318753c9a0e9967ff579f20ec185bf3c2a75e7a4a556388fc86a378610ce4a467f3e722c6f610da34d4c33bc3d6b10551731f07

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
deleted file mode 100644
index d7e68eab372..00000000000
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
+++ /dev/null
@@ -1,83 +0,0 @@
-# Copyright 1999-2018 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=6
-
-inherit autotools
-
-MYP=${PN}-gpl-${PV}-src
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="http://mirrors.cdn.adacore.com/art/591c45e2c7a447af2deed055
-	-> ${MYP}.tar.gz"
-
-LICENSE="GPL-3"
-SLOT="0"
-KEYWORDS="amd64"
-IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
-RESTRICT=strip
-
-DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
-	dev-ml/menhir
-	coq? ( sci-mathematics/coq )
-	doc? ( dev-tex/rubber )
-	gtk? ( dev-ml/lablgtk[sourceview] )
-	emacs? ( app-editors/emacs:* )
-	html? ( dev-tex/hevea )
-	hypothesis-selection? ( dev-ml/ocamlgraph )
-	zarith? ( dev-ml/zarith )
-	zip? ( >=dev-ml/camlzip-1.07 )"
-RDEPEND="${DEPEND}"
-
-S="${WORKDIR}"/${MYP}
-
-PATCHES=( "${FILESDIR}"/${P}-gentoo.patch )
-
-REQUIRED_USE="html? ( doc )"
-
-src_prepare() {
-	mv configure.{in,ac} || die
-	sed -i \
-		-e "s:configure.in:configure.ac:g" \
-		Makefile.in
-	default
-	eautoreconf
-}
-
-src_configure() {
-	econf \
-		--disable-pvs-libs \
-		--disable-isabelle-libs \
-		$(use_enable coq coq-libs) \
-		$(use_enable coq coq-tactic) \
-		$(use_enable doc) \
-		$(use_enable emacs emacs-compilation) \
-		$(use_enable gtk ide) \
-		$(use_enable html html-doc) \
-		$(use_enable hypothesis-selection) \
-		$(use_enable ocamlopt native-code) \
-		$(use_enable profiling) \
-		$(use_enable zarith) \
-		$(use_enable zip)
-}
-
-src_compile() {
-	default
-	if use ocamlopt; then
-		emake byte
-	fi
-	use doc && emake doc
-}
-
-src_install() {
-	default
-	emake DESTDIR="${D}" install-lib
-	emake DESTDIR="${D}" install_spark2014_dev
-	docompress -x /usr/share/doc/${PF}/examples
-	dodoc -r examples
-	if use doc; then
-		dodoc doc/manual.pdf
-		use html && dodoc -r doc/html
-	fi
-}

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
index da20dbb96af..5400b37276c 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2018 Gentoo Authors
+# Copyright 1999-2019 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=6
@@ -23,7 +23,7 @@ DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
 	coq? ( sci-mathematics/coq )
 	doc? ( dev-tex/rubber )
 	gtk? ( dev-ml/lablgtk[sourceview] )
-	emacs? ( app-editors/emacs:* )
+	emacs? ( virtual/emacs )
 	html? ( dev-tex/hevea )
 	hypothesis-selection? ( dev-ml/ocamlgraph )
 	zarith? ( dev-ml/zarith )

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     05ca892773aa24c6dd3b8b0fa28d5aa261ffe4f0
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Sun Dec 16 08:36:37 2018 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Sun Dec 16 08:36:37 2018 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=05ca8927

sci-mathematics/why3-for-spark: Stable

Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>
Package-Manager: Portage-2.3.51, Repoman-2.3.11

 sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild | 4 ++--
 sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
index f79b8ccbe05..d7e68eab372 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2018 Gentoo Foundation
+# Copyright 1999-2018 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=6
@@ -14,7 +14,7 @@ SRC_URI="http://mirrors.cdn.adacore.com/art/591c45e2c7a447af2deed055
 
 LICENSE="GPL-3"
 SLOT="0"
-KEYWORDS="~amd64"
+KEYWORDS="amd64"
 IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
 RESTRICT=strip
 

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
index e766cce4ade..da20dbb96af 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2018 Gentoo Foundation
+# Copyright 1999-2018 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=6
@@ -14,7 +14,7 @@ SRC_URI="http://mirrors.cdn.adacore.com/art/5b0819dec7a447df26c27a43
 
 LICENSE="GPL-3"
 SLOT="0"
-KEYWORDS="~amd64"
+KEYWORDS="amd64"
 IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
 RESTRICT=strip
 

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     414f51e061f8082d6be5f1e342924bc8cf24ed3b
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Tue Mar 27 06:05:35 2018 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Tue Mar 27 06:05:35 2018 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=414f51e0

sci-mathematics/why3-for-spark: Fix STRIP_MASK usage. Bug #651458

Package-Manager: Portage-2.3.24, Repoman-2.3.6

 sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
index 1fa2034863d..f79b8ccbe05 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2017 Gentoo Foundation
+# Copyright 1999-2018 Gentoo Foundation
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=6
@@ -16,6 +16,7 @@ LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="~amd64"
 IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
+RESTRICT=strip
 
 DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
 	dev-ml/menhir
@@ -65,10 +66,6 @@ src_compile() {
 	default
 	if use ocamlopt; then
 		emake byte
-	else
-		# If using bytecode we dont want to strip the binary as it would remove
-		# the bytecode and only leave ocamlrun...
-		export STRIP_MASK="*/bin/*"
 	fi
 	use doc && emake doc
 }

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     ce9a2c2e5a2c8c7acc61c556147b7385139071a5
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Mon Nov  6 21:09:20 2017 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Mon Nov  6 21:09:20 2017 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ce9a2c2e

sci-mathematics/why3-for-spark: dev-ml/camlzip-1.06 causes problem.

Package-Manager: Portage-2.3.8, Repoman-2.3.3

 sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
index 63af700cd3e..1fa2034863d 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
@@ -26,7 +26,7 @@ DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
 	html? ( dev-tex/hevea )
 	hypothesis-selection? ( dev-ml/ocamlgraph )
 	zarith? ( dev-ml/zarith )
-	zip? ( dev-ml/camlzip )"
+	zip? ( >=dev-ml/camlzip-1.07 )"
 RDEPEND="${DEPEND}"
 
 S="${WORKDIR}"/${MYP}

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     8762ce2768ade2f75a3f87f4591bd30a3be88f21
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Sat Nov  4 20:46:39 2017 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Sat Nov  4 20:46:39 2017 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=8762ce27

sci-mathematics/why3-for-spark: Add ocamlopt use flag

Package-Manager: Portage-2.3.8, Repoman-2.3.3

 sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
index ca75d4898e4..63af700cd3e 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
@@ -15,9 +15,9 @@ SRC_URI="http://mirrors.cdn.adacore.com/art/591c45e2c7a447af2deed055
 LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk html hypothesis-selection profiling zarith zip"
+IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip"
 
-DEPEND=">=dev-lang/ocaml-4.02.3
+DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?]
 	dev-ml/menhir
 	coq? ( sci-mathematics/coq )
 	doc? ( dev-tex/rubber )
@@ -55,6 +55,7 @@ src_configure() {
 		$(use_enable gtk ide) \
 		$(use_enable html html-doc) \
 		$(use_enable hypothesis-selection) \
+		$(use_enable ocamlopt native-code) \
 		$(use_enable profiling) \
 		$(use_enable zarith) \
 		$(use_enable zip)
@@ -62,6 +63,13 @@ src_configure() {
 
 src_compile() {
 	default
+	if use ocamlopt; then
+		emake byte
+	else
+		# If using bytecode we dont want to strip the binary as it would remove
+		# the bytecode and only leave ocamlrun...
+		export STRIP_MASK="*/bin/*"
+	fi
 	use doc && emake doc
 }
 

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     9ca01a8eb0c26afe211e01dcea811b54b29f0b28
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Sat Nov  4 18:28:34 2017 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Sat Nov  4 18:28:34 2017 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=9ca01a8e

sci-mathematics/why3-for-spark: Install libraries

Package-Manager: Portage-2.3.8, Repoman-2.3.3

 sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild | 1 +
 1 file changed, 1 insertion(+)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
index 3fd44106514..ca75d4898e4 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
@@ -67,6 +67,7 @@ src_compile() {
 
 src_install() {
 	default
+	emake DESTDIR="${D}" install-lib
 	emake DESTDIR="${D}" install_spark2014_dev
 	docompress -x /usr/share/doc/${PF}/examples
 	dodoc -r examples

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     7e278f5c3b1dc15bbce41b0c5574dfae1db6fc51
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Wed Oct 25 17:28:48 2017 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Wed Oct 25 17:28:48 2017 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=7e278f5c

sci-mathematics/why3-for-spark: remove extra --disable-zip

Package-Manager: Portage-2.3.8, Repoman-2.3.3

 sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild | 1 -
 1 file changed, 1 deletion(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
index 0216951fd81..c143320a492 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
@@ -49,7 +49,6 @@ src_configure() {
 		--disable-coq-tactic \
 		--disable-pvs-libs \
 		--disable-isabelle-libs \
-		--disable-zip \
 		$(use_enable coq coq-libs) \
 		$(use_enable doc) \
 		$(use_enable emacs emacs-compilation) \

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     06a07ce4bfbcaf034558bb8a95c18e644b3683c6
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Tue Oct 24 19:58:51 2017 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Tue Oct 24 19:58:51 2017 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=06a07ce4

sci-mathematics/why3-for-spark: Add zip use flags

Package-Manager: Portage-2.3.8, Repoman-2.3.3

 sci-mathematics/why3-for-spark/metadata.xml               | 1 +
 sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild | 8 +++++---
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/metadata.xml b/sci-mathematics/why3-for-spark/metadata.xml
index f73ffa40b69..dfc2bea31bd 100644
--- a/sci-mathematics/why3-for-spark/metadata.xml
+++ b/sci-mathematics/why3-for-spark/metadata.xml
@@ -23,5 +23,6 @@
 		<flag name="hypothesis-selection">Enable hypothesis selection</flag>
 		<flag name="profiling">Enable profiling</flag>
 		<flag name="zarith">Use <pkg>dev-ml/zarith</pkg></flag>
+		<flag name="zip">Enable compression of session files</flag>
 	</use>
 </pkgmetadata>

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
index 596bdfc7fe1..0216951fd81 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
@@ -15,7 +15,7 @@ SRC_URI="http://mirrors.cdn.adacore.com/art/591c45e2c7a447af2deed055
 LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk html hypothesis-selection profiling zarith"
+IUSE="coq doc emacs gtk html hypothesis-selection profiling zarith zip"
 
 DEPEND=">=dev-lang/ocaml-4.02.3
 	dev-ml/menhir
@@ -25,7 +25,8 @@ DEPEND=">=dev-lang/ocaml-4.02.3
 	emacs? ( app-editors/emacs:* )
 	html? ( dev-tex/hevea )
 	hypothesis-selection? ( dev-ml/ocamlgraph )
-	zarith? ( dev-ml/zarith )"
+	zarith? ( dev-ml/zarith )
+	zip? ( dev-ml/camlzip )"
 RDEPEND="${DEPEND}"
 
 S="${WORKDIR}"/${MYP}
@@ -56,7 +57,8 @@ src_configure() {
 		$(use_enable html html-doc) \
 		$(use_enable hypothesis-selection) \
 		$(use_enable profiling) \
-		$(use_enable zarith)
+		$(use_enable zarith) \
+		$(use_enable zip)
 }
 
 src_compile() {

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     68056447a56bcd1c6d4ff5c342651190889c252a
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Tue Oct 24 18:32:44 2017 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Tue Oct 24 18:32:44 2017 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=68056447

sci-mathematics/why3-for-spark: Adding examples

Package-Manager: Portage-2.3.8, Repoman-2.3.3

 sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
index 956e82a9c41..596bdfc7fe1 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
@@ -67,6 +67,8 @@ src_compile() {
 src_install() {
 	default
 	emake DESTDIR="${D}" install_spark2014_dev
+	docompress -x /usr/share/doc/${PF}/examples
+	dodoc -r examples
 	if use doc; then
 		dodoc doc/manual.pdf
 		use html && dodoc -r doc/html

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     b9de4cea63a1f308a54f7fdfbe818a65bf9bcace
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Mon Oct 23 18:29:37 2017 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Mon Oct 23 18:30:36 2017 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=b9de4cea

sci-mathematics/why3-for-spark: Fix SRC_URI

Package-Manager: Portage-2.3.8, Repoman-2.3.3

 sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
index b69b22e506f..956e82a9c41 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2017.ebuild
@@ -9,7 +9,7 @@ MYP=${PN}-gpl-${PV}-src
 
 DESCRIPTION="Platform for deductive program verification"
 HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https//mirrors.cdn.adacore.com/art/591c45e2c7a447af2deed055
+SRC_URI="http://mirrors.cdn.adacore.com/art/591c45e2c7a447af2deed055
 	-> ${MYP}.tar.gz"
 
 LICENSE="GPL-3"

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/

[Alfredo Tupone]

commit:     cb97b25bd87da46462a3d73b4d5bcda6cc13f2e1
Author:     Tupone Alfredo <tupone <AT> gentoo <DOT> org>
AuthorDate: Fri Oct 20 05:48:20 2017 +0000
Commit:     Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Fri Oct 20 05:48:20 2017 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=cb97b25b

sci-mathematics/why3-for-spark: Fix metadata.xml

Package-Manager: Portage-2.3.8, Repoman-2.3.3

 sci-mathematics/why3-for-spark/metadata.xml | 46 ++++++++++++++---------------
 1 file changed, 23 insertions(+), 23 deletions(-)

diff --git a/sci-mathematics/why3-for-spark/metadata.xml b/sci-mathematics/why3-for-spark/metadata.xml
index 6dbb21558b6..f73ffa40b69 100644
--- a/sci-mathematics/why3-for-spark/metadata.xml
+++ b/sci-mathematics/why3-for-spark/metadata.xml
@@ -1,27 +1,27 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
 <pkgmetadata>
-<maintainer type="project">
-  <email>sci-mathematics@gentoo.org</email>
-  <name>Gentoo Mathematics Project</name>
-</maintainer>
-<longdescription>
-  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.
-</longdescription>
-<use>
-  <flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag>
-  <flag name="html">Build HTML documentation</flag>
-  <flag name="hypothesis-selection">Enable hypothesis selection</flag>
-  <flag name="profiling">Enable profiling</flag>
-  <flag name="zarith">Use <pkg>dev-ml/zarith</pkg></flag>
-</use>
+	<maintainer type="person">
+		<email>tupone@gentoo.org</email>
+		<name>Tupone Alfredo</name>
+	</maintainer>
+	<longdescription lang="en">
+		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.
+	</longdescription>
+	<use>
+		<flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag>
+		<flag name="html">Build HTML documentation</flag>
+		<flag name="hypothesis-selection">Enable hypothesis selection</flag>
+		<flag name="profiling">Enable profiling</flag>
+		<flag name="zarith">Use <pkg>dev-ml/zarith</pkg></flag>
+	</use>
 </pkgmetadata>