diff options
Diffstat (limited to 'sci-mathematics/why3-for-spark')
4 files changed, 83 insertions, 4 deletions
diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest index a26a6debde4c..c7e4d5cf6348 100644 --- a/sci-mathematics/why3-for-spark/Manifest +++ b/sci-mathematics/why3-for-spark/Manifest @@ -2,6 +2,7 @@ AUX why3-for-spark-2018-gentoo.patch 1015 BLAKE2B 201846ae0ef17bc6d777b7c1a8badd AUX why3-for-spark-2019-gentoo.patch 432 BLAKE2B 44e4dda628cdd9b1d27d000ac0e9a37e56cb87a704cf7f83c634775f7ecf8d868d9750561e078c318be5079f91bf9e0f30de9616e781a8a128fdd853e74b431f SHA512 804d9914031450ebdeeea24d2aad472b1765e0534d8ebe404189f039d78be361b51deb21027c85f2d1919668c1f5ef25e65694424a22f7533e5cd264e7e5a191 DIST why3-2019-20190517-197BB-src.tar.gz 9439414 BLAKE2B 68072064e8ee9152528c90afc948047a1f4d58b960ac05b276761fdca5ba1204100c75f33db7bb0ea1a8a646b734e62892ed41bd875b954354f52b8f9d498d4a SHA512 9169a4ff9ee994a19f9f04b689d1b9c679f5340bcd631d7d49b4c55064f505bd5a6ca8149077e5d24d36f5365f0cab58587094e86f352a9105fc46f10c0746ba DIST why3-for-spark-gpl-2018-src.tar.gz 7682767 BLAKE2B 0b0272ca4d5519ca402990b234d0847378bcd2a0949fea78ea10e355233a16aebe79b938cdf8e4daadabb909171cab83b9d6ccacf9f2dc1c0b57bb6da6fd1fe0 SHA512 fc798acf343484fd8e70f470a318753c9a0e9967ff579f20ec185bf3c2a75e7a4a556388fc86a378610ce4a467f3e722c6f610da34d4c33bc3d6b10551731f07 -EBUILD why3-for-spark-2018.ebuild 1699 BLAKE2B 5d648c18c5c77e02afab395c874a769042acc6b705901477c016bd3ab77c02a892116d3a0d85631a67a2ffacc7cf044a4de3547b20deb3e2fdabdafd6648d6ca SHA512 271340f364718d8a29b36b4def19806d8428d7b84c0b8e882898018c91cfc892ae2f6d3d0dc74e05a5788ba0d73810ca1537b4f2ebb1f84f21f2cb588246a607 -EBUILD why3-for-spark-2019.ebuild 1768 BLAKE2B e598cf8b526394df6493c1f8753d0e45c9ec29a4e2337c19a16f00ccaa87bbf7021f0e9d5d2a3d336ac442350b8cc9280bc27bcb4483072998e297041887d8bd SHA512 43b68af3ada262eec23ed89adbf8e2ae3524a915eb649d219f9cbf663ad6face045ef3a29ad9a89d58d20fc00ce006216daf63ec0c6dcbe21612a8762e2a240a +EBUILD why3-for-spark-2018.ebuild 1712 BLAKE2B 6bab5512436341fe88e22657752081b5ed78f6ae27f1b3e5dc95a916a2b641f1f362aba40a333b74622a3832b5c385100d9266bdc25a692f43a20a93be2605a8 SHA512 0077d68c18911e71f5ff3a54b48700b3e63dbf976acf9f153ebb9ce81d8de6f697b9750be0ac5dfd214f40677a3dbe9325d8005df169a853b90980099d7ce762 +EBUILD why3-for-spark-2019-r1.ebuild 1829 BLAKE2B 6329924da6edd1c9174ed3ce4b469e6b32ced981761a63077c75a4b28d4299365d1382dade9e5631f2fad90815f80afe828b01f517275c1f9c9d167f769fba8c SHA512 c8e256b8c9944791f2d86e86e2e48d277a6e98196de2f62f6d6afcf92d8d900d63a0971fc9f8575b752fc7a83082bffdf96f3bb5ca39c63e68f4b4cb9da413d2 +EBUILD why3-for-spark-2019.ebuild 1781 BLAKE2B 00bb8e39eff2bc94757bb823c663911ad308488a3d3491e6f00a4a30e541a2724a7e29f999c4c32966d9cc45feaf99b76bf3259a6014b133d9125ccff687fdbf SHA512 81e68202740eaea33e19dad98c14e6baa9fafaa69a4a25d87132bb55248d977cc94871f50929802f67fd670a068f01ae62d9863a8a091e97c4e5d762566850c3 MISC metadata.xml 1363 BLAKE2B 820bfc974ca6984f78340f223f8f19d12f0313016118110a35cfe149129c2dc189d6f03f34bf3d30c9d3e5d9c9ab90bba33dca4320c034821a7a89f97b92a7f9 SHA512 ee8323cc37fdea800e355fc14ba67cac66c3ec3c41528d481a7e938b1d3e23859bdddfb06d3b6653725cdcfcc0d07e66ba1d3cc80b3637a781db7bab5f7dc677 diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild index 5400b37276c2..2335a61928f9 100644 --- a/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild +++ b/sci-mathematics/why3-for-spark/why3-for-spark-2018.ebuild @@ -23,7 +23,7 @@ DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?] coq? ( sci-mathematics/coq ) doc? ( dev-tex/rubber ) gtk? ( dev-ml/lablgtk[sourceview] ) - emacs? ( virtual/emacs ) + emacs? ( >=app-editors/emacs-23.1:* ) html? ( dev-tex/hevea ) hypothesis-selection? ( dev-ml/ocamlgraph ) zarith? ( dev-ml/zarith ) diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild new file mode 100644 index 000000000000..8d152264c067 --- /dev/null +++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019-r1.ebuild @@ -0,0 +1,78 @@ +# Copyright 1999-2020 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=6 + +inherit autotools + +MYP=why3-${PV}-20190517-197BB-src + +DESCRIPTION="Platform for deductive program verification" +HOMEPAGE="http://why3.lri.fr/" +SRC_URI="http://mirrors.cdn.adacore.com/art/5cdf915d31e87a8f1c967d54 + -> ${MYP}.tar.gz" + +LICENSE="GPL-3" +SLOT="0" +KEYWORDS="~amd64" +IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt profiling zarith zip" +RESTRICT=strip + +DEPEND=">=dev-lang/ocaml-4.09.0[ocamlopt?] + >=dev-ml/ocamlbuild-0.14.0 + dev-ml/menhir + dev-ml/num + coq? ( >=sci-mathematics/coq-8.9.1 ) + doc? ( dev-tex/rubber ) + gtk? ( dev-ml/lablgtk[sourceview] ) + emacs? ( >=app-editors/emacs-23.1:* ) + html? ( dev-tex/hevea ) + hypothesis-selection? ( dev-ml/ocamlgraph ) + zarith? ( dev-ml/zarith ) + zip? ( >=dev-ml/camlzip-1.07 )" +RDEPEND="${DEPEND}" + +S="${WORKDIR}"/${MYP} + +PATCHES=( "${FILESDIR}"/${P}-gentoo.patch ) + +REQUIRED_USE="html? ( doc )" + +src_configure() { + econf \ + --disable-pvs-libs \ + --disable-isabelle-libs \ + --enable-verbose-make \ + $(use_enable coq coq-libs) \ + $(use_enable doc) \ + $(use_enable emacs emacs-compilation) \ + $(use_enable gtk ide) \ + $(use_enable html html-doc) \ + $(use_enable hypothesis-selection) \ + $(use_enable ocamlopt native-code) \ + $(use_enable profiling) \ + $(use_enable zarith) \ + $(use_enable zip) +} + +src_compile() { + emake -j1 + if use ocamlopt; then + emake byte + fi + use doc && emake doc +} + +src_install() { + emake DESTDIR="${D}" -j1 install + emake DESTDIR="${D}" -j1 install-lib + emake DESTDIR="${D}" install_spark2014_dev + dosym ../why3server /usr/$(get_libdir)/why3/commands/why3server + einstalldocs + docompress -x /usr/share/doc/${PF}/examples + dodoc -r examples + if use doc; then + dodoc doc/manual.pdf + use html && dodoc -r doc/html + fi +} diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild index a0caa7b6cf68..409bfc36cda5 100644 --- a/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild +++ b/sci-mathematics/why3-for-spark/why3-for-spark-2019.ebuild @@ -23,7 +23,7 @@ DEPEND=">=dev-lang/ocaml-4.02.3[ocamlopt?] coq? ( sci-mathematics/coq ) doc? ( dev-tex/rubber ) gtk? ( dev-ml/lablgtk[sourceview] ) - emacs? ( virtual/emacs ) + emacs? ( >=app-editors/emacs-23.1:* ) html? ( dev-tex/hevea ) hypothesis-selection? ( dev-ml/ocamlgraph ) zarith? ( dev-ml/zarith ) |