sci-mathematics/why3-for-spark: add USE to select sexp

Closes: https://bugs.gentoo.org/834881
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Alfredo Tupone <tupone@gentoo.org>

2 files changed, 40 insertions, 28 deletions

diff --git a/sci-mathematics/why3-for-spark/metadata.xml b/sci-mathematics/why3-for-spark/metadata.xml
index edf687ae15b9..9b2196685bde 100644
--- a/sci-mathematics/why3-for-spark/metadata.xml
+++ b/sci-mathematics/why3-for-spark/metadata.xml
@@ -21,7 +21,8 @@
 		<flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag>
 		<flag name="html">Build HTML documentation</flag>
 		<flag name="hypothesis-selection">Enable hypothesis selection</flag>
-		<flag name="zarith">Use <pkg>dev-ml/zarith</pkg></flag>
+		<flag name="sexp">Add support for outputting S-expressions with <pkg>dev-ml/ppx_sexp_conv</pkg></flag>
+		<flag name="zarith">Use Zarith (<pkg>dev-ml/zarith</pkg>) instead of Nums (<pkg>dev-ml/num</pkg>) for computations</flag>
 		<flag name="zip">Enable compression of session files</flag>
 	</use>
 </pkgmetadata>
diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
index fb9acf5c9a31..986e7bf497fd 100644
--- a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021-r1.ebuild
@@ -3,7 +3,7 @@
 
 EAPI=7
 
-inherit autotools
+inherit autotools findlib
 
 ADAMIRROR=https://community.download.adacore.com/v1
 ID=dd74ae7ecfd7d56aff7b17cee7a35559384a600f
@@ -16,29 +16,36 @@ SRC_URI="${ADAMIRROR}/${ID}?filename=${MYP}.tar.gz -> ${MYP}.tar.gz"
 LICENSE="GPL-3"
 SLOT="0"
 KEYWORDS="~amd64"
-IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt zarith zip"
+IUSE="coq doc emacs gtk html hypothesis-selection +ocamlopt sexp zarith zip"
 RESTRICT="strip"
 
-DEPEND=">=dev-lang/ocaml-4.11:=[ocamlopt?]
+RDEPEND="
+	>=dev-lang/ocaml-4.11:=[ocamlopt?]
 	dev-ml/menhir:=
 	dev-ml/num:=
 	dev-ml/yojson:=
-	coq? (
-		sci-mathematics/coq
+	coq? ( sci-mathematics/coq )
+	emacs? ( app-editors/emacs:* )
+	gtk? ( dev-ml/lablgtk:=[sourceview] )
+	html? ( dev-tex/hevea:= )
+	hypothesis-selection? ( dev-ml/ocamlgraph:= )
+	sexp? (
+		dev-ml/ppx_deriving:=[ocamlopt?]
+		dev-ml/ppx_sexp_conv:=[ocamlopt?]
+		dev-ml/sexplib:=[ocamlopt?]
 	)
+	zarith? ( dev-ml/zarith:= )
+	zip? ( dev-ml/camlzip:= )
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
 	doc? (
-		dev-tex/rubber
 		dev-python/sphinx
-		media-gfx/graphviz
 		dev-python/sphinxcontrib-bibtex
+		dev-tex/rubber
+		media-gfx/graphviz
 	)
-	gtk? ( dev-ml/lablgtk:=[sourceview] )
-	emacs? ( app-editors/emacs:* )
-	html? ( dev-tex/hevea:= )
-	hypothesis-selection? ( dev-ml/ocamlgraph:= )
-	zarith? ( dev-ml/zarith:= )
-	zip? ( dev-ml/camlzip:= )"
-RDEPEND="${DEPEND}"
+"
 
 S="${WORKDIR}"/${MYP}
 
@@ -68,30 +75,34 @@ QA_FLAGS_IGNORED=(
 	/usr/bin/gnat_server
 	/usr/bin/gnatwhy3
 	/usr/bin/why3realize.cmxs
+	/usr/bin/why3ide.cmxs
 )
 
 REQUIRED_USE="html? ( doc )"
 
 src_prepare() {
 	find examples -name \*gz | xargs gunzip
-	default
 	eautoreconf
+	default
 }
 
 src_configure() {
-	econf \
-		--disable-pvs-libs \
-		--disable-isabelle-libs \
-		--enable-verbose-make \
-		$(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) \
+	local myconf=(
+		--disable-pvs-libs
+		--disable-isabelle-libs
+		--enable-verbose-make
+		$(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 sexp pp-sexp)
+		$(use_enable zarith)
 		$(use_enable zip)
+	)
+	econf "${myconf[@]}"
 }
 
 src_compile() {