mirror of
https://github.com/gentoo-mirror/guru.git
synced 2026-07-22 21:43:03 -04:00
sci-mathematics/why3: moved to ::gentoo
Signed-off-by: Andrew Ammerlaan <andrewammerlaan@gentoo.org>
This commit is contained in:
Andrew Ammerlaan
@@ -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
|
|
||||||
@@ -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>
|
|
||||||
@@ -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
|
|
||||||
}
|
|
||||||
@@ -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
|
|
||||||
}
|
|
||||||
Reference in New Issue
Block a user