2 files changed, 136 insertions, 0 deletions
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index f2ec969686e3..2a6a677eb317 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,6 +1,8 @@
 AUX why3-1.7.2-signum.patch 406 BLAKE2B ab81e95db7537a31fd75e3d0551ee57cf664aa6f41779c2d72100b39c88ca0f3a90fa517e07dd1f17c3f93fff134802cb1e3fa192e15b66b8163e840c1e75dd8 SHA512 3491b58cc54bfdd8601242b2f78d7a8afbed8097758610dd38815e8ed90cf462d02ded16905838a51275fd16ed634f89ba11e38a8d573c78ca01477fcfa35237
 DIST why3-1.6.0.tar.gz 6850062 BLAKE2B 91db6f67a9d0fe24b7d7d18e6c5e9cd362563a55702bfb28c478754f53e831beb3033adde251214facd8d64ab923389b0b9fe7b240b6cd09f0b4b3e6f8eca143 SHA512 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1
 DIST why3-1.7.2.tar.gz 7005562 BLAKE2B cd1b25e35147a319e5d5d1f1380ecfaa3555624c797459e8df5cb3b1558928d9c02b567645a2f2952b877c7135a5a393f4b734dd35e569bea6e6b073708901ce SHA512 7e80671480ce0dc3c69514bea2836f5899c686b43a4e8607c27d28e63f78150150dc45fcac5760dbee9721d363e456b1dcaeb1501fc9f63f360722a1021f675f
+DIST why3-1.8.0.tar.gz 7373730 BLAKE2B c650d0578c6ae28f01872f01ba2c6e58ebf00c8fc87f4040f51430aad6b94b52f031b17d5b75178a6a6d5f254f3d42dbbdb031f676335a2d896021c0663192a9 SHA512 8d30ac4a1280a7d7741ef862365e06aa3218a78fd01ca7f969f0d6515245c7259fcc81897bfe08c581c6b37639d1465ab4a96657f3baf4c747988df8201d4549
 EBUILD why3-1.6.0.ebuild 2349 BLAKE2B 946115ce4d70ed1505fb3072c7ad6e67c6c3ea0c97a03dd6141b069ef8b2502f43e44717ff9f3dbc5c4de367fb25d7dbd98369f8313ff75ba0471f35c320df04 SHA512 8a196dfa7a161c980e2023f1363d6ff91af3ca854e96539ca44d004efa2b5d813b480c79dd0d51e31796a0c0b6f886d094bd06751469dd8b236aad239ddaf1f7
 EBUILD why3-1.7.2.ebuild 2410 BLAKE2B 00e650a1716213d2be02c98e07157d44311996a6faf64c52193f7bbe1dcf16dde133a81468cc36e950a48c0891100096119960323b0045a79ae068599c6685b3 SHA512 aa928c405d247f6462b2e2571f5efe2e01993034d6515d6f0c4a3bb847fb352f319621ec1d31ffb3e6f8336cc32372cb6170e621bf9507e71866c5b1dddfd612
+EBUILD why3-1.8.0.ebuild 2764 BLAKE2B 1380a104d899b427a4009cf4ac38bfe813c802a1dede77666efafe8021eb259d1ee49ef9a49da345e2dc912ce308fb467641c85018fe8c8396eeb5381519f13d SHA512 6452354cb1a3f30541e2e50fbec3f307985af70ecee63cea2ddac9c51ef6d760e294eea21b24336150cfc8aa0ebd76c8c4fcebf7c568422c90ff58bb35a11c8f
 MISC metadata.xml 1902 BLAKE2B 1868834e446b471f4b3f7b11fc987661dee83790110fa31c73f0060fd8340891ff85ec16591d1326977760c726ec04bd06a4cca46fb1a87f792340a002cba247 SHA512 4dc9408d44eafc037bfce9c996570e58c161e07c3ded2a052954c834fcf8c3a36cf8429493bc705ced7445d199eaf207cabb5df1b0ed6b625015af518e55d9e9
diff --git a/sci-mathematics/why3/why3-1.8.0.ebuild b/sci-mathematics/why3/why3-1.8.0.ebuild
new file mode 100644
index 000000000000..7d4c10c81bae
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.8.0.ebuild
@@ -0,0 +1,134 @@
+# 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/"
+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
+}