diff options
Diffstat (limited to 'sci-mathematics')
| -rw-r--r-- | sci-mathematics/Manifest.gz | bin | 19534 -> 19532 bytes | |||
| -rw-r--r-- | sci-mathematics/why3-for-spark/Manifest | 3 | ||||
| -rw-r--r-- | sci-mathematics/why3-for-spark/files/why3-for-spark-2023.12.13-flags.patch | 28 | ||||
| -rw-r--r-- | sci-mathematics/why3-for-spark/why3-for-spark-2023.12.13.ebuild | 127 |
4 files changed, 158 insertions, 0 deletions
diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz Binary files differindex 8122d580f7fa..a895f5bcc3fc 100644 --- a/sci-mathematics/Manifest.gz +++ b/sci-mathematics/Manifest.gz diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest index 57c67374b35d..29f43833e16e 100644 --- a/sci-mathematics/why3-for-spark/Manifest +++ b/sci-mathematics/why3-for-spark/Manifest @@ -2,6 +2,9 @@ AUX why3-for-spark-2020-bibtex.patch 288 BLAKE2B 50459e0dfe6ef3d5b455993e9e7fbc3 AUX why3-for-spark-2020-gentoo.patch 332 BLAKE2B d71897d1d253a95f2a783483ee7bb0d243961cbc7218e05f3717a95388da0613e3f162a39cb4dac816035d6381ac69f189e352f2d83530b70b46b2439f7b92c3 SHA512 766de53c5cdede4bfdbac671851ec7de5060712622d4c89ce9117ef31596c2e4bd938bd2fe50d6a969f93ae252c40c83c2f782ad710fd52ab652434765483f90 AUX why3-for-spark-2021-flags.patch 1234 BLAKE2B 617040fbf9204382adda8161a07ab5244bb60daf1936a8c549ccd3c28a10e447c80cf8875ef2d16103751dfc9881c15e0a8f39f2877fe7d0adf9a8dd374e1e21 SHA512 abbe1b1f9ed6b5aedf0521e0f8d19b6f0267c5304000419f6df91b581bfa99a46c4b46ceed5a294ffc47c0b2f987666c6cd5801049da14b79f24885cbd227bcb AUX why3-for-spark-2021-make.patch 350 BLAKE2B 970a7ba442a22d96e5807aacd07997587c20a53660045392229e2069801ae4b8f92c5385fa732341acb2498dbcf515d51aa5f2e96d6375006dfedc7ee2eea53f SHA512 b729369bb74e3a8546b449f186cac490d83e764a4fe801de9dd9cb134a8e21dcd9b45af6c63733d953b3072e4363e95599d0cd8e6dfdb936648c3acb9918828e +AUX why3-for-spark-2023.12.13-flags.patch 863 BLAKE2B c6456f944667dc72eb87b2e76d3ac0537208bbbda6b9fa4584295380fab030a2b3751cf1cf490c88e78beb1547ac2daaec2e8246258a640d0d94d56ddeb9425b SHA512 f5db8c0c03eff52bfe9f675dc7e784d8dd86e37e070fa5756dbc7065b88577c7006d9d132fc4093b25abde692b114facf9445965b5485bea56c97290b5087af5 DIST why3-2021-20210519-19ADF-src.tar.gz 10386938 BLAKE2B 93b6323c562126244f5cccef34088a521fe3dc1cec07c966e94472503ec8492707b20a641936449307f0439e711a82260d36679cbc69f53df8e7886a1d3673c3 SHA512 65e3c1430001962f2c7cce786f3e30f14b5295cff89c4087d95c1545e81743723319ba0309dbe15c4c46552110b25ff57addc3ee085dade02ea59a2273b127db +DIST why3-for-spark-2023.12.13.tar.gz 7119379 BLAKE2B 4fd78efaabc2ca40853a905b1581ed976660f5b1b01ab9490c422022284132d8306289aad3eb2111d85d5cde5b50242b5d94d313e8d78a7443b7fcc4298fd11b SHA512 88220595eae9c5cf4125c0dc9d5176e637a1f1e355f61f51176bdb7643a000c837e501101e45c2b50ae3f41f81436e1133be241fd5fb0b6816823b2106113ae7 EBUILD why3-for-spark-2021-r1.ebuild 3103 BLAKE2B fd8e8cd70d1d38c69fad088c3ba66f101e335bea625ab3dffe996d1462f364a2e4e5489869c462396b4a0ec7a4e418df593f1869927188840ffadd4b56a02cb6 SHA512 dc2472a0a6375bb8cf08760d438fdb4cd3f4dcc41063f6b4950657cf7d277c7b6506269fbbd8c711b951fc8cfb8d65fde9df5fa4af556c7a68814001961370e9 +EBUILD why3-for-spark-2023.12.13.ebuild 3023 BLAKE2B 0184260f5a33640e520bb05199d38f98860dd03e2e09e179cd6a7052c104901b5d6004445566366c127ae595c0e5dbea8017e9f767b7fe638f5f7dc4972ac6ab SHA512 cf860788b9775ebaa7924f6b5ae977d74f02e56e05abd43dc82a3a74c4fd057597d351988d6c66bdc9e6d7f556d9a6ee5c793db59584b723886f86732ec55af1 MISC metadata.xml 1561 BLAKE2B 48c1ebe394b9a4152cd3b3a0560ff5e2d0e93e48422265d224b49b80b5b625b110f3561a09825e7e6efaf1dbb1dca8362612cfdccd43d954f4a848fb39624653 SHA512 02c1cecdd192e289d0146d0ba16148a2fcd9daddc39b6afbaa2a510594475a12cacd4b4c92d1c1b7bf40c291a90d66b887fdbf19fa82af45f197e2323e4b2b20 diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2023.12.13-flags.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2023.12.13-flags.patch new file mode 100644 index 000000000000..ec8d74745789 --- /dev/null +++ b/sci-mathematics/why3-for-spark/files/why3-for-spark-2023.12.13-flags.patch @@ -0,0 +1,28 @@ +--- a/Makefile.in 2020-06-12 21:03:33.375534124 +0200 ++++ b/Makefile.in 2020-06-12 21:03:48.623283408 +0200 +@@ -129,7 +129,7 @@ + + WARNINGS = A-4-9-41-42-44-45-52@5@8@14@48@50 + +-FLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -thread $(INCLUDES) ++FLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -thread $(INCLUDES) -cclib "$(LDFLAGS)" -ccopt "$(CFLAGS)" + OFLAGS = $(FLAGS) + BFLAGS = $(FLAGS) + +@@ -807,13 +807,13 @@ + all: $(TOOLS) + + lib/why3server$(EXE): $(SERVER_O) +- $(CC) -Wall -o $@ $^ ++ $(CC) -Wall $(CFLAGS) -o $@ $^ $(LDFLAGS) + + lib/why3cpulimit$(EXE): $(CPULIM_O) +- $(CC) -Wall -o $@ $^ ++ $(CC) -Wall $(CFLAGS) -o $@ $^ $(LDFLAGS) + + %.o: %.c +- $(CC) -Wall -O -g -o $@ -c $< ++ $(CC) -Wall $(CFLAGS) -O -g -o $@ -c $< + + uninstall-bin:: + rm -f $(LIBDIR)/why3/why3server$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE) diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2023.12.13.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2023.12.13.ebuild new file mode 100644 index 000000000000..fcbbcab6ccbc --- /dev/null +++ b/sci-mathematics/why3-for-spark/why3-for-spark-2023.12.13.ebuild @@ -0,0 +1,127 @@ +# Copyright 1999-2025 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +inherit autotools findlib + +ID=fb4ca6cd8c7d888d3e8d281e6de87c66ec20f084 + +DESCRIPTION="SPARK 2014 repository for the Why3 verification platform" +HOMEPAGE="https://www.why3.org/ https://github.com/AdaCore/why3" +SRC_URI="https://github.com/AdaCore/why3/archive/${ID}.tar.gz + -> ${P}.tar.gz" + +S="${WORKDIR}"/why3-${ID} + +LICENSE="GPL-3" +SLOT="0" +KEYWORDS="~amd64" +IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt sexp zarith zip" +RESTRICT="strip" + +RDEPEND=" + >=dev-lang/ocaml-4.11:=[ocamlopt?] + dev-ml/menhir:=[ocamlopt?] + dev-ml/num:=[ocamlopt?] + dev-ml/yojson:= + coq? ( sci-mathematics/coq ) + emacs? ( app-editors/emacs:* ) + gtk? ( dev-ml/lablgtk:=[sourceview] ) + html? ( dev-tex/hevea:= ) + hypothesis-selection? ( dev-ml/ocamlgraph:= ) + dev-ml/ppx_deriving:=[ocamlopt?] + dev-ml/ppx_sexp_conv:=[ocamlopt?] + dev-ml/sexplib:=[ocamlopt?] + zarith? ( dev-ml/zarith:=[ocamlopt?] ) + zip? ( dev-ml/camlzip:=[ocamlopt?] ) +" +DEPEND="${RDEPEND}" +BDEPEND=" + doc? ( + dev-python/sphinx + dev-python/sphinxcontrib-bibtex + dev-tex/rubber + media-gfx/graphviz + ) +" + +PATCHES=( + "${FILESDIR}"/${PN}-2020-gentoo.patch + "${FILESDIR}"/${P}-flags.patch + "${FILESDIR}"/${PN}-2021-make.patch #Bug #883167 + "${FILESDIR}"/${PN}-2020-bibtex.patch +) + +QA_FLAGS_IGNORED=( + '/usr/lib.*/why3/commands/.*cmxs' + '/usr/lib.*/why3/plugins/.*cmxs' + '/usr/lib.*/ocaml/why3/.*cmxs' + /usr/bin/why3 + /usr/bin/why3config.cmxs + /usr/bin/why3session.cmxs + /usr/bin/gnat_server + /usr/bin/gnatwhy3 + /usr/bin/why3realize.cmxs + /usr/bin/why3ide.cmxs +) + +# Forcing native for bug #913497 +REQUIRED_USE="html? ( doc ) ocamlopt" + +src_prepare() { + find examples -name \*gz | xargs gunzip + eautoreconf + default +} + +src_configure() { + local myconf=( + --disable-pvs-libs + --disable-isabelle-libs + --enable-verbose-make + --enable-sexp + $(use_enable coq coq-libs) + $(use_enable doc) + $(use_enable emacs emacs-compilation) + $(use_enable gtk ide) + $(use_enable html html-pdf) + $(use_enable hypothesis-selection) + $(use_enable ocamlopt native-code) + $(use_enable zarith) + $(use_enable zip) + ) + econf "${myconf[@]}" +} + +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 + local cmdPath=/usr/$(get_libdir)/why3/commands + dosym ../why3server ${cmdPath}/why3server + # Remove duplicated files + for filename in config.cmxs ide.cmxs realize.cmxs server session.cmxs; do + if [[ -e "${D}"${cmdPath}/why3${filename} ]]; then + rm "${D}"${cmdPath}/why3${filename} + dosym ../../../bin/why3${filename} ${cmdPath}/why3${filename} + fi + done + rm "${D}"/usr/$(get_libdir)/why3/why3cpulimit + dosym ../../bin/why3cpulimit /usr/$(get_libdir)/why3/why3cpulimit + + einstalldocs + docompress -x /usr/share/doc/${PF}/examples + dodoc -r examples + if use doc; then + use html && dodoc -r doc/html + fi +} |