* [gentoo-commits] repo/proj/guru:master commit in: sci-mathematics/why3/
@ 2021-01-10 11:31 Andrew Ammerlaan
0 siblings, 0 replies; 6+ messages in thread
From: Andrew Ammerlaan @ 2021-01-10 11:31 UTC (permalink / raw
To: gentoo-commits
commit: 8774c3bacb82b878b97365d5c3c9764c1d38ae8a
Author: François-Xavier Carton <fx.carton91 <AT> gmail <DOT> com>
AuthorDate: Fri Nov 27 18:16:28 2020 +0000
Commit: Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
CommitDate: Sat Jan 9 16:44:42 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=8774c3ba
sci-mathematics/why3: new package
This is a bump from the version in ::science.
Signed-off-by: François-Xavier Carton <fx.carton91 <AT> gmail.com>
sci-mathematics/why3/Manifest | 1 +
sci-mathematics/why3/metadata.xml | 27 ++++++++++++
sci-mathematics/why3/why3-1.3.3.ebuild | 80 ++++++++++++++++++++++++++++++++++
3 files changed, 108 insertions(+)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
new file mode 100644
index 00000000..20a390e4
--- /dev/null
+++ b/sci-mathematics/why3/Manifest
@@ -0,0 +1 @@
+DIST why3-1.3.3.tar.gz 5807572 BLAKE2B b1a04e78010f841e217b9a81c096cadfa0cddabadbe81ef55c310a104668feb1e46cd50576a965a58c74658903d6d08f9fd348bd2064a79ac3b176548927bcbe SHA512 a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce
diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
new file mode 100644
index 00000000..444f26b5
--- /dev/null
+++ b/sci-mathematics/why3/metadata.xml
@@ -0,0 +1,27 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
+<pkgmetadata>
+ <maintainer type="person">
+ <name>François-Xavier Carton</name>
+ <email>fx.carton91@gmail.com</email>
+ </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="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.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild
new file mode 100644
index 00000000..b5665dc3
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -0,0 +1,80 @@
+# Copyright 1999-2020 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+inherit autotools
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/"
+SRC_URI="https://gforge.inria.fr/frs/download.php/file/38367/${P}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64"
+IUSE="coq emacs gtk +ocamlopt re +zarith zip"
+
+DEPEND=">=dev-lang/ocaml-4.05.0[ocamlopt?]
+ >=dev-ml/menhir-20151112
+ dev-ml/findlib
+ dev-ml/num
+ coq? ( >=sci-mathematics/coq-8.6 )
+ emacs? ( app-editors/emacs:* )
+ gtk? ( dev-ml/lablgtk:*[sourceview,ocamlopt?] )
+ re? ( dev-ml/re dev-ml/seq )
+ zarith? ( dev-ml/zarith )
+ zip? ( dev-ml/camlzip )"
+RDEPEND="${DEPEND}"
+
+# doc needs sphinxcontrib-bibtex which is currently not packaged
+# doc? (
+# dev-python/sphinx
+# dev-python/sphinxcontrib-bibtex
+# || ( dev-texlive/texlive-latex dev-tex/latexmk dev-tex/rubber )
+# )
+
+DOCS=( CHANGES.md README.md )
+
+src_prepare() {
+ mv doc/why.1 doc/why3.1 || die
+ mv configure.in configure.ac || die
+ sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+ eautoreconf
+ eapply_user
+}
+
+src_configure() {
+ econf \
+ --disable-hypothesis-selection \
+ --disable-pvs-libs \
+ --disable-isabelle-libs \
+ --disable-frama-c \
+ --disable-web-ide \
+ --disable-doc \
+ $(use_enable coq coq-libs) \
+ $(use_enable emacs emacs-compilation) \
+ $(use_enable gtk ide) \
+ $(use_enable ocamlopt native-code) \
+ $(use_enable re) \
+ $(use_enable zarith) \
+ $(use_enable zip)
+}
+
+src_compile() {
+ emake
+ emake plugins
+ #use doc && emake doc
+}
+
+src_install(){
+ emake install install-lib DESTDIR="${ED}"
+
+ doman doc/why3.1
+ einstalldocs
+ docompress -x /usr/share/doc/${PF}/examples
+ dodoc -r examples
+ #if use doc; then
+ # dodoc doc/latex/manual.pdf
+ # dodoc -r doc/html
+ #fi
+}
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [gentoo-commits] repo/proj/guru:master commit in: sci-mathematics/why3/
@ 2021-03-31 10:23 Andrew Ammerlaan
0 siblings, 0 replies; 6+ messages in thread
From: Andrew Ammerlaan @ 2021-03-31 10:23 UTC (permalink / raw
To: gentoo-commits
commit: 42c0da6a668a33653427f8b8ff93073a189819c7
Author: François-Xavier Carton <fx.carton91 <AT> gmail <DOT> com>
AuthorDate: Tue Mar 30 19:32:21 2021 +0000
Commit: Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
CommitDate: Tue Mar 30 19:32:21 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=42c0da6a
sci-mathematics/why3: bump to 1.4.0
Signed-off-by: François-Xavier Carton <fx.carton91 <AT> gmail.com>
sci-mathematics/why3/Manifest | 1 +
sci-mathematics/why3/metadata.xml | 1 +
sci-mathematics/why3/why3-1.4.0.ebuild | 83 ++++++++++++++++++++++++++++++++++
3 files changed, 85 insertions(+)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index 20a390e40..9987a255a 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1 +1,2 @@
DIST why3-1.3.3.tar.gz 5807572 BLAKE2B b1a04e78010f841e217b9a81c096cadfa0cddabadbe81ef55c310a104668feb1e46cd50576a965a58c74658903d6d08f9fd348bd2064a79ac3b176548927bcbe SHA512 a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce
+DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5 SHA512 b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
index 444f26b5b..008bf6030 100644
--- a/sci-mathematics/why3/metadata.xml
+++ b/sci-mathematics/why3/metadata.xml
@@ -21,6 +21,7 @@ language for the verification of C, Java, or Ada programs.
<flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag>
<flag name="gtk">Build the IDE <pkg>x11-libs/gtk+</pkg></flag>
<flag name="re">Use Re (<pkg>dev-ml/re</pkg>) instead of Str for regular expressions</flag>
+ <flag name="sexp">Add support for outputting S-expressions with <pkg>dev-ml/ppx_sexp_conv</pkg></flag>
<flag name="zarith">Use Zarith (<pkg>dev-ml/zarith</pkg>) instead of Nums (<pkg>dev-ml/num</pkg>) for computations</flag>
<flag name="zip">Enable compression of session files</flag>
</use>
diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild b/sci-mathematics/why3/why3-1.4.0.ebuild
new file mode 100644
index 000000000..d85c95cfc
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.4.0.ebuild
@@ -0,0 +1,83 @@
+# Copyright 1999-2020 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+inherit autotools
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/"
+SRC_URI="https://gforge.inria.fr/frs/download.php/file/38425/${P}.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64"
+IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
+
+DEPEND=">=dev-lang/ocaml-4.05.0[ocamlopt?]
+ >=dev-ml/menhir-20151112
+ dev-ml/findlib
+ dev-ml/num
+ coq? ( >=sci-mathematics/coq-8.6 )
+ doc? (
+ dev-python/sphinx
+ dev-python/sphinxcontrib-bibtex
+ || ( dev-texlive/texlive-latex dev-tex/latexmk dev-tex/rubber )
+ )
+ emacs? ( app-editors/emacs:* )
+ gtk? ( dev-ml/lablgtk:*[sourceview,ocamlopt?] )
+ re? ( dev-ml/re dev-ml/seq )
+ sexp? (
+ dev-ml/ppx_deriving[ocamlopt?]
+ dev-ml/ppx_sexp_conv[ocamlopt?]
+ dev-ml/sexplib[ocamlopt?]
+ )
+ zarith? ( dev-ml/zarith )
+ zip? ( dev-ml/camlzip )"
+RDEPEND="${DEPEND}"
+
+DOCS=( CHANGES.md README.md )
+
+src_prepare() {
+ mv configure.in configure.ac || die
+ sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+ eautoreconf
+ eapply_user
+}
+
+src_configure() {
+ econf \
+ --disable-hypothesis-selection \
+ --disable-pvs-libs \
+ --disable-isabelle-libs \
+ --disable-frama-c \
+ --disable-infer \
+ --disable-web-ide \
+ $(use_enable coq coq-libs) \
+ $(use_enable doc) \
+ $(use_enable emacs emacs-compilation) \
+ $(use_enable gtk ide) \
+ $(use_enable ocamlopt native-code) \
+ $(use_enable re) \
+ $(use_enable sexp pp-sexp) \
+ $(use_enable zarith) \
+ $(use_enable zip)
+}
+
+src_compile() {
+ emake
+ emake plugins
+ use doc && emake doc
+}
+
+src_install(){
+ emake install install-lib DESTDIR="${ED}"
+
+ einstalldocs
+ docompress -x /usr/share/doc/${PF}/examples
+ dodoc -r examples
+ if use doc; then
+ dodoc doc/latex/manual.pdf
+ dodoc -r doc/html
+ fi
+}
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [gentoo-commits] repo/proj/guru:master commit in: sci-mathematics/why3/
@ 2021-04-19 8:04 Andrew Ammerlaan
0 siblings, 0 replies; 6+ messages in thread
From: Andrew Ammerlaan @ 2021-04-19 8:04 UTC (permalink / raw
To: gentoo-commits
commit: 556d223d1e4531cb91e44a21bba602ac92f2a25d
Author: François-Xavier Carton <fx.carton91 <AT> gmail <DOT> com>
AuthorDate: Mon Apr 19 01:03:43 2021 +0000
Commit: Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
CommitDate: Mon Apr 19 01:15:31 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=556d223d
sci-mathematics/why3: respect CFLAGS & LDFLAGS
Closes: https://bugs.gentoo.org/781650
Signed-off-by: François-Xavier Carton <fx.carton91 <AT> gmail.com>
sci-mathematics/why3/why3-1.3.3.ebuild | 3 +++
sci-mathematics/why3/why3-1.4.0.ebuild | 3 +++
2 files changed, 6 insertions(+)
diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild
index b5665dc3a..b710f8a1a 100644
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -39,6 +39,9 @@ src_prepare() {
mv doc/why.1 doc/why3.1 || die
mv configure.in configure.ac || die
sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+ sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
+ -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+ -i Makefile.in || die
eautoreconf
eapply_user
}
diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild b/sci-mathematics/why3/why3-1.4.0.ebuild
index d85c95cfc..7a1ab9ca4 100644
--- a/sci-mathematics/why3/why3-1.4.0.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0.ebuild
@@ -41,6 +41,9 @@ DOCS=( CHANGES.md README.md )
src_prepare() {
mv configure.in configure.ac || die
sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
+ sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
+ -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
+ -i Makefile.in || die
eautoreconf
eapply_user
}
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [gentoo-commits] repo/proj/guru:master commit in: sci-mathematics/why3/
@ 2021-10-01 21:04 Haelwenn Monnier
0 siblings, 0 replies; 6+ messages in thread
From: Haelwenn Monnier @ 2021-10-01 21:04 UTC (permalink / raw
To: gentoo-commits
commit: 4962103953030be5b8f12c33f6ff110952fb6e06
Author: François-Xavier Carton <fx.carton91 <AT> gmail <DOT> com>
AuthorDate: Fri Oct 1 13:07:43 2021 +0000
Commit: Haelwenn Monnier <contact <AT> hacktivis <DOT> me>
CommitDate: Fri Oct 1 13:07:43 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=49621039
sci-mathematics/why3: update SRC_URI
Signed-off-by: François-Xavier Carton <fx.carton91 <AT> gmail.com>
sci-mathematics/why3/why3-1.3.3.ebuild | 2 +-
sci-mathematics/why3/why3-1.4.0.ebuild | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild
index 75f796891..89ff253ff 100644
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -7,7 +7,7 @@ inherit autotools findlib
DESCRIPTION="Platform for deductive program verification"
HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https://gforge.inria.fr/frs/download.php/file/38367/${P}.tar.gz"
+SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
LICENSE="LGPL-2"
SLOT="0"
diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild b/sci-mathematics/why3/why3-1.4.0.ebuild
index 9174013f3..cce31164b 100644
--- a/sci-mathematics/why3/why3-1.4.0.ebuild
+++ b/sci-mathematics/why3/why3-1.4.0.ebuild
@@ -7,7 +7,7 @@ inherit autotools findlib
DESCRIPTION="Platform for deductive program verification"
HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https://gforge.inria.fr/frs/download.php/file/38425/${P}.tar.gz"
+SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
LICENSE="LGPL-2"
SLOT="0"
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/why3/
@ 2021-12-15 10:35 Andrew Ammerlaan
2021-12-15 10:35 ` [gentoo-commits] repo/proj/guru:master " Andrew Ammerlaan
0 siblings, 1 reply; 6+ messages in thread
From: Andrew Ammerlaan @ 2021-12-15 10:35 UTC (permalink / raw
To: gentoo-commits
commit: d6f443bcf23ca2f4f6e583bd02a79fadcb1c1875
Author: Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
AuthorDate: Wed Dec 15 10:32:13 2021 +0000
Commit: Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
CommitDate: Wed Dec 15 10:35:02 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=d6f443bc
sci-mathematics/why3: moved to ::gentoo
Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> gentoo.org>
sci-mathematics/why3/Manifest | 2 -
sci-mathematics/why3/metadata.xml | 28 -----------
sci-mathematics/why3/why3-1.3.3.ebuild | 83 --------------------------------
sci-mathematics/why3/why3-1.4.0.ebuild | 86 ----------------------------------
4 files changed, 199 deletions(-)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
deleted file mode 100644
index 9987a255a..000000000
--- a/sci-mathematics/why3/Manifest
+++ /dev/null
@@ -1,2 +0,0 @@
-DIST why3-1.3.3.tar.gz 5807572 BLAKE2B b1a04e78010f841e217b9a81c096cadfa0cddabadbe81ef55c310a104668feb1e46cd50576a965a58c74658903d6d08f9fd348bd2064a79ac3b176548927bcbe SHA512 a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce
-DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5 SHA512 b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
deleted file mode 100644
index d64bca822..000000000
--- a/sci-mathematics/why3/metadata.xml
+++ /dev/null
@@ -1,28 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
-<pkgmetadata>
- <maintainer type="person">
- <name>François-Xavier Carton</name>
- <email>fx.carton91@gmail.com</email>
- </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="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.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild
deleted file mode 100644
index 89ff253ff..000000000
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ /dev/null
@@ -1,83 +0,0 @@
-# Copyright 1999-2020 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0"
-KEYWORDS="~amd64"
-IUSE="coq emacs gtk +ocamlopt re +zarith zip"
-
-DEPEND=">=dev-lang/ocaml-4.05.0[ocamlopt?]
- >=dev-ml/menhir-20151112
- dev-ml/num
- coq? ( >=sci-mathematics/coq-8.6 )
- emacs? ( app-editors/emacs:* )
- gtk? ( dev-ml/lablgtk:*[sourceview,ocamlopt?] )
- re? ( dev-ml/re dev-ml/seq )
- zarith? ( dev-ml/zarith )
- zip? ( dev-ml/camlzip )"
-RDEPEND="${DEPEND}"
-
-# doc needs sphinxcontrib-bibtex which is currently not packaged
-# doc? (
-# dev-python/sphinx
-# dev-python/sphinxcontrib-bibtex
-# || ( dev-texlive/texlive-latex dev-tex/latexmk dev-tex/rubber )
-# )
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
- mv doc/why.1 doc/why3.1 || die
- mv configure.in configure.ac || die
- sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
- sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
- -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
- -i Makefile.in || die
- eautoreconf
- eapply_user
-}
-
-src_configure() {
- econf \
- --disable-hypothesis-selection \
- --disable-pvs-libs \
- --disable-isabelle-libs \
- --disable-frama-c \
- --disable-web-ide \
- --disable-doc \
- $(use_enable coq coq-libs) \
- $(use_enable emacs emacs-compilation) \
- $(use_enable gtk ide) \
- $(use_enable ocamlopt native-code) \
- $(use_enable re) \
- $(use_enable zarith) \
- $(use_enable zip)
-}
-
-src_compile() {
- emake
- emake plugins
- #use doc && emake doc
-}
-
-src_install(){
- findlib_src_preinst
- emake install install-lib DESTDIR="${ED}"
-
- doman doc/why3.1
- 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
-}
diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild b/sci-mathematics/why3/why3-1.4.0.ebuild
deleted file mode 100644
index cce31164b..000000000
--- a/sci-mathematics/why3/why3-1.4.0.ebuild
+++ /dev/null
@@ -1,86 +0,0 @@
-# Copyright 1999-2020 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0"
-KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
-
-DEPEND=">=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 )"
-RDEPEND="${DEPEND}"
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
- mv configure.in configure.ac || die
- sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
- sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
- -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
- -i Makefile.in || die
- eautoreconf
- eapply_user
-}
-
-src_configure() {
- econf \
- --disable-hypothesis-selection \
- --disable-pvs-libs \
- --disable-isabelle-libs \
- --disable-frama-c \
- --disable-infer \
- --disable-web-ide \
- $(use_enable coq coq-libs) \
- $(use_enable doc) \
- $(use_enable emacs emacs-compilation) \
- $(use_enable gtk ide) \
- $(use_enable ocamlopt native-code) \
- $(use_enable re) \
- $(use_enable sexp pp-sexp) \
- $(use_enable zarith) \
- $(use_enable zip)
-}
-
-src_compile() {
- emake
- emake plugins
- use doc && emake doc
-}
-
-src_install(){
- 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] 6+ messages in thread
* [gentoo-commits] repo/proj/guru:master commit in: sci-mathematics/why3/
2021-12-15 10:35 [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/why3/ Andrew Ammerlaan
@ 2021-12-15 10:35 ` Andrew Ammerlaan
0 siblings, 0 replies; 6+ messages in thread
From: Andrew Ammerlaan @ 2021-12-15 10:35 UTC (permalink / raw
To: gentoo-commits
commit: d6f443bcf23ca2f4f6e583bd02a79fadcb1c1875
Author: Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
AuthorDate: Wed Dec 15 10:32:13 2021 +0000
Commit: Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
CommitDate: Wed Dec 15 10:35:02 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=d6f443bc
sci-mathematics/why3: moved to ::gentoo
Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> gentoo.org>
sci-mathematics/why3/Manifest | 2 -
sci-mathematics/why3/metadata.xml | 28 -----------
sci-mathematics/why3/why3-1.3.3.ebuild | 83 --------------------------------
sci-mathematics/why3/why3-1.4.0.ebuild | 86 ----------------------------------
4 files changed, 199 deletions(-)
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
deleted file mode 100644
index 9987a255a..000000000
--- a/sci-mathematics/why3/Manifest
+++ /dev/null
@@ -1,2 +0,0 @@
-DIST why3-1.3.3.tar.gz 5807572 BLAKE2B b1a04e78010f841e217b9a81c096cadfa0cddabadbe81ef55c310a104668feb1e46cd50576a965a58c74658903d6d08f9fd348bd2064a79ac3b176548927bcbe SHA512 a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce
-DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5 SHA512 b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a
diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
deleted file mode 100644
index d64bca822..000000000
--- a/sci-mathematics/why3/metadata.xml
+++ /dev/null
@@ -1,28 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
-<pkgmetadata>
- <maintainer type="person">
- <name>François-Xavier Carton</name>
- <email>fx.carton91@gmail.com</email>
- </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="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.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild
deleted file mode 100644
index 89ff253ff..000000000
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ /dev/null
@@ -1,83 +0,0 @@
-# Copyright 1999-2020 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0"
-KEYWORDS="~amd64"
-IUSE="coq emacs gtk +ocamlopt re +zarith zip"
-
-DEPEND=">=dev-lang/ocaml-4.05.0[ocamlopt?]
- >=dev-ml/menhir-20151112
- dev-ml/num
- coq? ( >=sci-mathematics/coq-8.6 )
- emacs? ( app-editors/emacs:* )
- gtk? ( dev-ml/lablgtk:*[sourceview,ocamlopt?] )
- re? ( dev-ml/re dev-ml/seq )
- zarith? ( dev-ml/zarith )
- zip? ( dev-ml/camlzip )"
-RDEPEND="${DEPEND}"
-
-# doc needs sphinxcontrib-bibtex which is currently not packaged
-# doc? (
-# dev-python/sphinx
-# dev-python/sphinxcontrib-bibtex
-# || ( dev-texlive/texlive-latex dev-tex/latexmk dev-tex/rubber )
-# )
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
- mv doc/why.1 doc/why3.1 || die
- mv configure.in configure.ac || die
- sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
- sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
- -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
- -i Makefile.in || die
- eautoreconf
- eapply_user
-}
-
-src_configure() {
- econf \
- --disable-hypothesis-selection \
- --disable-pvs-libs \
- --disable-isabelle-libs \
- --disable-frama-c \
- --disable-web-ide \
- --disable-doc \
- $(use_enable coq coq-libs) \
- $(use_enable emacs emacs-compilation) \
- $(use_enable gtk ide) \
- $(use_enable ocamlopt native-code) \
- $(use_enable re) \
- $(use_enable zarith) \
- $(use_enable zip)
-}
-
-src_compile() {
- emake
- emake plugins
- #use doc && emake doc
-}
-
-src_install(){
- findlib_src_preinst
- emake install install-lib DESTDIR="${ED}"
-
- doman doc/why3.1
- 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
-}
diff --git a/sci-mathematics/why3/why3-1.4.0.ebuild b/sci-mathematics/why3/why3-1.4.0.ebuild
deleted file mode 100644
index cce31164b..000000000
--- a/sci-mathematics/why3/why3-1.4.0.ebuild
+++ /dev/null
@@ -1,86 +0,0 @@
-# Copyright 1999-2020 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-inherit autotools findlib
-
-DESCRIPTION="Platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https://why3.gitlabpages.inria.fr/releases/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0"
-KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk +ocamlopt re sexp +zarith zip"
-
-DEPEND=">=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 )"
-RDEPEND="${DEPEND}"
-
-DOCS=( CHANGES.md README.md )
-
-src_prepare() {
- mv configure.in configure.ac || die
- sed -i 's/configure\.in/configure.ac/g' Makefile.in || die
- sed -e '/^lib\/why3[a-z]*\$(EXE):/{n;s/-Wall/$(CFLAGS) $(LDFLAGS)/}' \
- -e '/^%.o: %.c/{n;s/\$(CC).*-o/$(CC) $(CFLAGS) -o/}' \
- -i Makefile.in || die
- eautoreconf
- eapply_user
-}
-
-src_configure() {
- econf \
- --disable-hypothesis-selection \
- --disable-pvs-libs \
- --disable-isabelle-libs \
- --disable-frama-c \
- --disable-infer \
- --disable-web-ide \
- $(use_enable coq coq-libs) \
- $(use_enable doc) \
- $(use_enable emacs emacs-compilation) \
- $(use_enable gtk ide) \
- $(use_enable ocamlopt native-code) \
- $(use_enable re) \
- $(use_enable sexp pp-sexp) \
- $(use_enable zarith) \
- $(use_enable zip)
-}
-
-src_compile() {
- emake
- emake plugins
- use doc && emake doc
-}
-
-src_install(){
- 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] 6+ messages in thread
end of thread, other threads:[~2021-12-15 10:35 UTC | newest]
Thread overview: 6+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2021-12-15 10:35 [gentoo-commits] repo/proj/guru:dev commit in: sci-mathematics/why3/ Andrew Ammerlaan
2021-12-15 10:35 ` [gentoo-commits] repo/proj/guru:master " Andrew Ammerlaan
-- strict thread matches above, loose matches on Subject: below --
2021-10-01 21:04 Haelwenn Monnier
2021-04-19 8:04 Andrew Ammerlaan
2021-03-31 10:23 Andrew Ammerlaan
2021-01-10 11:31 Andrew Ammerlaan
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox