sci-mathematics/why3: bump to 1.8.2

Signed-off-by: Maciej Barć <xgqt@gentoo.org>
2026-08-05 12:38:09 -07:00 · 2025-09-27 21:05:42 +02:00
parent 8c53c8e735
commit 8fec647a40
2 changed files with 136 additions and 0 deletions
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -2,3 +2,4 @@ DIST why3-1.6.0.tar.gz 6850062 BLAKE2B 91db6f67a9d0fe24b7d7d18e6c5e9cd362563a557
 DIST why3-1.7.2.tar.gz 7005562 BLAKE2B cd1b25e35147a319e5d5d1f1380ecfaa3555624c797459e8df5cb3b1558928d9c02b567645a2f2952b877c7135a5a393f4b734dd35e569bea6e6b073708901ce SHA512 7e80671480ce0dc3c69514bea2836f5899c686b43a4e8607c27d28e63f78150150dc45fcac5760dbee9721d363e456b1dcaeb1501fc9f63f360722a1021f675f
 DIST why3-1.8.0.tar.gz 7373730 BLAKE2B c650d0578c6ae28f01872f01ba2c6e58ebf00c8fc87f4040f51430aad6b94b52f031b17d5b75178a6a6d5f254f3d42dbbdb031f676335a2d896021c0663192a9 SHA512 8d30ac4a1280a7d7741ef862365e06aa3218a78fd01ca7f969f0d6515245c7259fcc81897bfe08c581c6b37639d1465ab4a96657f3baf4c747988df8201d4549
 DIST why3-1.8.1.tar.gz 7371036 BLAKE2B 9cee7cdf2eae77d46b7be6e5c572007e93e449a0ea5ae68d1903b020731bf7197adf2d6b006f10d58a8422961071db90ab5bf676a9c40b4946219df234168e1a SHA512 b188b64cc8f116c2174e78d1ccb65dede0984265b8ed2fdf8160bf67e74bf9fb24cbb1d5b3c130f924424222b9241f89525cade66f5de7ef66d714eb2e6448b4
+DIST why3-1.8.2.tar.gz 7360550 BLAKE2B 7723bda7242855974b3749511bec883f632f1294ec3f965d69ffc6254db3a05da3ed8df2c441be7ec75676cd915f619469f22658e5a36efa1b0bfcd051acfb1c SHA512 a35e88fafe1aa29c36d2248c1a644eae85afa1bb7b3009193f4a5c28ba684d0882717d63733d8581a7c2cd5ec493e2d15c82baabef615b4d00323fa9309875f8
--- a/sci-mathematics/why3/why3-1.8.2.ebuild
+++ b/sci-mathematics/why3/why3-1.8.2.ebuild
@@ -0,0 +1,135 @@
+# Copyright 1999-2025 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit autotools findlib
+
+DESCRIPTION="Platform for deductive program verification"
+HOMEPAGE="https://www.why3.org/
+	https://gitlab.inria.fr/why3/why3/"
+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 stackify zip"
+
+RDEPEND="
+	!sci-mathematics/why3-for-spark
+	>=dev-lang/ocaml-4.05.0:=[ocamlopt?]
+	>=dev-ml/menhir-20170418:=
+	dev-ml/num:=
+	dev-ml/zarith:=
+	coq? (
+		>=sci-mathematics/coq-8.15:=
+		>=sci-mathematics/flocq-4.2.1
+	)
+	emacs? ( app-editors/emacs:* )
+	gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )
+	re? ( dev-ml/re:= )
+	sexp? (
+		dev-ml/ppx_deriving:=[ocamlopt?]
+		dev-ml/ppx_sexp_conv:=[ocamlopt?]
+		dev-ml/sexplib:=[ocamlopt?]
+	)
+	stackify? ( dev-ml/ocamlgraph:=[ocamlopt?] )
+	zip? ( dev-ml/camlzip:= )
+"
+DEPEND="
+	${RDEPEND}
+"
+BDEPEND="
+	doc? (
+		dev-python/sphinx
+		dev-python/sphinxcontrib-bibtex
+		media-gfx/graphviz
+		dev-texlive/texlive-latex
+		dev-texlive/texlive-fontsrecommended
+		dev-texlive/texlive-latexextra
+	)
+"
+
+DOCS=( CHANGES.md README.md )
+
+src_prepare() {
+	rm configure || die
+	mv configure.in configure.ac || die
+
+	sed -e 's/configure\.in/configure.ac/g' \
+		-i 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/}' \
+		-e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
+		-i 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/}' \
+		-e '/\$(SPHINX)/s/ -d doc\/\.doctrees / /' \
+		-i Makefile.in \
+		|| die
+
+	# remove QA warning about duplicated compressed file:
+	rm examples/mlcfg/basic/why3shapes.gz || die
+
+	eautoreconf
+	default
+
+	# Bad var replacement.
+	sed -e 's|\$(OCAMLC -|\$(ocamlc -|g' \
+		-i configure \
+		|| die
+}
+
+src_configure() {
+	local -x OCAMLC="ocamlc"
+
+	local -a myconf=(
+		--enable-verbose-make
+
+		--disable-frama-c
+		--disable-hypothesis-selection
+		--disable-infer
+		--disable-isabelle-libs
+		--disable-java
+		--disable-js-of-ocaml
+		--disable-pvs-libs
+		--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)
+		$(use_enable stackify)
+		$(use_enable zip)
+	)
+	econf "${myconf[@]}"
+}
+
+src_compile() {
+	emake
+
+	if use doc ; then
+		emake doc
+	fi
+}
+
+src_install(){
+	findlib_src_preinst
+	emake DESTDIR="${ED}" install install-lib
+
+	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
+}