gentoo auto-resync : 20:11:2024 - 03:02:59

2 files changed, 109 insertions, 0 deletions

diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest
index ed5979c08b8f..32defd10808f 100644
--- a/sci-mathematics/why3/Manifest
+++ b/sci-mathematics/why3/Manifest
@@ -1,3 +1,5 @@
 DIST why3-1.6.0.tar.gz 6850062 BLAKE2B 91db6f67a9d0fe24b7d7d18e6c5e9cd362563a55702bfb28c478754f53e831beb3033adde251214facd8d64ab923389b0b9fe7b240b6cd09f0b4b3e6f8eca143 SHA512 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1
+DIST why3-1.7.2.tar.gz 7005562 BLAKE2B cd1b25e35147a319e5d5d1f1380ecfaa3555624c797459e8df5cb3b1558928d9c02b567645a2f2952b877c7135a5a393f4b734dd35e569bea6e6b073708901ce SHA512 7e80671480ce0dc3c69514bea2836f5899c686b43a4e8607c27d28e63f78150150dc45fcac5760dbee9721d363e456b1dcaeb1501fc9f63f360722a1021f675f
 EBUILD why3-1.6.0.ebuild 2348 BLAKE2B 0b8f27f14bb7d2117a9f5f6451d12e57ae3123ac6f491c653fb762bdf2410b5af17f9f3d7c2655c56f6a2f3f198aad07411a7c07e4943e62e1673b66e4779e41 SHA512 7a4ff6be794f77a6a319ee5e39e0bb3c80c82777d45da510d54ab6ac1793c0d249ebf10516c4db4ad7bf27441a0ef37171c43c04295ae0bd757f34619ac6fd61
+EBUILD why3-1.7.2.ebuild 2364 BLAKE2B f58d8a3fe69e1f50efd2fa08b47091e83a80fb8796c0b8326d242ab918792342817abf61422f0b930f94e14a333e332ec48254ffa95522e93637a8814e14f917 SHA512 45fc4136e2efb6e95c3bf39a48857246e02be2cf557fda5d2f231cd8e9b004ad23d197b8b2566c6b041f18471994dec9e679f83979ac355bfa4f2e6247af98b4
 MISC metadata.xml 1902 BLAKE2B 1868834e446b471f4b3f7b11fc987661dee83790110fa31c73f0060fd8340891ff85ec16591d1326977760c726ec04bd06a4cca46fb1a87f792340a002cba247 SHA512 4dc9408d44eafc037bfce9c996570e58c161e07c3ded2a052954c834fcf8c3a36cf8429493bc705ced7445d199eaf207cabb5df1b0ed6b625015af518e55d9e9
diff --git a/sci-mathematics/why3/why3-1.7.2.ebuild b/sci-mathematics/why3/why3-1.7.2.ebuild
new file mode 100644
index 000000000000..7517d54b1b67
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.7.2.ebuild
@@ -0,0 +1,107 @@
+# Copyright 1999-2024 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://why3.lri.fr/"
+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 +zarith zip"
+
+RDEPEND="
+	!sci-mathematics/why3-for-spark
+	>=dev-lang/ocaml-4.05.0:=[ocamlopt?]
+	>=dev-ml/menhir-20170418:=
+	dev-ml/num:=
+	coq? ( >=sci-mathematics/coq-8.7:= )
+	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?] )
+	zarith? ( dev-ml/zarith:= )
+	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() {
+	mv configure.in configure.ac || die
+
+	sed -i 's/configure\.in/configure.ac/g' 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
+}
+
+src_configure() {
+	local -a myconf=(
+		--enable-verbose-make
+		--disable-frama-c
+		--disable-hypothesis-selection
+		--disable-infer
+		--disable-isabelle-libs
+		--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 zarith)
+		$(use_enable zip)
+	)
+	econf "${myconf[@]}"
+}
+
+src_compile() {
+	emake
+	emake plugins
+
+	use doc && emake doc
+}
+
+src_install(){
+	findlib_src_preinst
+	emake install install-lib DESTDIR="${ED}"
+
+	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
+}