* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2021-12-12 1:59 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2021-12-12 1:59 UTC (permalink / raw
To: gentoo-commits
commit: afa23b7e71a8114ea0919675d3d4029f6d6b6176
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sun Dec 12 00:56:49 2021 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sun Dec 12 01:59:46 2021 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=afa23b7e
sci-mathematics/why3: new package; add version 1.4.0
Move from ::guru to ::gentoo,
add François-Xavier Carton as a co-maintainer.
Package-Manager: Portage-3.0.28, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/Manifest | 1 +
sci-mathematics/why3/metadata.xml | 33 ++++++++++++
sci-mathematics/why3/why3-1.4.0.ebuild | 92 ++++++++++++++++++++++++++++++++++
3 files changed, 126 insertions(+)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
new file mode 100644
index 000000000000..a5e04572eda6
--- /dev/null
+++ b/sci-mathematics/why3/Manifest
@@ -0,0 +1 @@
+DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5 SHA512 b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
new file mode 100644
index 000000000000..6c2999e4f4d7
--- /dev/null
+++ b/sci-mathematics/why3/metadata.xml
@@ -0,0 +1,33 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+ <maintainer type="person" proxied="yes">
+ <name>François-Xavier Carton</name>
+ <email>fx.carton91@gmail.com</email>
+ </maintainer>
+ <maintainer type="project">
+ <email>ml@gentoo.org</email>
+ <name>ML</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="gtk">Build the IDE <pkg>x11-libs/gtk+</pkg></flag>
+ <flag name="re">Use Re (<pkg>dev-ml/re</pkg>) instead of Str for regular expressions</flag>
+ <flag name="sexp">Add support for outputting S-expressions with <pkg>dev-ml/ppx_sexp_conv</pkg></flag>
+ <flag name="zarith">Use Zarith (<pkg>dev-ml/zarith</pkg>) instead of Nums (<pkg>dev-ml/num</pkg>) for computations</flag>
+ <flag name="zip">Enable compression of session files</flag>
+ </use>
+</pkgmetadata>
diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild b/sci-mathematics/why3/why3-1.4.0.ebuild
new file mode 100644
index 000000000000..42012b020215
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.4.0.ebuild
@@ -0,0 +1,92 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+inherit autotools findlib
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/"
+SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0/${PV}"
+KEYWORDS="~amd64"
+IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
+
+RDEPEND="
+ !sci-mathematics/why3-for-spark
+ >=dev-lang/ocaml-4.05.0[ocamlopt?]
+ >=dev-ml/menhir-20151112
+ dev-ml/num
+ coq? ( >=sci-mathematics/coq-8.6 )
+ doc? (
+ dev-python/sphinx
+ dev-python/sphinxcontrib-bibtex
+ || ( dev-texlive/texlive-latex dev-tex/latexmk dev-tex/rubber )
+ )
+ emacs? ( app-editors/emacs:* )
+ gtk? ( dev-ml/lablgtk:*[sourceview,ocamlopt?] )
+ re? ( dev-ml/re dev-ml/seq )
+ sexp? (
+ dev-ml/ppx_deriving[ocamlopt?]
+ dev-ml/ppx_sexp_conv[ocamlopt?]
+ dev-ml/sexplib[ocamlopt?]
+ )
+ zarith? ( dev-ml/zarith )
+ zip? ( dev-ml/camlzip )
+"
+DEPEND="${RDEPEND}"
+
+DOCS=( CHANGES.md README.md )
+
+src_prepare() {
+ mv configure.in configure.ac || die
+ sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+ sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
+ -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+ -i Makefile.in || die
+
+ eautoreconf
+ default
+}
+
+src_configure() {
+ local myconf=(
+ --disable-hypothesis-selection
+ --disable-pvs-libs
+ --disable-isabelle-libs
+ --disable-frama-c
+ --disable-infer
+ --disable-web-ide
+ $(use_enable coq coq-libs)
+ $(use_enable doc)
+ $(use_enable emacs emacs-compilation)
+ $(use_enable gtk ide)
+ $(use_enable ocamlopt native-code)
+ $(use_enable re)
+ $(use_enable sexp pp-sexp)
+ $(use_enable zarith)
+ $(use_enable zip)
+ )
+ econf "${myconf[@]}"
+}
+
+src_compile() {
+ emake
+ emake plugins
+ use doc && emake doc
+}
+
+src_install(){
+ findlib_src_preinst
+ emake install install-lib DESTDIR="${ED}"
+
+ einstalldocs
+ docompress -x /usr/share/doc/${PF}/examples
+ dodoc -r examples
+ if use doc; then
+ dodoc doc/latex/manual.pdf
+ dodoc -r doc/html
+ fi
+}
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2021-12-12 12:14 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2021-12-12 12:14 UTC (permalink / raw
To: gentoo-commits
commit: 61686012dfc33cda5b87f4726ffce518c68897dc
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sun Dec 12 12:13:18 2021 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sun Dec 12 12:14:50 2021 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=61686012
sci-mathematics/why3: fix *DEPEND
Closes: https://bugs.gentoo.org/828974
Package-Manager: Portage-3.0.28, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
.../{why3-1.4.0.ebuild => why3-1.4.0-r1.ebuild} | 31 ++++++++++++----------
1 file changed, 17 insertions(+), 14 deletions(-)
diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild b/sci-mathematics/why3/why3-1.4.0-r1.ebuild
similarity index 83%
rename from sci-mathematics/why3/why3-1.4.0.ebuild
rename to sci-mathematics/why3/why3-1.4.0-r1.ebuild
index 42012b020215..badf49628e94 100644
--- a/sci-mathematics/why3/why3-1.4.0.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0-r1.ebuild
@@ -16,27 +16,30 @@ IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
RDEPEND="
!sci-mathematics/why3-for-spark
- >=dev-lang/ocaml-4.05.0[ocamlopt?]
- >=dev-ml/menhir-20151112
- dev-ml/num
+ >=dev-lang/ocaml-4.05.0:=[ocamlopt?]
+ >=dev-ml/menhir-20151112:=
+ dev-ml/num:=
coq? ( >=sci-mathematics/coq-8.6 )
+ emacs? ( app-editors/emacs:* )
+ gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
+ re? ( dev-ml/re:= dev-ml/seq:= )
+ 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-python/sphinx
dev-python/sphinxcontrib-bibtex
+ media-gfx/graphviz
|| ( dev-texlive/texlive-latex dev-tex/latexmk dev-tex/rubber )
)
- emacs? ( app-editors/emacs:* )
- gtk? ( dev-ml/lablgtk:*[sourceview,ocamlopt?] )
- re? ( dev-ml/re dev-ml/seq )
- sexp? (
- dev-ml/ppx_deriving[ocamlopt?]
- dev-ml/ppx_sexp_conv[ocamlopt?]
- dev-ml/sexplib[ocamlopt?]
- )
- zarith? ( dev-ml/zarith )
- zip? ( dev-ml/camlzip )
"
-DEPEND="${RDEPEND}"
DOCS=( CHANGES.md README.md )
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2022-01-13 16:41 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2022-01-13 16:41 UTC (permalink / raw
To: gentoo-commits
commit: c87b6eaca316012d6da22935421b4279bd91b128
Author: François-Xavier Carton <fx.carton91 <AT> gmail <DOT> com>
AuthorDate: Wed Jan 12 22:34:35 2022 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Jan 13 16:38:07 2022 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c87b6eac
sci-mathematics/why3: add missing latex dependencies
Closes: https://bugs.gentoo.org/828997
Closes: https://github.com/gentoo/gentoo/pull/23774
Signed-off-by: François-Xavier Carton <fx.carton91 <AT> gmail.com>
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/{why3-1.4.0-r1.ebuild => why3-1.4.0-r2.ebuild} | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/sci-mathematics/why3/why3-1.4.0-r1.ebuild b/sci-mathematics/why3/why3-1.4.0-r2.ebuild
similarity index 95%
rename from sci-mathematics/why3/why3-1.4.0-r1.ebuild
rename to sci-mathematics/why3/why3-1.4.0-r2.ebuild
index badf49628e94..cb84e64b2802 100644
--- a/sci-mathematics/why3/why3-1.4.0-r1.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0-r2.ebuild
@@ -37,7 +37,9 @@ BDEPEND="
dev-python/sphinx
dev-python/sphinxcontrib-bibtex
media-gfx/graphviz
- || ( dev-texlive/texlive-latex dev-tex/latexmk dev-tex/rubber )
+ dev-texlive/texlive-latex
+ dev-texlive/texlive-fontsrecommended
+ dev-texlive/texlive-latexextra
)
"
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2022-01-15 6:08 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2022-01-15 6:08 UTC (permalink / raw
To: gentoo-commits
commit: 5377b0ede6969e3ce4b0c0b2b019b3835f5a7c62
Author: François-Xavier Carton <fx.carton91 <AT> gmail <DOT> com>
AuthorDate: Sat Jan 15 02:20:22 2022 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Jan 15 06:00:17 2022 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=5377b0ed
sci-mathematics/why3: fix race condition in parallel make doc
"make doc" uses sphinx to build both latex and html documentation. Both
sphinx rules in the makefile include "-d doc/.doctrees", ie. the same
path for "the cached environment and doctree files". In a parallel make
build, the rules are called simulateously, which means the cached files
could be read by one process while they are still being written by the
other.
Closes: https://bugs.gentoo.org/831168
Signed-off-by: François-Xavier Carton <fx.carton91 <AT> gmail.com>
Closes: https://github.com/gentoo/gentoo/pull/23802
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/why3-1.4.0-r2.ebuild | 1 +
1 file changed, 1 insertion(+)
diff --git a/sci-mathematics/why3/why3-1.4.0-r2.ebuild b/sci-mathematics/why3/why3-1.4.0-r2.ebuild
index cb84e64b2802..85da04d96b8a 100644
--- a/sci-mathematics/why3/why3-1.4.0-r2.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0-r2.ebuild
@@ -50,6 +50,7 @@ src_prepare() {
sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
-e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+ -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
-i Makefile.in || die
eautoreconf
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2022-01-17 21:23 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2022-01-17 21:23 UTC (permalink / raw
To: gentoo-commits
commit: 586be943f77e4b876942a5768b12f4fb4762c2bd
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Mon Jan 17 21:22:51 2022 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Mon Jan 17 21:22:51 2022 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=586be943
sci-mathematics/why3: add sci-mathematics to maintainers
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/metadata.xml | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
index 6c2999e4f4d7..97474dfdb2ec 100644
--- a/sci-mathematics/why3/metadata.xml
+++ b/sci-mathematics/why3/metadata.xml
@@ -10,6 +10,10 @@
<email>ml@gentoo.org</email>
<name>ML</name>
</maintainer>
+ <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,
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2022-03-04 11:06 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2022-03-04 11:06 UTC (permalink / raw
To: gentoo-commits
commit: da140912911bef67070defaa18676a365f269cf2
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Fri Mar 4 11:02:09 2022 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Fri Mar 4 11:02:09 2022 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=da140912
sci-mathematics/why3: bump to 1.4.1
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/Manifest | 1 +
sci-mathematics/why3/why3-1.4.1.ebuild | 98 ++++++++++++++++++++++++++++++++++
2 files changed, 99 insertions(+)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index a5e04572eda6..5eda325aedbe 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1 +1,2 @@
DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5 SHA512 b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
+DIST why3-1.4.1.tar.gz 6305011 BLAKE2B 2d916fbf333550f8021bff9e7ccf4ca5685763ca7f82ae133298feaf96f3e8b36290a103fd27224fb6fb2dc36c8d7ad5d93ffc92e8cf7fe1a61abb5a40aecb39 SHA512 7990519179c088be1bc9b5b6d469f6d6fbd683445e20cbf5edd5c97682f2931b2657a92b60e539d7647033bfdc5a63401f28af61fd9b14b41011144afa2016e0
diff --git a/sci-mathematics/why3/why3-1.4.1.ebuild b/sci-mathematics/why3/why3-1.4.1.ebuild
new file mode 100644
index 000000000000..a9a9ef515374
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.4.1.ebuild
@@ -0,0 +1,98 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+inherit autotools findlib
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/"
+SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0/${PV}"
+KEYWORDS="~amd64"
+IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
+
+RDEPEND="
+ !sci-mathematics/why3-for-spark
+ >=dev-lang/ocaml-4.05.0:=[ocamlopt?]
+ >=dev-ml/menhir-20151112:=
+ dev-ml/num:=
+ coq? ( >=sci-mathematics/coq-8.6 )
+ emacs? ( app-editors/emacs:* )
+ gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
+ re? ( dev-ml/re:= dev-ml/seq:= )
+ 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-python/sphinx
+ dev-python/sphinxcontrib-bibtex
+ media-gfx/graphviz
+ dev-texlive/texlive-latex
+ dev-texlive/texlive-fontsrecommended
+ dev-texlive/texlive-latexextra
+ )
+"
+
+DOCS=( CHANGES.md README.md )
+
+src_prepare() {
+ mv configure.in configure.ac || die
+ sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+ sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
+ -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+ -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
+ -i Makefile.in || die
+
+ eautoreconf
+ default
+}
+
+src_configure() {
+ local myconf=(
+ --disable-hypothesis-selection
+ --disable-pvs-libs
+ --disable-isabelle-libs
+ --disable-frama-c
+ --disable-infer
+ --disable-web-ide
+ $(use_enable coq coq-libs)
+ $(use_enable doc)
+ $(use_enable emacs emacs-compilation)
+ $(use_enable gtk ide)
+ $(use_enable ocamlopt native-code)
+ $(use_enable re)
+ $(use_enable sexp pp-sexp)
+ $(use_enable zarith)
+ $(use_enable zip)
+ )
+ econf "${myconf[@]}"
+}
+
+src_compile() {
+ emake
+ emake plugins
+ use doc && emake doc
+}
+
+src_install(){
+ findlib_src_preinst
+ emake install install-lib DESTDIR="${ED}"
+
+ einstalldocs
+ docompress -x /usr/share/doc/${PF}/examples
+ dodoc -r examples
+ if use doc; then
+ dodoc doc/latex/manual.pdf
+ dodoc -r doc/html
+ fi
+}
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2022-04-16 21:25 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2022-04-16 21:25 UTC (permalink / raw
To: gentoo-commits
commit: e0300e30cdf32fdb0d0ca67c9eb6c3e5e53e5bf3
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Apr 16 21:24:31 2022 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Apr 16 21:24:41 2022 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e0300e30
sci-mathematics/why3: increase required menhir version
this is a very minor change to keep it in sync with
https://opam.ocaml.org/packages/why3
also, no bump is needed since 20170418 version
is long gone from ::gentoo
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/why3-1.4.0-r2.ebuild | 4 ++--
sci-mathematics/why3/why3-1.4.1.ebuild | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/sci-mathematics/why3/why3-1.4.0-r2.ebuild b/sci-mathematics/why3/why3-1.4.0-r2.ebuild
index 85da04d96b8a..efe23fa3bbde 100644
--- a/sci-mathematics/why3/why3-1.4.0-r2.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0-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
@@ -17,7 +17,7 @@ IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
RDEPEND="
!sci-mathematics/why3-for-spark
>=dev-lang/ocaml-4.05.0:=[ocamlopt?]
- >=dev-ml/menhir-20151112:=
+ >=dev-ml/menhir-20170418:=
dev-ml/num:=
coq? ( >=sci-mathematics/coq-8.6 )
emacs? ( app-editors/emacs:* )
diff --git a/sci-mathematics/why3/why3-1.4.1.ebuild b/sci-mathematics/why3/why3-1.4.1.ebuild
index a9a9ef515374..efe23fa3bbde 100644
--- a/sci-mathematics/why3/why3-1.4.1.ebuild
+++ b/sci-mathematics/why3/why3-1.4.1.ebuild
@@ -17,7 +17,7 @@ IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
RDEPEND="
!sci-mathematics/why3-for-spark
>=dev-lang/ocaml-4.05.0:=[ocamlopt?]
- >=dev-ml/menhir-20151112:=
+ >=dev-ml/menhir-20170418:=
dev-ml/num:=
coq? ( >=sci-mathematics/coq-8.6 )
emacs? ( app-editors/emacs:* )
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2022-05-07 16:50 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2022-05-07 16:50 UTC (permalink / raw
To: gentoo-commits
commit: 7a4a24d0168c9092f69cafa35ca1872d7e77e0de
Author: François-Xavier Carton <fx.carton91 <AT> gmail <DOT> com>
AuthorDate: Sat May 7 16:15:12 2022 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat May 7 16:50:25 2022 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=7a4a24d0
sci-mathematics/why3: bump to 1.5.0
Signed-off-by: François-Xavier Carton <fx.carton91 <AT> gmail.com>
Closes: https://github.com/gentoo/gentoo/pull/25372
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/Manifest | 1 +
sci-mathematics/why3/metadata.xml | 1 +
sci-mathematics/why3/why3-1.5.0.ebuild | 103 +++++++++++++++++++++++++++++++++
3 files changed, 105 insertions(+)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index 5eda325aedbe..e4d7b6aceaad 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,2 +1,3 @@
DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5 SHA512 b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
DIST why3-1.4.1.tar.gz 6305011 BLAKE2B 2d916fbf333550f8021bff9e7ccf4ca5685763ca7f82ae133298feaf96f3e8b36290a103fd27224fb6fb2dc36c8d7ad5d93ffc92e8cf7fe1a61abb5a40aecb39 SHA512 7990519179c088be1bc9b5b6d469f6d6fbd683445e20cbf5edd5c97682f2931b2657a92b60e539d7647033bfdc5a63401f28af61fd9b14b41011144afa2016e0
+DIST why3-1.5.0.tar.gz 6723500 BLAKE2B e6ae5034cf0b3923dfaa760d604f754d4e385ea92ca1f70c7d4bd9985c75192ed381bb50d7211451f35d485e5c0969b3de4987603720b2fd6609cca5d074b85f SHA512 3ae443733321f2e487d6e503c4dbfe37d0e24c7dbe88eb94a3907775a1e6e30530b58ff835e3b2fff3fac5cd16622d758602e4f2b59aea567c7073199d67888c
diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
index 9974e9e2b8a1..c8d6f06359fb 100644
--- a/sci-mathematics/why3/metadata.xml
+++ b/sci-mathematics/why3/metadata.xml
@@ -31,6 +31,7 @@
<flag name="gtk">Build the IDE <pkg>x11-libs/gtk+</pkg></flag>
<flag name="re">Use Re (<pkg>dev-ml/re</pkg>) instead of Str for regular expressions</flag>
<flag name="sexp">Add support for outputting S-expressions with <pkg>dev-ml/ppx_sexp_conv</pkg></flag>
+ <flag name="stackify">Enable structure reconstruction algorithm for MLCFG</flag>
<flag name="zarith">Use Zarith (<pkg>dev-ml/zarith</pkg>) instead of Nums (<pkg>dev-ml/num</pkg>) for computations</flag>
<flag name="zip">Enable compression of session files</flag>
</use>
diff --git a/sci-mathematics/why3/why3-1.5.0.ebuild b/sci-mathematics/why3/why3-1.5.0.ebuild
new file mode 100644
index 000000000000..9c250c09c3d0
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.5.0.ebuild
@@ -0,0 +1,103 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+inherit autotools findlib
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/"
+SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0/${PV}"
+KEYWORDS="~amd64"
+IUSE="coq doc emacs gtk +ocamlopt re sexp stackify +zarith zip"
+
+RDEPEND="
+ !sci-mathematics/why3-for-spark
+ >=dev-lang/ocaml-4.05.0:=[ocamlopt?]
+ >=dev-ml/menhir-20170418:=
+ dev-ml/num:=
+ coq? ( >=sci-mathematics/coq-8.7 )
+ emacs? ( app-editors/emacs:* )
+ gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
+ re? ( dev-ml/re:= dev-ml/seq:= )
+ sexp? (
+ dev-ml/ppx_deriving:=[ocamlopt?]
+ dev-ml/ppx_sexp_conv:=[ocamlopt?]
+ dev-ml/sexplib:=[ocamlopt?]
+ )
+ stackify? ( dev-ml/ocamlgraph:=[ocamlopt?] )
+ zarith? ( dev-ml/zarith:= )
+ zip? ( dev-ml/camlzip:= )
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
+ doc? (
+ dev-python/sphinx
+ dev-python/sphinxcontrib-bibtex
+ media-gfx/graphviz
+ dev-texlive/texlive-latex
+ dev-texlive/texlive-fontsrecommended
+ dev-texlive/texlive-latexextra
+ )
+"
+
+DOCS=( CHANGES.md README.md )
+
+src_prepare() {
+ mv configure.in configure.ac || die
+ sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+ sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
+ -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+ -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
+ -i Makefile.in || die
+
+ # remove QA warning about duplicated compressed file:
+ rm examples/mlcfg/basic/why3shapes.gz || die
+
+ eautoreconf
+ default
+}
+
+src_configure() {
+ local myconf=(
+ --disable-hypothesis-selection
+ --disable-pvs-libs
+ --disable-isabelle-libs
+ --disable-frama-c
+ --disable-infer
+ --disable-web-ide
+ $(use_enable coq coq-libs)
+ $(use_enable doc)
+ $(use_enable emacs emacs-compilation)
+ $(use_enable gtk ide)
+ $(use_enable ocamlopt native-code)
+ $(use_enable re)
+ $(use_enable sexp pp-sexp)
+ $(use_enable stackify)
+ $(use_enable zarith)
+ $(use_enable zip)
+ )
+ econf "${myconf[@]}"
+}
+
+src_compile() {
+ emake
+ emake plugins
+ use doc && emake doc
+}
+
+src_install(){
+ findlib_src_preinst
+ emake install install-lib DESTDIR="${ED}"
+
+ einstalldocs
+ docompress -x /usr/share/doc/${PF}/examples
+ dodoc -r examples
+ if use doc; then
+ dodoc doc/latex/manual.pdf
+ dodoc -r doc/html
+ fi
+}
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2022-07-23 0:06 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2022-07-23 0:06 UTC (permalink / raw
To: gentoo-commits
commit: 28fa4c56bba04fe751e45cff07af6e2285bca741
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Fri Jul 22 22:23:52 2022 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Jul 23 00:03:18 2022 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=28fa4c56
sci-mathematics/why3: remove unnecessary seq dependency
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/{why3-1.4.0-r2.ebuild => why3-1.4.0-r3.ebuild} | 2 +-
sci-mathematics/why3/{why3-1.4.1.ebuild => why3-1.4.1-r1.ebuild} | 2 +-
sci-mathematics/why3/{why3-1.5.0.ebuild => why3-1.5.0-r1.ebuild} | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/sci-mathematics/why3/why3-1.4.0-r2.ebuild b/sci-mathematics/why3/why3-1.4.0-r3.ebuild
similarity index 98%
rename from sci-mathematics/why3/why3-1.4.0-r2.ebuild
rename to sci-mathematics/why3/why3-1.4.0-r3.ebuild
index efe23fa3bbde..e57cc66c0237 100644
--- a/sci-mathematics/why3/why3-1.4.0-r2.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0-r3.ebuild
@@ -22,7 +22,7 @@ RDEPEND="
coq? ( >=sci-mathematics/coq-8.6 )
emacs? ( app-editors/emacs:* )
gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
- re? ( dev-ml/re:= dev-ml/seq:= )
+ re? ( dev-ml/re:= )
sexp? (
dev-ml/ppx_deriving:=[ocamlopt?]
dev-ml/ppx_sexp_conv:=[ocamlopt?]
diff --git a/sci-mathematics/why3/why3-1.4.1.ebuild b/sci-mathematics/why3/why3-1.4.1-r1.ebuild
similarity index 98%
rename from sci-mathematics/why3/why3-1.4.1.ebuild
rename to sci-mathematics/why3/why3-1.4.1-r1.ebuild
index efe23fa3bbde..e57cc66c0237 100644
--- a/sci-mathematics/why3/why3-1.4.1.ebuild
+++ b/sci-mathematics/why3/why3-1.4.1-r1.ebuild
@@ -22,7 +22,7 @@ RDEPEND="
coq? ( >=sci-mathematics/coq-8.6 )
emacs? ( app-editors/emacs:* )
gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
- re? ( dev-ml/re:= dev-ml/seq:= )
+ re? ( dev-ml/re:= )
sexp? (
dev-ml/ppx_deriving:=[ocamlopt?]
dev-ml/ppx_sexp_conv:=[ocamlopt?]
diff --git a/sci-mathematics/why3/why3-1.5.0.ebuild b/sci-mathematics/why3/why3-1.5.0-r1.ebuild
similarity index 98%
rename from sci-mathematics/why3/why3-1.5.0.ebuild
rename to sci-mathematics/why3/why3-1.5.0-r1.ebuild
index 9c250c09c3d0..5f542a4b9e57 100644
--- a/sci-mathematics/why3/why3-1.5.0.ebuild
+++ b/sci-mathematics/why3/why3-1.5.0-r1.ebuild
@@ -22,7 +22,7 @@ RDEPEND="
coq? ( >=sci-mathematics/coq-8.7 )
emacs? ( app-editors/emacs:* )
gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
- re? ( dev-ml/re:= dev-ml/seq:= )
+ re? ( dev-ml/re:= )
sexp? (
dev-ml/ppx_deriving:=[ocamlopt?]
dev-ml/ppx_sexp_conv:=[ocamlopt?]
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2022-07-26 19:54 Alfredo Tupone
0 siblings, 0 replies; 16+ messages in thread
From: Alfredo Tupone @ 2022-07-26 19:54 UTC (permalink / raw
To: gentoo-commits
commit: 5c16384ca80bcca7f7bf0b7d5926e8ef5d3867d9
Author: Michael Mair-Keimberger <mmk <AT> levelnine <DOT> at>
AuthorDate: Tue Jul 26 19:38:11 2022 +0000
Commit: Alfredo Tupone <tupone <AT> gentoo <DOT> org>
CommitDate: Tue Jul 26 19:54:10 2022 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=5c16384c
sci-mathematics/why3: use https
Signed-off-by: Michael Mair-Keimberger <mmk <AT> levelnine.at>
Portage 3.0.34 / pkgdev 0.2.1 / pkgcheck 0.10.11
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org>
sci-mathematics/why3/why3-1.4.0-r3.ebuild | 2 +-
sci-mathematics/why3/why3-1.4.1-r1.ebuild | 2 +-
sci-mathematics/why3/why3-1.5.0-r1.ebuild | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/sci-mathematics/why3/why3-1.4.0-r3.ebuild b/sci-mathematics/why3/why3-1.4.0-r3.ebuild
index e57cc66c0237..6d1e01d9863c 100644
--- a/sci-mathematics/why3/why3-1.4.0-r3.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0-r3.ebuild
@@ -6,7 +6,7 @@ EAPI=7
inherit autotools findlib
DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
+HOMEPAGE="https://why3.lri.fr/"
SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
LICENSE="LGPL-2"
diff --git a/sci-mathematics/why3/why3-1.4.1-r1.ebuild b/sci-mathematics/why3/why3-1.4.1-r1.ebuild
index e57cc66c0237..6d1e01d9863c 100644
--- a/sci-mathematics/why3/why3-1.4.1-r1.ebuild
+++ b/sci-mathematics/why3/why3-1.4.1-r1.ebuild
@@ -6,7 +6,7 @@ EAPI=7
inherit autotools findlib
DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
+HOMEPAGE="https://why3.lri.fr/"
SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
LICENSE="LGPL-2"
diff --git a/sci-mathematics/why3/why3-1.5.0-r1.ebuild b/sci-mathematics/why3/why3-1.5.0-r1.ebuild
index 5f542a4b9e57..d592ff2803b1 100644
--- a/sci-mathematics/why3/why3-1.5.0-r1.ebuild
+++ b/sci-mathematics/why3/why3-1.5.0-r1.ebuild
@@ -6,7 +6,7 @@ EAPI=7
inherit autotools findlib
DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
+HOMEPAGE="https://why3.lri.fr/"
SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
LICENSE="LGPL-2"
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2022-09-19 18:59 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2022-09-19 18:59 UTC (permalink / raw
To: gentoo-commits
commit: 0e667f1eec8cf52339e41e209591281258574fc7
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Mon Sep 19 18:44:26 2022 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Mon Sep 19 18:59:23 2022 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0e667f1e
sci-mathematics/why3: bump to 1.5.1
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/Manifest | 1 +
sci-mathematics/why3/why3-1.5.1.ebuild | 103 +++++++++++++++++++++++++++++++++
2 files changed, 104 insertions(+)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index e4d7b6aceaad..4f6bc6bc9f21 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,3 +1,4 @@
DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5 SHA512 b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
DIST why3-1.4.1.tar.gz 6305011 BLAKE2B 2d916fbf333550f8021bff9e7ccf4ca5685763ca7f82ae133298feaf96f3e8b36290a103fd27224fb6fb2dc36c8d7ad5d93ffc92e8cf7fe1a61abb5a40aecb39 SHA512 7990519179c088be1bc9b5b6d469f6d6fbd683445e20cbf5edd5c97682f2931b2657a92b60e539d7647033bfdc5a63401f28af61fd9b14b41011144afa2016e0
DIST why3-1.5.0.tar.gz 6723500 BLAKE2B e6ae5034cf0b3923dfaa760d604f754d4e385ea92ca1f70c7d4bd9985c75192ed381bb50d7211451f35d485e5c0969b3de4987603720b2fd6609cca5d074b85f SHA512 3ae443733321f2e487d6e503c4dbfe37d0e24c7dbe88eb94a3907775a1e6e30530b58ff835e3b2fff3fac5cd16622d758602e4f2b59aea567c7073199d67888c
+DIST why3-1.5.1.tar.gz 6727576 BLAKE2B db88dc011856bc779a917613adb20c14744f5491aba54e424909106a1133362ddf9eb22e4a05660cb3153bfddfa54c488e1f9df046e3c413732924e127975e82 SHA512 1452a21ea9191f57debcc082afe458aec503d6aa24f8bc83f734041cdd302c4f166c9c4fe5f9ec25369b6e83011bdd7b485d67b092efa71ff0c1b39447f4bdac
diff --git a/sci-mathematics/why3/why3-1.5.1.ebuild b/sci-mathematics/why3/why3-1.5.1.ebuild
new file mode 100644
index 000000000000..46885e778d78
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.5.1.ebuild
@@ -0,0 +1,103 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit autotools findlib
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="https://why3.lri.fr/"
+SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0/${PV}"
+KEYWORDS="~amd64"
+IUSE="coq doc emacs gtk +ocamlopt re sexp stackify +zarith zip"
+
+RDEPEND="
+ !sci-mathematics/why3-for-spark
+ >=dev-lang/ocaml-4.05.0:=[ocamlopt?]
+ >=dev-ml/menhir-20170418:=
+ dev-ml/num:=
+ coq? ( >=sci-mathematics/coq-8.7 )
+ emacs? ( app-editors/emacs:* )
+ gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
+ re? ( dev-ml/re:= )
+ sexp? (
+ dev-ml/ppx_deriving:=[ocamlopt?]
+ dev-ml/ppx_sexp_conv:=[ocamlopt?]
+ dev-ml/sexplib:=[ocamlopt?]
+ )
+ stackify? ( dev-ml/ocamlgraph:=[ocamlopt?] )
+ zarith? ( dev-ml/zarith:= )
+ zip? ( dev-ml/camlzip:= )
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
+ doc? (
+ dev-python/sphinx
+ dev-python/sphinxcontrib-bibtex
+ media-gfx/graphviz
+ dev-texlive/texlive-latex
+ dev-texlive/texlive-fontsrecommended
+ dev-texlive/texlive-latexextra
+ )
+"
+
+DOCS=( CHANGES.md README.md )
+
+src_prepare() {
+ mv configure.in configure.ac || die
+ sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+ sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
+ -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+ -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
+ -i Makefile.in || die
+
+ # remove QA warning about duplicated compressed file:
+ rm examples/mlcfg/basic/why3shapes.gz || die
+
+ eautoreconf
+ default
+}
+
+src_configure() {
+ local myconf=(
+ --disable-hypothesis-selection
+ --disable-pvs-libs
+ --disable-isabelle-libs
+ --disable-frama-c
+ --disable-infer
+ --disable-web-ide
+ $(use_enable coq coq-libs)
+ $(use_enable doc)
+ $(use_enable emacs emacs-compilation)
+ $(use_enable gtk ide)
+ $(use_enable ocamlopt native-code)
+ $(use_enable re)
+ $(use_enable sexp pp-sexp)
+ $(use_enable stackify)
+ $(use_enable zarith)
+ $(use_enable zip)
+ )
+ econf "${myconf[@]}"
+}
+
+src_compile() {
+ emake
+ emake plugins
+ use doc && emake doc
+}
+
+src_install(){
+ findlib_src_preinst
+ emake install install-lib DESTDIR="${ED}"
+
+ einstalldocs
+ docompress -x /usr/share/doc/${PF}/examples
+ dodoc -r examples
+ if use doc; then
+ dodoc doc/latex/manual.pdf
+ dodoc -r doc/html
+ fi
+}
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2023-04-01 22:57 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2023-04-01 22:57 UTC (permalink / raw
To: gentoo-commits
commit: ee8a6c729b7e0d802129ac020fba8b7b212c49f0
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Apr 1 21:43:46 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Apr 1 22:35:47 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ee8a6c72
sci-mathematics/why3: bump to 1.6.0
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/Manifest | 1 +
sci-mathematics/why3/why3-1.6.0.ebuild | 106 +++++++++++++++++++++++++++++++++
2 files changed, 107 insertions(+)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index 4f6bc6bc9f21..636bb81746b6 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -2,3 +2,4 @@ DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a58
DIST why3-1.4.1.tar.gz 6305011 BLAKE2B 2d916fbf333550f8021bff9e7ccf4ca5685763ca7f82ae133298feaf96f3e8b36290a103fd27224fb6fb2dc36c8d7ad5d93ffc92e8cf7fe1a61abb5a40aecb39 SHA512 7990519179c088be1bc9b5b6d469f6d6fbd683445e20cbf5edd5c97682f2931b2657a92b60e539d7647033bfdc5a63401f28af61fd9b14b41011144afa2016e0
DIST why3-1.5.0.tar.gz 6723500 BLAKE2B e6ae5034cf0b3923dfaa760d604f754d4e385ea92ca1f70c7d4bd9985c75192ed381bb50d7211451f35d485e5c0969b3de4987603720b2fd6609cca5d074b85f SHA512 3ae443733321f2e487d6e503c4dbfe37d0e24c7dbe88eb94a3907775a1e6e30530b58ff835e3b2fff3fac5cd16622d758602e4f2b59aea567c7073199d67888c
DIST why3-1.5.1.tar.gz 6727576 BLAKE2B db88dc011856bc779a917613adb20c14744f5491aba54e424909106a1133362ddf9eb22e4a05660cb3153bfddfa54c488e1f9df046e3c413732924e127975e82 SHA512 1452a21ea9191f57debcc082afe458aec503d6aa24f8bc83f734041cdd302c4f166c9c4fe5f9ec25369b6e83011bdd7b485d67b092efa71ff0c1b39447f4bdac
+DIST why3-1.6.0.tar.gz 6850062 BLAKE2B 91db6f67a9d0fe24b7d7d18e6c5e9cd362563a55702bfb28c478754f53e831beb3033adde251214facd8d64ab923389b0b9fe7b240b6cd09f0b4b3e6f8eca143 SHA512 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1
diff --git a/sci-mathematics/why3/why3-1.6.0.ebuild b/sci-mathematics/why3/why3-1.6.0.ebuild
new file mode 100644
index 000000000000..1c3b6b458cc9
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.6.0.ebuild
@@ -0,0 +1,106 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit autotools findlib
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="https://why3.lri.fr/"
+SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0/${PV}"
+KEYWORDS="~amd64"
+IUSE="coq doc emacs gtk +ocamlopt re sexp stackify +zarith zip"
+
+RDEPEND="
+ !sci-mathematics/why3-for-spark
+ >=dev-lang/ocaml-4.05.0:=[ocamlopt?]
+ >=dev-ml/menhir-20170418:=
+ dev-ml/num:=
+ coq? ( >=sci-mathematics/coq-8.7:= )
+ emacs? ( app-editors/emacs:* )
+ gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
+ re? ( dev-ml/re:= )
+ sexp? (
+ dev-ml/ppx_deriving:=[ocamlopt?]
+ dev-ml/ppx_sexp_conv:=[ocamlopt?]
+ dev-ml/sexplib:=[ocamlopt?]
+ )
+ stackify? ( dev-ml/ocamlgraph:=[ocamlopt?] )
+ zarith? ( dev-ml/zarith:= )
+ zip? ( dev-ml/camlzip:= )
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
+ doc? (
+ dev-python/sphinx
+ dev-python/sphinxcontrib-bibtex
+ media-gfx/graphviz
+ dev-texlive/texlive-latex
+ dev-texlive/texlive-fontsrecommended
+ dev-texlive/texlive-latexextra
+ )
+"
+
+DOCS=( CHANGES.md README.md )
+
+src_prepare() {
+ mv configure.in configure.ac || die
+
+ sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+ sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
+ -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+ -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
+ -i Makefile.in || die
+
+ # remove QA warning about duplicated compressed file:
+ rm examples/mlcfg/basic/why3shapes.gz || die
+
+ eautoreconf
+ default
+}
+
+src_configure() {
+ local -a myconf=(
+ --disable-frama-c
+ --disable-hypothesis-selection
+ --disable-infer
+ --disable-isabelle-libs
+ --disable-pvs-libs
+ --disable-web-ide
+ $(use_enable coq coq-libs)
+ $(use_enable doc)
+ $(use_enable emacs emacs-compilation)
+ $(use_enable gtk ide)
+ $(use_enable ocamlopt native-code)
+ $(use_enable re)
+ $(use_enable sexp pp-sexp)
+ $(use_enable stackify)
+ $(use_enable zarith)
+ $(use_enable zip)
+ )
+ econf "${myconf[@]}"
+}
+
+src_compile() {
+ emake
+ emake plugins
+
+ use doc && emake doc
+}
+
+src_install(){
+ findlib_src_preinst
+ emake install install-lib DESTDIR="${ED}"
+
+ einstalldocs
+ docompress -x /usr/share/doc/${PF}/examples
+ dodoc -r examples
+
+ if use doc; then
+ dodoc doc/latex/manual.pdf
+ dodoc -r doc/html
+ fi
+}
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2023-04-01 22:57 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2023-04-01 22:57 UTC (permalink / raw
To: gentoo-commits
commit: c369073451a29ba37f806d8429a1e69cdc999745
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Apr 1 21:43:59 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Apr 1 22:35:47 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c3690734
sci-mathematics/why3: drop old 1.4.0-r3
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/Manifest | 1 -
sci-mathematics/why3/why3-1.4.0-r3.ebuild | 98 -------------------------------
2 files changed, 99 deletions(-)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index 636bb81746b6..3c2590f06042 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,4 +1,3 @@
-DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5 SHA512 b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
DIST why3-1.4.1.tar.gz 6305011 BLAKE2B 2d916fbf333550f8021bff9e7ccf4ca5685763ca7f82ae133298feaf96f3e8b36290a103fd27224fb6fb2dc36c8d7ad5d93ffc92e8cf7fe1a61abb5a40aecb39 SHA512 7990519179c088be1bc9b5b6d469f6d6fbd683445e20cbf5edd5c97682f2931b2657a92b60e539d7647033bfdc5a63401f28af61fd9b14b41011144afa2016e0
DIST why3-1.5.0.tar.gz 6723500 BLAKE2B e6ae5034cf0b3923dfaa760d604f754d4e385ea92ca1f70c7d4bd9985c75192ed381bb50d7211451f35d485e5c0969b3de4987603720b2fd6609cca5d074b85f SHA512 3ae443733321f2e487d6e503c4dbfe37d0e24c7dbe88eb94a3907775a1e6e30530b58ff835e3b2fff3fac5cd16622d758602e4f2b59aea567c7073199d67888c
DIST why3-1.5.1.tar.gz 6727576 BLAKE2B db88dc011856bc779a917613adb20c14744f5491aba54e424909106a1133362ddf9eb22e4a05660cb3153bfddfa54c488e1f9df046e3c413732924e127975e82 SHA512 1452a21ea9191f57debcc082afe458aec503d6aa24f8bc83f734041cdd302c4f166c9c4fe5f9ec25369b6e83011bdd7b485d67b092efa71ff0c1b39447f4bdac
diff --git a/sci-mathematics/why3/why3-1.4.0-r3.ebuild b/sci-mathematics/why3/why3-1.4.0-r3.ebuild
deleted file mode 100644
index 6d1e01d9863c..000000000000
--- a/sci-mathematics/why3/why3-1.4.0-r3.ebuild
+++ /dev/null
@@ -1,98 +0,0 @@
-# Copyright 1999-2022 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="https://why3.lri.fr/"
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
-
-RDEPEND="
- !sci-mathematics/why3-for-spark
- >=dev-lang/ocaml-4.05.0:=[ocamlopt?]
- >=dev-ml/menhir-20170418:=
- dev-ml/num:=
- coq? ( >=sci-mathematics/coq-8.6 )
- emacs? ( app-editors/emacs:* )
- gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
- re? ( dev-ml/re:= )
- 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-python/sphinx
- dev-python/sphinxcontrib-bibtex
- media-gfx/graphviz
- dev-texlive/texlive-latex
- dev-texlive/texlive-fontsrecommended
- dev-texlive/texlive-latexextra
- )
-"
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
- mv configure.in configure.ac || die
- sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
- sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
- -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
- -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
- -i Makefile.in || die
-
- eautoreconf
- default
-}
-
-src_configure() {
- local myconf=(
- --disable-hypothesis-selection
- --disable-pvs-libs
- --disable-isabelle-libs
- --disable-frama-c
- --disable-infer
- --disable-web-ide
- $(use_enable coq coq-libs)
- $(use_enable doc)
- $(use_enable emacs emacs-compilation)
- $(use_enable gtk ide)
- $(use_enable ocamlopt native-code)
- $(use_enable re)
- $(use_enable sexp pp-sexp)
- $(use_enable zarith)
- $(use_enable zip)
- )
- econf "${myconf[@]}"
-}
-
-src_compile() {
- emake
- emake plugins
- use doc && emake doc
-}
-
-src_install(){
- findlib_src_preinst
- emake install install-lib DESTDIR="${ED}"
-
- einstalldocs
- docompress -x /usr/share/doc/${PF}/examples
- dodoc -r examples
- if use doc; then
- dodoc doc/latex/manual.pdf
- dodoc -r doc/html
- fi
-}
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2023-04-01 22:57 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2023-04-01 22:57 UTC (permalink / raw
To: gentoo-commits
commit: 55c35b5dfb116b0619f48f6162afb4698b109891
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Apr 1 21:44:09 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Apr 1 22:35:48 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=55c35b5d
sci-mathematics/why3: drop old 1.5.0-r1
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/Manifest | 1 -
sci-mathematics/why3/why3-1.5.0-r1.ebuild | 103 ------------------------------
2 files changed, 104 deletions(-)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index 3c2590f06042..b4c557cc84db 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,4 +1,3 @@
DIST why3-1.4.1.tar.gz 6305011 BLAKE2B 2d916fbf333550f8021bff9e7ccf4ca5685763ca7f82ae133298feaf96f3e8b36290a103fd27224fb6fb2dc36c8d7ad5d93ffc92e8cf7fe1a61abb5a40aecb39 SHA512 7990519179c088be1bc9b5b6d469f6d6fbd683445e20cbf5edd5c97682f2931b2657a92b60e539d7647033bfdc5a63401f28af61fd9b14b41011144afa2016e0
-DIST why3-1.5.0.tar.gz 6723500 BLAKE2B e6ae5034cf0b3923dfaa760d604f754d4e385ea92ca1f70c7d4bd9985c75192ed381bb50d7211451f35d485e5c0969b3de4987603720b2fd6609cca5d074b85f SHA512 3ae443733321f2e487d6e503c4dbfe37d0e24c7dbe88eb94a3907775a1e6e30530b58ff835e3b2fff3fac5cd16622d758602e4f2b59aea567c7073199d67888c
DIST why3-1.5.1.tar.gz 6727576 BLAKE2B db88dc011856bc779a917613adb20c14744f5491aba54e424909106a1133362ddf9eb22e4a05660cb3153bfddfa54c488e1f9df046e3c413732924e127975e82 SHA512 1452a21ea9191f57debcc082afe458aec503d6aa24f8bc83f734041cdd302c4f166c9c4fe5f9ec25369b6e83011bdd7b485d67b092efa71ff0c1b39447f4bdac
DIST why3-1.6.0.tar.gz 6850062 BLAKE2B 91db6f67a9d0fe24b7d7d18e6c5e9cd362563a55702bfb28c478754f53e831beb3033adde251214facd8d64ab923389b0b9fe7b240b6cd09f0b4b3e6f8eca143 SHA512 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1
diff --git a/sci-mathematics/why3/why3-1.5.0-r1.ebuild b/sci-mathematics/why3/why3-1.5.0-r1.ebuild
deleted file mode 100644
index d592ff2803b1..000000000000
--- a/sci-mathematics/why3/why3-1.5.0-r1.ebuild
+++ /dev/null
@@ -1,103 +0,0 @@
-# Copyright 1999-2022 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="https://why3.lri.fr/"
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk +ocamlopt re sexp stackify +zarith zip"
-
-RDEPEND="
- !sci-mathematics/why3-for-spark
- >=dev-lang/ocaml-4.05.0:=[ocamlopt?]
- >=dev-ml/menhir-20170418:=
- dev-ml/num:=
- coq? ( >=sci-mathematics/coq-8.7 )
- emacs? ( app-editors/emacs:* )
- gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
- re? ( dev-ml/re:= )
- sexp? (
- dev-ml/ppx_deriving:=[ocamlopt?]
- dev-ml/ppx_sexp_conv:=[ocamlopt?]
- dev-ml/sexplib:=[ocamlopt?]
- )
- stackify? ( dev-ml/ocamlgraph:=[ocamlopt?] )
- zarith? ( dev-ml/zarith:= )
- zip? ( dev-ml/camlzip:= )
-"
-DEPEND="${RDEPEND}"
-BDEPEND="
- doc? (
- dev-python/sphinx
- dev-python/sphinxcontrib-bibtex
- media-gfx/graphviz
- dev-texlive/texlive-latex
- dev-texlive/texlive-fontsrecommended
- dev-texlive/texlive-latexextra
- )
-"
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
- mv configure.in configure.ac || die
- sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
- sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
- -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
- -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
- -i Makefile.in || die
-
- # remove QA warning about duplicated compressed file:
- rm examples/mlcfg/basic/why3shapes.gz || die
-
- eautoreconf
- default
-}
-
-src_configure() {
- local myconf=(
- --disable-hypothesis-selection
- --disable-pvs-libs
- --disable-isabelle-libs
- --disable-frama-c
- --disable-infer
- --disable-web-ide
- $(use_enable coq coq-libs)
- $(use_enable doc)
- $(use_enable emacs emacs-compilation)
- $(use_enable gtk ide)
- $(use_enable ocamlopt native-code)
- $(use_enable re)
- $(use_enable sexp pp-sexp)
- $(use_enable stackify)
- $(use_enable zarith)
- $(use_enable zip)
- )
- econf "${myconf[@]}"
-}
-
-src_compile() {
- emake
- emake plugins
- use doc && emake doc
-}
-
-src_install(){
- findlib_src_preinst
- emake install install-lib DESTDIR="${ED}"
-
- einstalldocs
- docompress -x /usr/share/doc/${PF}/examples
- dodoc -r examples
- if use doc; then
- dodoc doc/latex/manual.pdf
- dodoc -r doc/html
- fi
-}
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2023-07-15 22:17 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2023-07-15 22:17 UTC (permalink / raw
To: gentoo-commits
commit: 8172b96a31be44514df28bdd63c866ce615f9790
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Jul 15 21:52:19 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Jul 15 22:17:01 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=8172b96a
sci-mathematics/why3: drop old 1.4.1-r1
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/Manifest | 1 -
sci-mathematics/why3/why3-1.4.1-r1.ebuild | 98 -------------------------------
2 files changed, 99 deletions(-)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index b4c557cc84db..38a095398b28 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,3 +1,2 @@
-DIST why3-1.4.1.tar.gz 6305011 BLAKE2B 2d916fbf333550f8021bff9e7ccf4ca5685763ca7f82ae133298feaf96f3e8b36290a103fd27224fb6fb2dc36c8d7ad5d93ffc92e8cf7fe1a61abb5a40aecb39 SHA512 7990519179c088be1bc9b5b6d469f6d6fbd683445e20cbf5edd5c97682f2931b2657a92b60e539d7647033bfdc5a63401f28af61fd9b14b41011144afa2016e0
DIST why3-1.5.1.tar.gz 6727576 BLAKE2B db88dc011856bc779a917613adb20c14744f5491aba54e424909106a1133362ddf9eb22e4a05660cb3153bfddfa54c488e1f9df046e3c413732924e127975e82 SHA512 1452a21ea9191f57debcc082afe458aec503d6aa24f8bc83f734041cdd302c4f166c9c4fe5f9ec25369b6e83011bdd7b485d67b092efa71ff0c1b39447f4bdac
DIST why3-1.6.0.tar.gz 6850062 BLAKE2B 91db6f67a9d0fe24b7d7d18e6c5e9cd362563a55702bfb28c478754f53e831beb3033adde251214facd8d64ab923389b0b9fe7b240b6cd09f0b4b3e6f8eca143 SHA512 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1
diff --git a/sci-mathematics/why3/why3-1.4.1-r1.ebuild b/sci-mathematics/why3/why3-1.4.1-r1.ebuild
deleted file mode 100644
index 6d1e01d9863c..000000000000
--- a/sci-mathematics/why3/why3-1.4.1-r1.ebuild
+++ /dev/null
@@ -1,98 +0,0 @@
-# Copyright 1999-2022 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="https://why3.lri.fr/"
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
-
-RDEPEND="
- !sci-mathematics/why3-for-spark
- >=dev-lang/ocaml-4.05.0:=[ocamlopt?]
- >=dev-ml/menhir-20170418:=
- dev-ml/num:=
- coq? ( >=sci-mathematics/coq-8.6 )
- emacs? ( app-editors/emacs:* )
- gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
- re? ( dev-ml/re:= )
- 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-python/sphinx
- dev-python/sphinxcontrib-bibtex
- media-gfx/graphviz
- dev-texlive/texlive-latex
- dev-texlive/texlive-fontsrecommended
- dev-texlive/texlive-latexextra
- )
-"
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
- mv configure.in configure.ac || die
- sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
- sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
- -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
- -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
- -i Makefile.in || die
-
- eautoreconf
- default
-}
-
-src_configure() {
- local myconf=(
- --disable-hypothesis-selection
- --disable-pvs-libs
- --disable-isabelle-libs
- --disable-frama-c
- --disable-infer
- --disable-web-ide
- $(use_enable coq coq-libs)
- $(use_enable doc)
- $(use_enable emacs emacs-compilation)
- $(use_enable gtk ide)
- $(use_enable ocamlopt native-code)
- $(use_enable re)
- $(use_enable sexp pp-sexp)
- $(use_enable zarith)
- $(use_enable zip)
- )
- econf "${myconf[@]}"
-}
-
-src_compile() {
- emake
- emake plugins
- use doc && emake doc
-}
-
-src_install(){
- findlib_src_preinst
- emake install install-lib DESTDIR="${ED}"
-
- einstalldocs
- docompress -x /usr/share/doc/${PF}/examples
- dodoc -r examples
- if use doc; then
- dodoc doc/latex/manual.pdf
- dodoc -r doc/html
- fi
-}
^ permalink raw reply related [flat|nested] 16+ messages in thread
* [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/
@ 2023-07-15 22:17 Maciej Barć
0 siblings, 0 replies; 16+ messages in thread
From: Maciej Barć @ 2023-07-15 22:17 UTC (permalink / raw
To: gentoo-commits
commit: 0eb41919c406dc8282d78c71cceb73e7ea1e284d
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Jul 15 21:52:36 2023 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Jul 15 22:17:02 2023 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0eb41919
sci-mathematics/why3: drop old 1.5.1
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/why3/Manifest | 1 -
sci-mathematics/why3/why3-1.5.1.ebuild | 103 ---------------------------------
2 files changed, 104 deletions(-)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index 38a095398b28..b484111f886b 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,2 +1 @@
-DIST why3-1.5.1.tar.gz 6727576 BLAKE2B db88dc011856bc779a917613adb20c14744f5491aba54e424909106a1133362ddf9eb22e4a05660cb3153bfddfa54c488e1f9df046e3c413732924e127975e82 SHA512 1452a21ea9191f57debcc082afe458aec503d6aa24f8bc83f734041cdd302c4f166c9c4fe5f9ec25369b6e83011bdd7b485d67b092efa71ff0c1b39447f4bdac
DIST why3-1.6.0.tar.gz 6850062 BLAKE2B 91db6f67a9d0fe24b7d7d18e6c5e9cd362563a55702bfb28c478754f53e831beb3033adde251214facd8d64ab923389b0b9fe7b240b6cd09f0b4b3e6f8eca143 SHA512 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1
diff --git a/sci-mathematics/why3/why3-1.5.1.ebuild b/sci-mathematics/why3/why3-1.5.1.ebuild
deleted file mode 100644
index 46885e778d78..000000000000
--- a/sci-mathematics/why3/why3-1.5.1.ebuild
+++ /dev/null
@@ -1,103 +0,0 @@
-# Copyright 1999-2022 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="https://why3.lri.fr/"
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0/${PV}"
-KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk +ocamlopt re sexp stackify +zarith zip"
-
-RDEPEND="
- !sci-mathematics/why3-for-spark
- >=dev-lang/ocaml-4.05.0:=[ocamlopt?]
- >=dev-ml/menhir-20170418:=
- dev-ml/num:=
- coq? ( >=sci-mathematics/coq-8.7 )
- emacs? ( app-editors/emacs:* )
- gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
- re? ( dev-ml/re:= )
- sexp? (
- dev-ml/ppx_deriving:=[ocamlopt?]
- dev-ml/ppx_sexp_conv:=[ocamlopt?]
- dev-ml/sexplib:=[ocamlopt?]
- )
- stackify? ( dev-ml/ocamlgraph:=[ocamlopt?] )
- zarith? ( dev-ml/zarith:= )
- zip? ( dev-ml/camlzip:= )
-"
-DEPEND="${RDEPEND}"
-BDEPEND="
- doc? (
- dev-python/sphinx
- dev-python/sphinxcontrib-bibtex
- media-gfx/graphviz
- dev-texlive/texlive-latex
- dev-texlive/texlive-fontsrecommended
- dev-texlive/texlive-latexextra
- )
-"
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
- mv configure.in configure.ac || die
- sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
- sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
- -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
- -e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
- -i Makefile.in || die
-
- # remove QA warning about duplicated compressed file:
- rm examples/mlcfg/basic/why3shapes.gz || die
-
- eautoreconf
- default
-}
-
-src_configure() {
- local myconf=(
- --disable-hypothesis-selection
- --disable-pvs-libs
- --disable-isabelle-libs
- --disable-frama-c
- --disable-infer
- --disable-web-ide
- $(use_enable coq coq-libs)
- $(use_enable doc)
- $(use_enable emacs emacs-compilation)
- $(use_enable gtk ide)
- $(use_enable ocamlopt native-code)
- $(use_enable re)
- $(use_enable sexp pp-sexp)
- $(use_enable stackify)
- $(use_enable zarith)
- $(use_enable zip)
- )
- econf "${myconf[@]}"
-}
-
-src_compile() {
- emake
- emake plugins
- use doc && emake doc
-}
-
-src_install(){
- findlib_src_preinst
- emake install install-lib DESTDIR="${ED}"
-
- einstalldocs
- docompress -x /usr/share/doc/${PF}/examples
- dodoc -r examples
- if use doc; then
- dodoc doc/latex/manual.pdf
- dodoc -r doc/html
- fi
-}
^ permalink raw reply related [flat|nested] 16+ messages in thread
end of thread, other threads:[~2023-07-15 22:17 UTC | newest]
Thread overview: 16+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2023-07-15 22:17 [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/why3/ Maciej Barć
-- strict thread matches above, loose matches on Subject: below --
2023-07-15 22:17 Maciej Barć
2023-04-01 22:57 Maciej Barć
2023-04-01 22:57 Maciej Barć
2023-04-01 22:57 Maciej Barć
2022-09-19 18:59 Maciej Barć
2022-07-26 19:54 Alfredo Tupone
2022-07-23 0:06 Maciej Barć
2022-05-07 16:50 Maciej Barć
2022-04-16 21:25 Maciej Barć
2022-03-04 11:06 Maciej Barć
2022-01-17 21:23 Maciej Barć
2022-01-15 6:08 Maciej Barć
2022-01-13 16:41 Maciej Barć
2021-12-12 12:14 Maciej Barć
2021-12-12 1:59 Maciej Barć
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox