summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTupone Alfredo <tupone@gentoo.org>2017-10-20 07:48:20 +0200
committerTupone Alfredo <tupone@gentoo.org>2017-10-20 07:48:20 +0200
commitcb97b25bd87da46462a3d73b4d5bcda6cc13f2e1 (patch)
treea4274a35d52bf6b4db817bb30319944a16645800 /sci-mathematics
parentsys-apps/portage: version bump to 2.3.12 (diff)
downloadgentoo-cb97b25bd87da46462a3d73b4d5bcda6cc13f2e1.tar.gz
gentoo-cb97b25bd87da46462a3d73b4d5bcda6cc13f2e1.tar.bz2
gentoo-cb97b25bd87da46462a3d73b4d5bcda6cc13f2e1.zip
sci-mathematics/why3-for-spark: Fix metadata.xml
Package-Manager: Portage-2.3.8, Repoman-2.3.3
Diffstat (limited to 'sci-mathematics')
-rw-r--r--sci-mathematics/why3-for-spark/metadata.xml46
1 files changed, 23 insertions, 23 deletions
diff --git a/sci-mathematics/why3-for-spark/metadata.xml b/sci-mathematics/why3-for-spark/metadata.xml
index 6dbb21558b6c..f73ffa40b698 100644
--- a/sci-mathematics/why3-for-spark/metadata.xml
+++ b/sci-mathematics/why3-for-spark/metadata.xml
@@ -1,27 +1,27 @@
<?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="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="profiling">Enable profiling</flag>
- <flag name="zarith">Use <pkg>dev-ml/zarith</pkg></flag>
-</use>
+ <maintainer type="person">
+ <email>tupone@gentoo.org</email>
+ <name>Tupone Alfredo</name>
+ </maintainer>
+ <longdescription lang="en">
+ 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="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="profiling">Enable profiling</flag>
+ <flag name="zarith">Use <pkg>dev-ml/zarith</pkg></flag>
+ </use>
</pkgmetadata>