commit: 1eea6c611d6f09b6e77a2f06fdc3bf201b1b4db4 Author: Alfredo Tupone <tupone <AT> gentoo <DOT> org> AuthorDate: Fri Feb 7 20:52:53 2025 +0000 Commit: Alfredo Tupone <tupone <AT> gentoo <DOT> org> CommitDate: Fri Feb 7 20:56:27 2025 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=1eea6c61
sci-mathematics/why3-for-spark: add 2023.12.13 Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org> sci-mathematics/why3-for-spark/Manifest | 1 + .../files/why3-for-spark-2023.12.13-flags.patch | 28 +++++ .../why3-for-spark-2023.12.13.ebuild | 127 +++++++++++++++++++++ 3 files changed, 156 insertions(+) diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest index 1653ff46cefc..569da69e95b0 100644 --- a/sci-mathematics/why3-for-spark/Manifest +++ b/sci-mathematics/why3-for-spark/Manifest @@ -1 +1,2 @@ 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 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 +}
