* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2017-10-20 5:48 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2017-10-20 5:48 UTC (permalink / raw
To: gentoo-commits
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>
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2017-10-23 18:30 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2017-10-23 18:30 UTC (permalink / raw
To: gentoo-commits
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"
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2017-10-24 18:33 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2017-10-24 18:33 UTC (permalink / raw
To: gentoo-commits
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
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2017-10-24 19:59 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2017-10-24 19:59 UTC (permalink / raw
To: gentoo-commits
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() {
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2017-10-25 17:29 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2017-10-25 17:29 UTC (permalink / raw
To: gentoo-commits
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) \
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2017-11-04 18:31 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2017-11-04 18:31 UTC (permalink / raw
To: gentoo-commits
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
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2017-11-04 20:46 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2017-11-04 20:46 UTC (permalink / raw
To: gentoo-commits
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
}
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2017-11-06 21:09 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2017-11-06 21:09 UTC (permalink / raw
To: gentoo-commits
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}
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2018-03-27 6:05 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2018-03-27 6:05 UTC (permalink / raw
To: gentoo-commits
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
}
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2018-12-16 8:36 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2018-12-16 8:36 UTC (permalink / raw
To: gentoo-commits
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
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2019-03-15 7:25 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2019-03-15 7:25 UTC (permalink / raw
To: gentoo-commits
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 )
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2019-12-20 22:49 Ulrich Müller
0 siblings, 0 replies; 37+ messages in thread
From: Ulrich Müller @ 2019-12-20 22:49 UTC (permalink / raw
To: gentoo-commits
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 )
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2020-01-14 7:52 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2020-01-14 7:52 UTC (permalink / raw
To: gentoo-commits
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
+}
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2020-01-15 8:19 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2020-01-15 8:19 UTC (permalink / raw
To: gentoo-commits
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:* )
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2020-01-16 10:09 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2020-01-16 10:09 UTC (permalink / raw
To: gentoo-commits
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 )
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2020-01-17 10:41 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2020-01-17 10:41 UTC (permalink / raw
To: gentoo-commits
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)
}
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2020-06-14 11:49 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2020-06-14 11:49 UTC (permalink / raw
To: gentoo-commits
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
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2020-06-15 17:20 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2020-06-15 17:20 UTC (permalink / raw
To: gentoo-commits
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
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2021-01-17 4:10 Sam James
0 siblings, 0 replies; 37+ messages in thread
From: Sam James @ 2021-01-17 4:10 UTC (permalink / raw
To: gentoo-commits
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 )
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2021-01-17 4:10 Sam James
0 siblings, 0 replies; 37+ messages in thread
From: Sam James @ 2021-01-17 4:10 UTC (permalink / raw
To: gentoo-commits
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}
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2021-02-10 17:25 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2021-02-10 17:25 UTC (permalink / raw
To: gentoo-commits
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
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2021-06-29 14:16 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2021-06-29 14:16 UTC (permalink / raw
To: gentoo-commits
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) \
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2021-09-18 16:51 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2021-09-18 16:51 UTC (permalink / raw
To: gentoo-commits
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"
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2022-02-06 17:41 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2022-02-06 17:41 UTC (permalink / raw
To: gentoo-commits
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 )
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2022-02-07 9:55 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2022-02-07 9:55 UTC (permalink / raw
To: gentoo-commits
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
)
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2022-02-07 9:57 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2022-02-07 9:57 UTC (permalink / raw
To: gentoo-commits
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
)
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2022-02-07 12:50 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2022-02-07 12:50 UTC (permalink / raw
To: gentoo-commits
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:=
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2022-02-07 21:48 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2022-02-07 21:48 UTC (permalink / raw
To: gentoo-commits
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}
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2022-03-11 21:01 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2022-03-11 21:01 UTC (permalink / raw
To: gentoo-commits
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() {
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2022-06-27 6:19 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2022-06-27 6:19 UTC (permalink / raw
To: gentoo-commits
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
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2022-06-27 8:47 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2022-06-27 8:47 UTC (permalink / raw
To: gentoo-commits
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
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2022-07-26 19:54 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2022-07-26 19:54 UTC (permalink / raw
To: gentoo-commits
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"
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2022-11-26 13:47 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2022-11-26 13:47 UTC (permalink / raw
To: gentoo-commits
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) \
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2023-03-31 13:13 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2023-03-31 13:13 UTC (permalink / raw
To: gentoo-commits
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:= )
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2023-04-02 11:27 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2023-04-02 11:27 UTC (permalink / raw
To: gentoo-commits
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"
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2023-04-02 13:21 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2023-04-02 13:21 UTC (permalink / raw
To: gentoo-commits
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"
^ permalink raw reply related [flat|nested] 37+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/
@ 2023-12-29 22:44 Alfredo Tupone
0 siblings, 0 replies; 37+ messages in thread
From: Alfredo Tupone @ 2023-12-29 22:44 UTC (permalink / raw
To: gentoo-commits
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
^ permalink raw reply related [flat|nested] 37+ messages in thread
end of thread, other threads:[~2023-12-29 22:44 UTC | newest]
Thread overview: 37+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2017-11-04 18:31 [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3-for-spark/ Alfredo Tupone
-- strict thread matches above, loose matches on Subject: below --
2023-12-29 22:44 Alfredo Tupone
2023-04-02 13:21 Alfredo Tupone
2023-04-02 11:27 Alfredo Tupone
2023-03-31 13:13 Alfredo Tupone
2022-11-26 13:47 Alfredo Tupone
2022-07-26 19:54 Alfredo Tupone
2022-06-27 8:47 Alfredo Tupone
2022-06-27 6:19 Alfredo Tupone
2022-03-11 21:01 Alfredo Tupone
2022-02-07 21:48 Alfredo Tupone
2022-02-07 12:50 Alfredo Tupone
2022-02-07 9:57 Alfredo Tupone
2022-02-07 9:55 Alfredo Tupone
2022-02-06 17:41 Alfredo Tupone
2021-09-18 16:51 Alfredo Tupone
2021-06-29 14:16 Alfredo Tupone
2021-02-10 17:25 Alfredo Tupone
2021-01-17 4:10 Sam James
2021-01-17 4:10 Sam James
2020-06-15 17:20 Alfredo Tupone
2020-06-14 11:49 Alfredo Tupone
2020-01-17 10:41 Alfredo Tupone
2020-01-16 10:09 Alfredo Tupone
2020-01-15 8:19 Alfredo Tupone
2020-01-14 7:52 Alfredo Tupone
2019-12-20 22:49 Ulrich Müller
2019-03-15 7:25 Alfredo Tupone
2018-12-16 8:36 Alfredo Tupone
2018-03-27 6:05 Alfredo Tupone
2017-11-06 21:09 Alfredo Tupone
2017-11-04 20:46 Alfredo Tupone
2017-10-25 17:29 Alfredo Tupone
2017-10-24 19:59 Alfredo Tupone
2017-10-24 18:33 Alfredo Tupone
2017-10-23 18:30 Alfredo Tupone
2017-10-20 5:48 Alfredo Tupone
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox