1 |
commit: 8774c3bacb82b878b97365d5c3c9764c1d38ae8a |
2 |
Author: François-Xavier Carton <fx.carton91 <AT> gmail <DOT> com> |
3 |
AuthorDate: Fri Nov 27 18:16:28 2020 +0000 |
4 |
Commit: Francois-Xavier Carton <fx.carton91 <AT> gmail <DOT> com> |
5 |
CommitDate: Sat Jan 9 16:44:42 2021 +0000 |
6 |
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=8774c3ba |
7 |
|
8 |
sci-mathematics/why3: new package |
9 |
|
10 |
This is a bump from the version in ::science. |
11 |
|
12 |
Signed-off-by: François-Xavier Carton <fx.carton91 <AT> gmail.com> |
13 |
|
14 |
sci-mathematics/why3/Manifest | 1 + |
15 |
sci-mathematics/why3/metadata.xml | 27 ++++++++++++ |
16 |
sci-mathematics/why3/why3-1.3.3.ebuild | 80 ++++++++++++++++++++++++++++++++++ |
17 |
3 files changed, 108 insertions(+) |
18 |
|
19 |
diff --git a/sci-mathematics/why3/Manifest b/sci-mathematics/why3/Manifest |
20 |
new file mode 100644 |
21 |
index 00000000..20a390e4 |
22 |
--- /dev/null |
23 |
+++ b/sci-mathematics/why3/Manifest |
24 |
@@ -0,0 +1 @@ |
25 |
+DIST why3-1.3.3.tar.gz 5807572 BLAKE2B b1a04e78010f841e217b9a81c096cadfa0cddabadbe81ef55c310a104668feb1e46cd50576a965a58c74658903d6d08f9fd348bd2064a79ac3b176548927bcbe SHA512 a2dc95691cea29bbd20843a05add3985f777085086b654b53566ecdb752ba892366da703e232c85d5e0237d0e59564527aed55f6ccae9118d49e5f2cf93a53ce |
26 |
|
27 |
diff --git a/sci-mathematics/why3/metadata.xml b/sci-mathematics/why3/metadata.xml |
28 |
new file mode 100644 |
29 |
index 00000000..444f26b5 |
30 |
--- /dev/null |
31 |
+++ b/sci-mathematics/why3/metadata.xml |
32 |
@@ -0,0 +1,27 @@ |
33 |
+<?xml version="1.0" encoding="UTF-8"?> |
34 |
+<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> |
35 |
+<pkgmetadata> |
36 |
+ <maintainer type="person"> |
37 |
+ <name>François-Xavier Carton</name> |
38 |
+ <email>fx.carton91@×××××.com</email> |
39 |
+ </maintainer> |
40 |
+ <longdescription> |
41 |
+Why3 is a platform for deductive program verification. It provides |
42 |
+a rich language for specification and programming, called WhyML, |
43 |
+and relies on external theorem provers, both automated and interactive, |
44 |
+to discharge verification conditions. Why3 comes with a standard |
45 |
+library of logical theories (integer and real arithmetic, Boolean |
46 |
+operations, sets and maps, etc.) and basic programming data structures |
47 |
+(arrays, queues, hash tables, etc.). A user can write WhyML programs |
48 |
+directly and get correct-by-construction OCaml programs through an |
49 |
+automated extraction mechanism. WhyML is also used as an intermediate |
50 |
+language for the verification of C, Java, or Ada programs. |
51 |
+</longdescription> |
52 |
+ <use> |
53 |
+ <flag name="coq">Add <pkg>sci-mathematics/coq</pkg> support</flag> |
54 |
+ <flag name="gtk">Build the IDE <pkg>x11-libs/gtk+</pkg></flag> |
55 |
+ <flag name="re">Use Re (<pkg>dev-ml/re</pkg>) instead of Str for regular expressions</flag> |
56 |
+ <flag name="zarith">Use Zarith (<pkg>dev-ml/zarith</pkg>) instead of Nums (<pkg>dev-ml/num</pkg>) for computations</flag> |
57 |
+ <flag name="zip">Enable compression of session files</flag> |
58 |
+ </use> |
59 |
+</pkgmetadata> |
60 |
|
61 |
diff --git a/sci-mathematics/why3/why3-1.3.3.ebuild b/sci-mathematics/why3/why3-1.3.3.ebuild |
62 |
new file mode 100644 |
63 |
index 00000000..b5665dc3 |
64 |
--- /dev/null |
65 |
+++ b/sci-mathematics/why3/why3-1.3.3.ebuild |
66 |
@@ -0,0 +1,80 @@ |
67 |
+# Copyright 1999-2020 Gentoo Authors |
68 |
+# Distributed under the terms of the GNU General Public License v2 |
69 |
+ |
70 |
+EAPI=7 |
71 |
+ |
72 |
+inherit autotools |
73 |
+ |
74 |
+DESCRIPTION="Platform for deductive program verification" |
75 |
+HOMEPAGE="http://why3.lri.fr/" |
76 |
+SRC_URI="https://gforge.inria.fr/frs/download.php/file/38367/${P}.tar.gz" |
77 |
+ |
78 |
+LICENSE="LGPL-2" |
79 |
+SLOT="0" |
80 |
+KEYWORDS="~amd64" |
81 |
+IUSE="coq emacs gtk +ocamlopt re +zarith zip" |
82 |
+ |
83 |
+DEPEND=">=dev-lang/ocaml-4.05.0[ocamlopt?] |
84 |
+ >=dev-ml/menhir-20151112 |
85 |
+ dev-ml/findlib |
86 |
+ dev-ml/num |
87 |
+ coq? ( >=sci-mathematics/coq-8.6 ) |
88 |
+ emacs? ( app-editors/emacs:* ) |
89 |
+ gtk? ( dev-ml/lablgtk:*[sourceview,ocamlopt?] ) |
90 |
+ re? ( dev-ml/re dev-ml/seq ) |
91 |
+ zarith? ( dev-ml/zarith ) |
92 |
+ zip? ( dev-ml/camlzip )" |
93 |
+RDEPEND="${DEPEND}" |
94 |
+ |
95 |
+# doc needs sphinxcontrib-bibtex which is currently not packaged |
96 |
+# doc? ( |
97 |
+# dev-python/sphinx |
98 |
+# dev-python/sphinxcontrib-bibtex |
99 |
+# || ( dev-texlive/texlive-latex dev-tex/latexmk dev-tex/rubber ) |
100 |
+# ) |
101 |
+ |
102 |
+DOCS=( CHANGES.md README.md ) |
103 |
+ |
104 |
+src_prepare() { |
105 |
+ mv doc/why.1 doc/why3.1 || die |
106 |
+ mv configure.in configure.ac || die |
107 |
+ sed -i 's/configure\.in/configure.ac/g' Makefile.in || die |
108 |
+ eautoreconf |
109 |
+ eapply_user |
110 |
+} |
111 |
+ |
112 |
+src_configure() { |
113 |
+ econf \ |
114 |
+ --disable-hypothesis-selection \ |
115 |
+ --disable-pvs-libs \ |
116 |
+ --disable-isabelle-libs \ |
117 |
+ --disable-frama-c \ |
118 |
+ --disable-web-ide \ |
119 |
+ --disable-doc \ |
120 |
+ $(use_enable coq coq-libs) \ |
121 |
+ $(use_enable emacs emacs-compilation) \ |
122 |
+ $(use_enable gtk ide) \ |
123 |
+ $(use_enable ocamlopt native-code) \ |
124 |
+ $(use_enable re) \ |
125 |
+ $(use_enable zarith) \ |
126 |
+ $(use_enable zip) |
127 |
+} |
128 |
+ |
129 |
+src_compile() { |
130 |
+ emake |
131 |
+ emake plugins |
132 |
+ #use doc && emake doc |
133 |
+} |
134 |
+ |
135 |
+src_install(){ |
136 |
+ emake install install-lib DESTDIR="${ED}" |
137 |
+ |
138 |
+ doman doc/why3.1 |
139 |
+ einstalldocs |
140 |
+ docompress -x /usr/share/doc/${PF}/examples |
141 |
+ dodoc -r examples |
142 |
+ #if use doc; then |
143 |
+ # dodoc doc/latex/manual.pdf |
144 |
+ # dodoc -r doc/html |
145 |
+ #fi |
146 |
+} |