[gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/

[gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/

[Andrew Ammerlaan]

commit:     4d56f41bcbf02ab76cd1d36ecc7e1f93a3261ce2
Author:     Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
AuthorDate: Thu Mar  4 13:07:33 2021 +0000
Commit:     Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
CommitDate: Thu Mar  4 13:07:33 2021 +0000
URL:        https://gitweb.gentoo.org/proj/sci.git/commit/?id=4d56f41b

sci-mathematics/why3: use the proper version number for frame-c

Package-Manager: Portage-3.0.16, Repoman-3.0.2
Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> riseup.net>

 sci-mathematics/why3/why3-1.3.3.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild
index 41c1f9b9f..ab4a54b91 100644
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -29,7 +29,7 @@ DEPEND="
 	dev-ml/menhir
 	dev-ml/num
 	sci-mathematics/coq
-	frama-c? ( >=sci-mathematics/frama-c-20140301 )
+	frama-c? ( >=sci-mathematics/frama-c-22 )
 	float? ( sci-mathematics/flocq )
 "
 RDEPEND="${DEPEND}"

[gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/

[Andrew Ammerlaan]

commit:     05665ef52991dd10e4c912a13b34656b3397fefc
Author:     Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
AuthorDate: Mon Dec 13 10:57:12 2021 +0000
Commit:     Andrew Ammerlaan <andrewammerlaan <AT> gentoo <DOT> org>
CommitDate: Mon Dec 13 10:57:56 2021 +0000
URL:        https://gitweb.gentoo.org/proj/sci.git/commit/?id=05665ef5

sci-mathematics/why3: remove: ::guru version moved to ::gentoo

Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> gentoo.org>

 sci-mathematics/why3/metadata.xml      | 24 -------------
 sci-mathematics/why3/why3-1.3.3.ebuild | 63 ----------------------------------
 2 files changed, 87 deletions(-)

diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
deleted file mode 100644
index 5f92771c1..000000000
--- a/sci-mathematics/why3/metadata.xml
+++ /dev/null
@@ -1,24 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
-<pkgmetadata>
-	<maintainer type="project">
-		<email>sci-mathematics@gentoo.org</email>
-		<name>Gentoo Mathematics Project</name>
-	</maintainer>
-	<longdescription>
-Why3 is a platform for deductive program verification. It provides
-a rich language for specification and programming, called WhyML,
-and relies on external theorem provers, both automated and interactive,
-to discharge verification conditions. Why3 comes with a standard
-library of logical theories (integer and real arithmetic, Boolean
-operations, sets and maps, etc.) and basic programming data structures
-(arrays, queues, hash tables, etc.). A user can write WhyML programs
-directly and get correct-by-construction OCaml programs through an
-automated extraction mechanism. WhyML is also used as an intermediate
-language for the verification of C, Java, or Ada programs.
-</longdescription>
-	<use>
-		<flag name="float">Add <pkg>sci-mathematics/flocq</pkg> support</flag>
-		<flag name="frama-c">Enable Frama-C plugin</flag>
-	</use>
-</pkgmetadata>

diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild
deleted file mode 100644
index 62706c32f..000000000
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ /dev/null
@@ -1,63 +0,0 @@
-# Copyright 1999-2021 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=7
-
-PYTHON_COMPAT=( python3_{7,8,9} )
-DOCS_BUILDER="sphinx"
-DOCS_DIR="doc"
-DOCS_DEPEND="
-	dev-python/sphinxcontrib-bibtex
-	dev-python/graphviz
-"
-
-inherit python-any-r1 docs
-
-DESCRIPTION="Why3 is a platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https://gforge.inria.fr/frs/download.php/file/38367/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0"
-KEYWORDS="~amd64"
-
-IUSE="float frama-c examples"
-
-DEPEND="
-	>=dev-lang/ocaml-3.12.1
-	dev-ml/zarith
-	dev-ml/menhir
-	dev-ml/num
-	sci-mathematics/coq
-	frama-c? ( >=sci-mathematics/frama-c-22 )
-	float? ( sci-mathematics/flocq )
-"
-RDEPEND="${DEPEND}"
-
-src_prepare() {
-	default
-	mv doc/why.1 doc/why3.1 || die
-	sed -i configure.in -e "s/\"pvs\"/\"sri-pvs\"/g" || die
-	sed -i configure -e "s/\"pvs\"/\"sri-pvs\"/g" || die
-	# fix dev-ml/num path
-	sed -i configure.in -e "s/nums.cma/num.cma/g" -e "s/num.cmi/core\/num.cmi/g" || die
-	sed -i configure -e "s/nums.cma/num.cma/g" -e "s/num.cmi/core\/num.cmi/g" || die
-	sed -i Makefile.in -e "s:DESTDIR =::g" \
-		-e "s:\$(RUBBER) --warn all --pdf manual.tex:makeindex manual.tex; \$(RUBBER) --warn all --pdf manual.tex; cd ..:g" || die
-	# add autodoc to sphinx
-	sed -i -e "/^extensions = \[/a \ \ \ \ \'sphinx.ext.autodoc\'," doc/conf.py || die
-}
-
-src_configure() {
-	econf $(use_enable frama-c)
-}
-
-src_compile() {
-	docs_compile
-	default
-}
-
-src_install(){
-	default
-	use examples && dodoc -r examples
-}

[gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/

[Andrew Ammerlaan]

commit:     e6a9d839270d75261caea7f633aea55c6bb9cd33
Author:     Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
AuthorDate: Thu Mar  4 13:47:18 2021 +0000
Commit:     Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
CommitDate: Thu Mar  4 13:47:18 2021 +0000
URL:        https://gitweb.gentoo.org/proj/sci.git/commit/?id=e6a9d839

sci-mathematics/why3: fix StaticURL

Package-Manager: Portage-3.0.16, Repoman-3.0.2
Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> riseup.net>

 sci-mathematics/why3/why3-1.3.3.ebuild | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild
index ab4a54b91..62706c32f 100644
--- a/sci-mathematics/why3/why3-1.3.3.ebuild
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -15,7 +15,7 @@ inherit python-any-r1 docs
 
 DESCRIPTION="Why3 is a platform for deductive program verification"
 HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https://gforge.inria.fr/frs/download.php/file/38367/why3-1.3.3.tar.gz"
+SRC_URI="https://gforge.inria.fr/frs/download.php/file/38367/${P}.tar.gz"
 
 LICENSE="LGPL-2"
 SLOT="0"
@@ -59,9 +59,5 @@ src_compile() {
 
 src_install(){
 	default
-
-	if use examples; then
-		insinto /usr/share/doc/${PF}
-		doins -r examples
-	fi
+	use examples && dodoc -r examples
 }

[gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/

[Andrew Ammerlaan]

commit:     3da11fc58fc8db8834367e4d3fbb36e1e51011f3
Author:     Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
AuthorDate: Thu Mar  4 11:52:56 2021 +0000
Commit:     Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
CommitDate: Thu Mar  4 11:52:56 2021 +0000
URL:        https://gitweb.gentoo.org/proj/sci.git/commit/?id=3da11fc5

sci-mathematics/why3: drop old

Package-Manager: Portage-3.0.16, Repoman-3.0.2
Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> riseup.net>

 sci-mathematics/why3/why3-0.83.ebuild | 59 -----------------------------------
 1 file changed, 59 deletions(-)

diff --git a/sci-mathematics/why3/why3-0.83.ebuild b/sci-mathematics/why3/why3-0.83.ebuild
deleted file mode 100644
index ac914306c..000000000
--- a/sci-mathematics/why3/why3-0.83.ebuild
+++ /dev/null
@@ -1,59 +0,0 @@
-# Copyright 1999-2016 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=5
-
-inherit eutils
-
-DESCRIPTION=" Why3 is a platform for deductive program verification"
-HOMEPAGE="http://why3.lri.fr/"
-SRC_URI="https://gforge.inria.fr/frs/download.php/33490/${P}.tar.gz"
-
-LICENSE="LGPL-2"
-SLOT="0"
-KEYWORDS="~amd64"
-IUSE="float frama-c doc examples"
-
-DEPEND=">=dev-lang/ocaml-3.12.1
-		dev-ml/zarith
-		sci-mathematics/coq
-		frama-c? ( >=sci-mathematics/frama-c-20140301 )
-		float? ( sci-mathematics/flocq )
-		doc? ( dev-tex/rubber )"
-RDEPEND="${DEPEND}"
-
-DOCS=( CHANGES README Version )
-
-src_prepare() {
-	mv doc/why.1 doc/why3.1 || die
-	sed -i configure.in -e "s/\"pvs\"/\"sri-pvs\"/g" || die
-	sed -i configure -e "s/\"pvs\"/\"sri-pvs\"/g" || die
-	sed -i Makefile.in -e "s:DESTDIR =::g" \
-		-e "s:\$(RUBBER) --warn all --pdf manual.tex:makeindex manual.tex; \$(RUBBER) --warn all --pdf manual.tex; cd ..:g" || die
-}
-
-src_configure() {
-	econf $(use_enable frama-c)
-}
-
-src_compile() {
-	MAKEOPTS+=" -j1"
-
-	default
-	if use doc; then
-		emake doc/manual.pdf
-	fi
-}
-
-src_install(){
-	default
-
-	doman doc/why3.1
-	if use doc; then
-		dodoc doc/manual.pdf
-	fi
-	if use examples; then
-		insinto /usr/share/doc/${PF}
-		doins -r examples
-	fi
-}

[gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/

[Andrew Ammerlaan]

commit:     bd7ac0e244a891713e3dea57ca737b4dfd980175
Author:     Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
AuthorDate: Thu Mar  4 11:52:39 2021 +0000
Commit:     Andrew Ammerlaan <andrewammerlaan <AT> riseup <DOT> net>
CommitDate: Thu Mar  4 11:52:39 2021 +0000
URL:        https://gitweb.gentoo.org/proj/sci.git/commit/?id=bd7ac0e2

sci-mathematics/why3: version bump 1.3.3, EAPI bump

Package-Manager: Portage-3.0.16, Repoman-3.0.2
Signed-off-by: Andrew Ammerlaan <andrewammerlaan <AT> riseup.net>

 sci-mathematics/why3/why3-1.3.3.ebuild | 67 ++++++++++++++++++++++++++++++++++
 1 file changed, 67 insertions(+)

diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild
new file mode 100644
index 000000000..41c1f9b9f
--- /dev/null
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild
@@ -0,0 +1,67 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=7
+
+PYTHON_COMPAT=( python3_{7,8,9} )
+DOCS_BUILDER="sphinx"
+DOCS_DIR="doc"
+DOCS_DEPEND="
+	dev-python/sphinxcontrib-bibtex
+	dev-python/graphviz
+"
+
+inherit python-any-r1 docs
+
+DESCRIPTION="Why3 is a platform for deductive program verification"
+HOMEPAGE="http://why3.lri.fr/"
+SRC_URI="https://gforge.inria.fr/frs/download.php/file/38367/why3-1.3.3.tar.gz"
+
+LICENSE="LGPL-2"
+SLOT="0"
+KEYWORDS="~amd64"
+
+IUSE="float frama-c examples"
+
+DEPEND="
+	>=dev-lang/ocaml-3.12.1
+	dev-ml/zarith
+	dev-ml/menhir
+	dev-ml/num
+	sci-mathematics/coq
+	frama-c? ( >=sci-mathematics/frama-c-20140301 )
+	float? ( sci-mathematics/flocq )
+"
+RDEPEND="${DEPEND}"
+
+src_prepare() {
+	default
+	mv doc/why.1 doc/why3.1 || die
+	sed -i configure.in -e "s/\"pvs\"/\"sri-pvs\"/g" || die
+	sed -i configure -e "s/\"pvs\"/\"sri-pvs\"/g" || die
+	# fix dev-ml/num path
+	sed -i configure.in -e "s/nums.cma/num.cma/g" -e "s/num.cmi/core\/num.cmi/g" || die
+	sed -i configure -e "s/nums.cma/num.cma/g" -e "s/num.cmi/core\/num.cmi/g" || die
+	sed -i Makefile.in -e "s:DESTDIR =::g" \
+		-e "s:\$(RUBBER) --warn all --pdf manual.tex:makeindex manual.tex; \$(RUBBER) --warn all --pdf manual.tex; cd ..:g" || die
+	# add autodoc to sphinx
+	sed -i -e "/^extensions = \[/a \ \ \ \ \'sphinx.ext.autodoc\'," doc/conf.py || die
+}
+
+src_configure() {
+	econf $(use_enable frama-c)
+}
+
+src_compile() {
+	docs_compile
+	default
+}
+
+src_install(){
+	default
+
+	if use examples; then
+		insinto /usr/share/doc/${PF}
+		doins -r examples
+	fi
+}

[gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/

[Marius Brehler]

commit:     51abf617505aeccd1d7c9e866e206563d71ad3d0
Author:     Marius Brehler <marbre <AT> linux <DOT> sungazer <DOT> de>
AuthorDate: Wed Jun 15 14:55:40 2016 +0000
Commit:     Marius Brehler <marbre <AT> linux <DOT> sungazer <DOT> de>
CommitDate: Wed Jun 15 14:55:40 2016 +0000
URL:        https://gitweb.gentoo.org/proj/sci.git/commit/?id=51abf617

sci-mathematics/why3: Drop ~x86 keyword

Package-Manager: portage-2.2.28

 sci-mathematics/why3/why3-0.83.ebuild | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/why3/why3-0.83.ebuild b/sci-mathematics/why3/why3-0.83.ebuild
index b07bcc3..2b2643f 100644
--- a/sci-mathematics/why3/why3-0.83.ebuild
+++ b/sci-mathematics/why3/why3-0.83.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2015 Gentoo Foundation
+# Copyright 1999-2016 Gentoo Foundation
 # Distributed under the terms of the GNU General Public License v2
 # $Id$
 
@@ -12,7 +12,7 @@ SRC_URI="https://gforge.inria.fr/frs/download.php/33490/${P}.tar.gz"
 
 LICENSE="LGPL-2"
 SLOT="0"
-KEYWORDS="~amd64 ~x86"
+KEYWORDS="~amd64"
 IUSE="float frama-c doc examples"
 
 DEPEND=">=dev-lang/ocaml-3.12.1

[gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/

[Christoph Junghans]

commit:     c901a3e918a37be894738ac50ba0b12752916903
Author:     Marius Brehler <marbre <AT> linux <DOT> sungazer <DOT> de>
AuthorDate: Sun Feb  8 10:04:11 2015 +0000
Commit:     Christoph Junghans <ottxor <AT> gentoo <DOT> org>
CommitDate: Sun Feb  8 10:04:11 2015 +0000
URL:        http://sources.gentoo.org/gitweb/?p=proj/sci.git;a=commit;h=c901a3e9

sci-mathematics/why3-0.83: Cleanup ebuild

---
 sci-mathematics/why3/ChangeLog        |  6 +++++-
 sci-mathematics/why3/why3-0.83.ebuild | 28 ++++++++++++++++------------
 2 files changed, 21 insertions(+), 13 deletions(-)

diff --git a/sci-mathematics/why3/ChangeLog b/sci-mathematics/why3/ChangeLog
index 5fa385d..e50e10d 100644
--- a/sci-mathematics/why3/ChangeLog
+++ b/sci-mathematics/why3/ChangeLog
@@ -1,7 +1,11 @@
 # ChangeLog for sci-mathematics/why3
-# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
+# Copyright 1999-2015 Gentoo Foundation; Distributed under the GPL v2
 # $Header: $
 
+  08 Feb 2015; Marius Brehler <marbre@linux.sungazer.de>
+  why3-0.83.ebuild:
+  Cleanup ebuild
+
   16 Sep 2014; Christoph Junghans <ottxor@gentoo.org> why3-0.83.ebuild:
   drop autotools.eclass
 

diff --git a/sci-mathematics/why3/why3-0.83.ebuild b/sci-mathematics/why3/why3-0.83.ebuild
index 61ceaed..1abb3d5 100644
--- a/sci-mathematics/why3/why3-0.83.ebuild
+++ b/sci-mathematics/why3/why3-0.83.ebuild
@@ -1,8 +1,8 @@
-# Copyright 1999-2014 Gentoo Foundation
+# Copyright 1999-2015 Gentoo Foundation
 # Distributed under the terms of the GNU General Public License v2
 # $Header: $
 
-EAPI="5"
+EAPI=5
 
 inherit eutils
 
@@ -23,28 +23,32 @@ DEPEND=">=dev-lang/ocaml-3.12.1
 		doc? ( dev-tex/rubber )"
 RDEPEND="${DEPEND}"
 
+DOCS=( CHANGES README Version )
+
 src_prepare() {
-	mv doc/why.1 doc/why3.1
-	sed -i configure.in -e "s/\"pvs\"/\"sri-pvs\"/g"
-	sed -i configure -e "s/\"pvs\"/\"sri-pvs\"/g"
+	mv doc/why.1 doc/why3.1 || die
+	sed -i configure.in -e "s/\"pvs\"/\"sri-pvs\"/g" || die
+	sed -i configure -e "s/\"pvs\"/\"sri-pvs\"/g" || die
 	sed -i Makefile.in -e "s:DESTDIR =::g" \
-		-e "s:\$(RUBBER) --warn all --pdf manual.tex:makeindex manual.tex; \$(RUBBER) --warn all --pdf manual.tex; cd ..:g"
+		-e "s:\$(RUBBER) --warn all --pdf manual.tex:makeindex manual.tex; \$(RUBBER) --warn all --pdf manual.tex; cd ..:g" || die
 }
 
 src_configure() {
-	econf $(use_enable frama-c) || die "econf failed"
+	econf $(use_enable frama-c)
 }
 
 src_compile() {
-	emake -j1 || die "emake failed"
+	MAKEOPTS+=" -j1"
+
+	emake
 	if use doc; then
-		emake -j1 doc/manual.pdf || die "emake doc failed"
+		emake doc/manual.pdf
 	fi
 }
 
 src_install(){
-	emake install DESTDIR="${D}" || die "emake install failed"
-	dodoc CHANGES README Version
+	default
+
 	doman doc/why3.1
 	if use doc; then
 		dodoc doc/manual.pdf
@@ -53,4 +57,4 @@ src_install(){
 		insinto /usr/share/doc/${PF}
 		doins -r examples
 	fi
-	}
+}

[gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/

[Christoph Junghans]

commit:     87a518c55c7376f2ef9d0e13487a1e81b74eb977
Author:     Christoph Junghans <ottxor <AT> gentoo <DOT> org>
AuthorDate: Tue Sep 16 03:34:14 2014 +0000
Commit:     Christoph Junghans <ottxor <AT> gentoo <DOT> org>
CommitDate: Tue Sep 16 03:34:14 2014 +0000
URL:        http://sources.gentoo.org/gitweb/?p=proj/sci.git;a=commit;h=87a518c5

drop autotools.eclass

Package-Manager: portage-2.2.8-r1

---
 sci-mathematics/why3/ChangeLog        | 3 +++
 sci-mathematics/why3/why3-0.83.ebuild | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/sci-mathematics/why3/ChangeLog b/sci-mathematics/why3/ChangeLog
index a91bee8..5fa385d 100644
--- a/sci-mathematics/why3/ChangeLog
+++ b/sci-mathematics/why3/ChangeLog
@@ -2,6 +2,9 @@
 # Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2
 # $Header: $
 
+  16 Sep 2014; Christoph Junghans <ottxor@gentoo.org> why3-0.83.ebuild:
+  drop autotools.eclass
+
   21 Jun 2014; Jonathan-Christofer Demay <jcdemay@gmail.com>
   +ChangeLog, +metadata.xml, +why3-0.83.ebuild:
   initial version

diff --git a/sci-mathematics/why3/why3-0.83.ebuild b/sci-mathematics/why3/why3-0.83.ebuild
index 0f92282..61ceaed 100644
--- a/sci-mathematics/why3/why3-0.83.ebuild
+++ b/sci-mathematics/why3/why3-0.83.ebuild
@@ -4,7 +4,7 @@
 
 EAPI="5"
 
-inherit autotools eutils
+inherit eutils
 
 DESCRIPTION=" Why3 is a platform for deductive program verification"
 HOMEPAGE="http://why3.lri.fr/"

[gentoo-commits] proj/sci:master commit in: sci-mathematics/why3/

[Jauhien Piatlicki]

commit:     637e6ccd3529b1d3c9c69d192426315c17a3cbe8
Author:     Jauhien Piatlicki <jauhien <AT> gentoo <DOT> org>
AuthorDate: Tue Sep  2 20:43:43 2014 +0000
Commit:     Jauhien Piatlicki <jauhien <AT> gentoo <DOT> org>
CommitDate: Tue Sep  2 20:43:43 2014 +0000
URL:        http://sources.gentoo.org/gitweb/?p=proj/sci.git;a=commit;h=637e6ccd

sci-mathematics/why3: silence repoman, fix metadata.xml

---
 sci-mathematics/why3/metadata.xml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml
index 17c0a90..b116328 100644
--- a/sci-mathematics/why3/metadata.xml
+++ b/sci-mathematics/why3/metadata.xml
@@ -14,4 +14,8 @@
   automated extraction mechanism. WhyML is also used as an intermediate
   language for the verification of C, Java, or Ada programs.
 </longdescription>
+<use>
+  <flag name='float'>Add <pkg>sci-mathematics/flocq</pkg> support</flag>
+  <flag name='frama-c'>Enable Frama-C plugin</flag>
+</use>
 </pkgmetadata>