diff options
Diffstat (limited to 'sci-mathematics/why3')
| -rw-r--r-- | sci-mathematics/why3/ChangeLog | 7 | ||||
| -rw-r--r-- | sci-mathematics/why3/Manifest | 4 | ||||
| -rw-r--r-- | sci-mathematics/why3/metadata.xml | 23 | ||||
| -rw-r--r-- | sci-mathematics/why3/why3-0.83.ebuild | 55 |
4 files changed, 89 insertions, 0 deletions
diff --git a/sci-mathematics/why3/ChangeLog b/sci-mathematics/why3/ChangeLog new file mode 100644 index 000000000..a91bee85b --- /dev/null +++ b/sci-mathematics/why3/ChangeLog @@ -0,0 +1,7 @@ +# ChangeLog for sci-mathematics/why3 +# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2 +# $Header: $ + + 21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com> + +ChangeLog, +metadata.xml, +why3-0.83.ebuild: + initial version diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest new file mode 100644 index 000000000..ec2faf65e --- /dev/null +++ b/sci-mathematics/why3/Manifest @@ -0,0 +1,4 @@ +DIST why3-0.83.tar.gz 5347628 SHA256 cabf67e939e3422e491ef596f1a09ceaf1615642904182097cebde90e42e9ac9 SHA512 e1c4d462986835aa0e9a1ca117e4c3bbaf307b45b6de03da6ea8dd706770b8d9894031ea22ec732dfa7340d613b023ab499837203a132db5f138e51596e64177 WHIRLPOOL 4e1a6fb8462144ec5726f461a6548b5fdaeb2338557ec84cefa7a6eed5594c35908e7ccc337a93aaa704283f88874f5cb3ca1f9dbe2355266af163f27e81cf7e +EBUILD why3-0.83.ebuild 1325 SHA256 c13afa35013186d12ffa7127e51815f20e3d52675d09d94b80df2f681ee84695 SHA512 1b73870850779d619e6103a7d7febe7a7fa2aee83e57da855460591590759d3fa00cdf4f85ff76a60e3dc36ddf764ec26abca983738a651e51c8dd7a32709a85 WHIRLPOOL ae8dbf7afaefb87470a4e5f6c2a30aec79fcb0236ace2d7e6609feb50a65ea794dbcfd163bbe7810edc6637d201b8a22f019248c4ee5e1866480f6ffb754deed +MISC ChangeLog 248 SHA256 75e04e1c01a3bab95d3aea02729451bc72450b4a357e3cd7da5e250766dc4181 SHA512 59d5309b1fbc0e829ebe13318c221964cb97e6083ddb5c87acbcbe720882305911cd1f8187aa389b1394892edc0718370c4326cf889ed3144eb89e6d31259f24 WHIRLPOOL 743c17f5170e887142722dc269b465563ad496629dd35985870dfe25d94b41ecc18557d0a56ac55076b4c546c80e2fef3def54c9ce6f06fecda09bd03d37c89f +MISC metadata.xml 1003 SHA256 5bb7fa100e8393607e63b9bdd5974184c86f51759da8f66e45a36fb4beca4aba SHA512 6ac8f7a9ffe33f930fd9522d28fb321bacb914fece132778e2184d552e4279ee583cbaf73a01437fd64ab3ea1fc3c7c94959fe36125e95e07c2a1bbf9c60a567 WHIRLPOOL 58fcab163ae5ebf598512f5ba2ab655ee4d0dd9d352882c38e8adf5beaada7e3dac4dab98412f79d305773f9290c214e06cc686cf596d2ab1e459ff4ac22998b diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml new file mode 100644 index 000000000..361520dd3 --- /dev/null +++ b/sci-mathematics/why3/metadata.xml @@ -0,0 +1,23 @@ +<?xml version="1.0" encoding="UTF-8"?> +<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> +<pkgmetadata> + <herd>sci</herd> + <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> + <maintainer> + <email>sci@gentoo.org</email> + </maintainer> + <use> + <flag name="frama-c">?frama-c?</flag> + </use> +</pkgmetadata> diff --git a/sci-mathematics/why3/why3-0.83.ebuild b/sci-mathematics/why3/why3-0.83.ebuild new file mode 100644 index 000000000..55bc65684 --- /dev/null +++ b/sci-mathematics/why3/why3-0.83.ebuild @@ -0,0 +1,55 @@ +# Copyright 1999-2014 Gentoo Foundation +# Distributed under the terms of the GNU General Public License v2 +# $Header: $ + +EAPI="2" + +inherit autotools eutils + +DESCRIPTION=" Why3 is a platform for deductive program verification" +HOMEPAGE="http://why3.lri.fr/" +SRC_URI="https://gforge.inria.fr/frs/download.php/33490/${P}.tar.gz" + +LICENSE="LGPL-2" +SLOT="0" +KEYWORDS="~amd64 ~x86" +IUSE="frama-c doc examples" + +DEPEND=">=dev-lang/ocaml-3.12.1 + dev-ml/zarith + sci-mathematics/coq + frama-c? ( >=sci-mathematics/frama-c-20140301 ) + doc? ( dev-tex/rubber )" +RDEPEND="${DEPEND}" + +src_prepare() { + mv doc/why.1 doc/why3.1 + sed -i configure.in -e "s/\"pvs\"/\"sri-pvs\"/g" + sed -i configure -e "s/\"pvs\"/\"sri-pvs\"/g" + sed -i Makefile.in -e "s:DESTDIR =::g" \ + -e "s:\$(RUBBER) --warn all --pdf manual.tex:makeindex manual.tex; \$(RUBBER) --warn all --pdf manual.tex; cd ..:g" +} + +src_configure() { + econf $(use_enable frama-c) || die "econf failed" +} + +src_compile() { + emake -j1 || die "emake failed" + if use doc; then + emake -j1 doc/manual.pdf || die "emake doc failed" + fi +} + +src_install(){ + DESTDIR="${D}" emake install || die "emake install failed" + dodoc CHANGES README Version + doman doc/why3.1 + if use doc; then + dodoc doc/manual.pdf + fi + if use examples; then + insinto /usr/share/doc/${PF} + doins -r examples + fi + } |