From 93a93e9a3b53c1a73142a305ea1f8136846942ee Mon Sep 17 00:00:00 2001 From: V3n3RiX Date: Wed, 22 Dec 2021 14:08:05 +0000 Subject: gentoo resync : 22.12.2021 --- sci-mathematics/why3/Manifest | 3 + sci-mathematics/why3/metadata.xml | 33 +++++++++++ sci-mathematics/why3/why3-1.4.0-r1.ebuild | 95 +++++++++++++++++++++++++++++++ 3 files changed, 131 insertions(+) create mode 100644 sci-mathematics/why3/Manifest create mode 100644 sci-mathematics/why3/metadata.xml create mode 100644 sci-mathematics/why3/why3-1.4.0-r1.ebuild (limited to 'sci-mathematics/why3') diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest new file mode 100644 index 000000000000..56bc0cb38a09 --- /dev/null +++ b/sci-mathematics/why3/Manifest @@ -0,0 +1,3 @@ +DIST why3-1.4.0.tar.gz 6306524 BLAKE2B ade7803a608d090ea06d974ae47e920993de92a5849d60bd63dba68252919a8f4fd1f0f6a3c975fdb727c4ae3afe13921b5d31a14c005e0d08f518e64bcf05e5 SHA512 b492f08a3c7073782b143a4849c47766b12045ad53c56aa8d251fd5b6bc1863ddebe260c99b3ddb27c4e1e1e9ab986c8b02286ec24f4c30f99f81f5f13fdc90a +EBUILD why3-1.4.0-r1.ebuild 2089 BLAKE2B 5d3ccd3ab09f320640dc30b20d4dd0e4caad312bcbad1685507839f5803221ae8ac5da9e184aece2f77afa439e4e8cae5541f1ba02f71b0713ea9989f4758581 SHA512 6dc7c9572d02fccfec6445268f1f880f540c9cc53d618328865baf958dd6cc310904fe991341f2e7156c961ae38e6c73a3572a73cebb55937fa2055384a6a62a +MISC metadata.xml 1680 BLAKE2B 4443de2368a7003db59e341bc671c8aa4c664be935b65df1fd1af161900a977194e012ef3b486f877a77f6b32405d700ee814d7cdeb10703b2462f7337965fb5 SHA512 7cc8dbe476d891d1311cec6ea15b1c6e6391c32bdbe715fe1fb7d2549763384c148e0509fb2b7c68b98b70eec1feeb4d94271378a343d50ef58cb5bb8a07a109 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 @@ + + + + + + François-Xavier Carton + fx.carton91@gmail.com + + + ml@gentoo.org + ML + + + 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. + + + Add sci-mathematics/coq support + Build the IDE x11-libs/gtk+ + Use Re (dev-ml/re) instead of Str for regular expressions + Add support for outputting S-expressions with dev-ml/ppx_sexp_conv + Use Zarith (dev-ml/zarith) instead of Nums (dev-ml/num) for computations + Enable compression of session files + + diff --git a/sci-mathematics/why3/why3-1.4.0-r1.ebuild b/sci-mathematics/why3/why3-1.4.0-r1.ebuild new file mode 100644 index 000000000000..badf49628e94 --- /dev/null +++ b/sci-mathematics/why3/why3-1.4.0-r1.ebuild @@ -0,0 +1,95 @@ +# 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 ) + 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 ) + ) +" + +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 +} -- cgit v1.2.3