| 1 |
commit: cb97b25bd87da46462a3d73b4d5bcda6cc13f2e1 |
| 2 |
Author: Tupone Alfredo <tupone <AT> gentoo <DOT> org> |
| 3 |
AuthorDate: Fri Oct 20 05:48:20 2017 +0000 |
| 4 |
Commit: Alfredo Tupone <tupone <AT> gentoo <DOT> org> |
| 5 |
CommitDate: Fri Oct 20 05:48:20 2017 +0000 |
| 6 |
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=cb97b25b |
| 7 |
|
| 8 |
sci-mathematics/why3-for-spark: Fix metadata.xml |
| 9 |
|
| 10 |
Package-Manager: Portage-2.3.8, Repoman-2.3.3 |
| 11 |
|
| 12 |
sci-mathematics/why3-for-spark/metadata.xml | 46 ++++++++++++++--------------- |
| 13 |
1 file changed, 23 insertions(+), 23 deletions(-) |
| 14 |
|
| 15 |
diff --git a/sci-mathematics/why3-for-spark/metadata.xml b/sci-mathematics/why3-for-spark/metadata.xml |
| 16 |
index 6dbb21558b6..f73ffa40b69 100644 |
| 17 |
--- a/sci-mathematics/why3-for-spark/metadata.xml |
| 18 |
+++ b/sci-mathematics/why3-for-spark/metadata.xml |
| 19 |
@@ -1,27 +1,27 @@ |
| 20 |
<?xml version="1.0" encoding="UTF-8"?> |
| 21 |
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> |
| 22 |
<pkgmetadata> |
| 23 |
-<maintainer type="project"> |
| 24 |
- <email>sci-mathematics@g.o</email> |
| 25 |
- <name>Gentoo Mathematics Project</name> |
| 26 |
-</maintainer> |
| 27 |
-<longdescription> |
| 28 |
- Why3 is a platform for deductive program verification. It provides |
| 29 |
- a rich language for specification and programming, called WhyML, |
| 30 |
- and relies on external theorem provers, both automated and interactive, |
| 31 |
- to discharge verification conditions. Why3 comes with a standard |
| 32 |
- library of logical theories (integer and real arithmetic, Boolean |
| 33 |
- operations, sets and maps, etc.) and basic programming data structures |
| 34 |
- (arrays, queues, hash tables, etc.). A user can write WhyML programs |
| 35 |
- directly and get correct-by-construction OCaml programs through an |
| 36 |
- automated extraction mechanism. WhyML is also used as an intermediate |
| 37 |
- language for the verification of C, Java, or Ada programs. |
| 38 |
-</longdescription> |
| 39 |
-<use> |
| 40 |
- <flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag> |
| 41 |
- <flag name="html">Build HTML documentation</flag> |
| 42 |
- <flag name="hypothesis-selection">Enable hypothesis selection</flag> |
| 43 |
- <flag name="profiling">Enable profiling</flag> |
| 44 |
- <flag name="zarith">Use <pkg>dev-ml/zarith</pkg></flag> |
| 45 |
-</use> |
| 46 |
+ <maintainer type="person"> |
| 47 |
+ <email>tupone@g.o</email> |
| 48 |
+ <name>Tupone Alfredo</name> |
| 49 |
+ </maintainer> |
| 50 |
+ <longdescription lang="en"> |
| 51 |
+ Why3 is a platform for deductive program verification. It provides a |
| 52 |
+ rich language for specification and programming, called WhyML, and |
| 53 |
+ relies on external theorem provers, both automated and interactive, to |
| 54 |
+ discharge verification conditions. Why3 comes with a standard library |
| 55 |
+ of logical theories (integer and real arithmetic, Boolean operations, |
| 56 |
+ sets and maps, etc.) and basic programming data structures (arrays, |
| 57 |
+ queues, hash tables, etc.). A user can write WhyML programs directly |
| 58 |
+ and get correct-by-construction OCaml programs through an automated |
| 59 |
+ extraction mechanism. WhyML is also used as an intermediate language |
| 60 |
+ for the verification of C, Java, or Ada programs. |
| 61 |
+ </longdescription> |
| 62 |
+ <use> |
| 63 |
+ <flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag> |
| 64 |
+ <flag name="html">Build HTML documentation</flag> |
| 65 |
+ <flag name="hypothesis-selection">Enable hypothesis selection</flag> |
| 66 |
+ <flag name="profiling">Enable profiling</flag> |
| 67 |
+ <flag name="zarith">Use <pkg>dev-ml/zarith</pkg></flag> |
| 68 |
+ </use> |
| 69 |
</pkgmetadata> |
Archives