sci-mathematics/why3: bump to 1.8.1

Signed-off-by: Maciej Barć <xgqt@gentoo.org>
This commit is contained in:
Maciej Barć
2025-07-09 21:56:05 +02:00
parent 8a1a354f6b
commit 8cdcd95783
2 changed files with 135 additions and 0 deletions

View File

@@ -1,3 +1,4 @@
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
DIST why3-1.8.1.tar.gz 7371036 BLAKE2B 9cee7cdf2eae77d46b7be6e5c572007e93e449a0ea5ae68d1903b020731bf7197adf2d6b006f10d58a8422961071db90ab5bf676a9c40b4946219df234168e1a SHA512 b188b64cc8f116c2174e78d1ccb65dede0984265b8ed2fdf8160bf67e74bf9fb24cbb1d5b3c130f924424222b9241f89525cade66f5de7ef66d714eb2e6448b4

View File

@@ -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
}