1 |
commit: fa8a6b65b706ccd8cd58fe0d9d3bd0b6d00a610b |
2 |
Author: Alfredo Tupone <tupone <AT> gentoo <DOT> org> |
3 |
AuthorDate: Sat Jun 12 18:51:19 2021 +0000 |
4 |
Commit: Alfredo Tupone <tupone <AT> gentoo <DOT> org> |
5 |
CommitDate: Sat Jun 12 18:51:46 2021 +0000 |
6 |
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=fa8a6b65 |
7 |
|
8 |
sci-mathematics/why3-for-spark: version bump to 2021 |
9 |
|
10 |
Package-Manager: Portage-3.0.18, Repoman-3.0.2 |
11 |
Signed-off-by: Alfredo Tupone <tupone <AT> gentoo.org> |
12 |
|
13 |
sci-mathematics/why3-for-spark/Manifest | 1 + |
14 |
.../files/why3-for-spark-2021-flags.patch | 28 +++++ |
15 |
.../why3-for-spark/why3-for-spark-2021.ebuild | 123 +++++++++++++++++++++ |
16 |
3 files changed, 152 insertions(+) |
17 |
|
18 |
diff --git a/sci-mathematics/why3-for-spark/Manifest b/sci-mathematics/why3-for-spark/Manifest |
19 |
index 470f4f0fce2..a15aa4d6feb 100644 |
20 |
--- a/sci-mathematics/why3-for-spark/Manifest |
21 |
+++ b/sci-mathematics/why3-for-spark/Manifest |
22 |
@@ -1,3 +1,4 @@ |
23 |
DIST 8bb5801e17b8b23453262da69c981c091959eec7?filename=why3-2020-20200429-199EF-src.tar.gz 9739066 BLAKE2B c7c11a92d4926f90be9ffa94d74e65ad78423953b53ee617565ccfcea4a5a60b251367b0712c30d170ab717d5868f7d95d62694f38c3d2f52805a28a6522ab8a SHA512 61cd5509957230ff81186d2507b9749b182cdc44698f6658337ce294d210742e57164d25d7c0eb3eb5ea0c53f5f46dea099e6a0769fadcb709a5a8557ed3cae3 |
24 |
DIST why3-2019-20190517-197BB-src.tar.gz 9439414 BLAKE2B 68072064e8ee9152528c90afc948047a1f4d58b960ac05b276761fdca5ba1204100c75f33db7bb0ea1a8a646b734e62892ed41bd875b954354f52b8f9d498d4a SHA512 9169a4ff9ee994a19f9f04b689d1b9c679f5340bcd631d7d49b4c55064f505bd5a6ca8149077e5d24d36f5365f0cab58587094e86f352a9105fc46f10c0746ba |
25 |
+DIST why3-2021-20210519-19ADF-src.tar.gz 10386938 BLAKE2B 93b6323c562126244f5cccef34088a521fe3dc1cec07c966e94472503ec8492707b20a641936449307f0439e711a82260d36679cbc69f53df8e7886a1d3673c3 SHA512 65e3c1430001962f2c7cce786f3e30f14b5295cff89c4087d95c1545e81743723319ba0309dbe15c4c46552110b25ff57addc3ee085dade02ea59a2273b127db |
26 |
DIST why3-for-spark-gpl-2018-src.tar.gz 7682767 BLAKE2B 0b0272ca4d5519ca402990b234d0847378bcd2a0949fea78ea10e355233a16aebe79b938cdf8e4daadabb909171cab83b9d6ccacf9f2dc1c0b57bb6da6fd1fe0 SHA512 fc798acf343484fd8e70f470a318753c9a0e9967ff579f20ec185bf3c2a75e7a4a556388fc86a378610ce4a467f3e722c6f610da34d4c33bc3d6b10551731f07 |
27 |
|
28 |
diff --git a/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-flags.patch b/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-flags.patch |
29 |
new file mode 100644 |
30 |
index 00000000000..7f6dfd0f446 |
31 |
--- /dev/null |
32 |
+++ b/sci-mathematics/why3-for-spark/files/why3-for-spark-2021-flags.patch |
33 |
@@ -0,0 +1,28 @@ |
34 |
+--- a/Makefile.in 2020-06-12 21:03:33.375534124 +0200 |
35 |
++++ b/Makefile.in 2020-06-12 21:03:48.623283408 +0200 |
36 |
+@@ -127,7 +127,7 @@ |
37 |
+ |
38 |
+ WARNINGS = A-4-9-41-44-45-50-52@5@8@48 |
39 |
+ |
40 |
+-FLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -thread $(INCLUDES) |
41 |
++FLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -thread $(INCLUDES) -cclib "$(LDFLAGS)" -ccopt "$(CFLAGS)" |
42 |
+ OFLAGS = $(FLAGS) |
43 |
+ BFLAGS = $(FLAGS) |
44 |
+ |
45 |
+@@ -778,13 +778,13 @@ |
46 |
+ all: $(TOOLS) |
47 |
+ |
48 |
+ lib/why3server$(EXE): $(SERVER_O) |
49 |
+- $(CC) -Wall -o $@ $^ |
50 |
++ $(CC) -Wall $(CFLAGS) -o $@ $^ $(LDFLAGS) |
51 |
+ |
52 |
+ lib/why3cpulimit$(EXE): $(CPULIM_O) |
53 |
+- $(CC) -Wall -o $@ $^ |
54 |
++ $(CC) -Wall $(CFLAGS) -o $@ $^ $(LDFLAGS) |
55 |
+ |
56 |
+ %.o: %.c |
57 |
+- $(CC) -Wall -O -g -o $@ -c $< |
58 |
++ $(CC) -Wall $(CFLAGS) -O -g -o $@ -c $< |
59 |
+ |
60 |
+ uninstall-bin:: |
61 |
+ rm -f $(LIBDIR)/why3/why3server$(EXE) $(LIBDIR)/why3/why3cpulimit$(EXE) |
62 |
|
63 |
diff --git a/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild b/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild |
64 |
new file mode 100644 |
65 |
index 00000000000..04dd0ae9fcb |
66 |
--- /dev/null |
67 |
+++ b/sci-mathematics/why3-for-spark/why3-for-spark-2021.ebuild |
68 |
@@ -0,0 +1,123 @@ |
69 |
+# Copyright 1999-2021 Gentoo Authors |
70 |
+# Distributed under the terms of the GNU General Public License v2 |
71 |
+ |
72 |
+EAPI=7 |
73 |
+ |
74 |
+inherit autotools |
75 |
+ |
76 |
+ADAMIRROR=https://community.download.adacore.com/v1 |
77 |
+ID=dd74ae7ecfd7d56aff7b17cee7a35559384a600f |
78 |
+MYP=why3-${PV}-20210519-19ADF-src |
79 |
+ |
80 |
+DESCRIPTION="Platform for deductive program verification" |
81 |
+HOMEPAGE="http://why3.lri.fr/" |
82 |
+SRC_URI="${ADAMIRROR}/${ID}?filename=${MYP}.tar.gz -> ${MYP}.tar.gz" |
83 |
+ |
84 |
+LICENSE="GPL-3" |
85 |
+SLOT="0" |
86 |
+KEYWORDS="~amd64" |
87 |
+IUSE="coq doc emacs gtk html +ocamlopt zarith zip" |
88 |
+RESTRICT="strip" |
89 |
+ |
90 |
+DEPEND="dev-lang/ocaml:0/4.11[ocamlopt?] |
91 |
+ dev-ml/menhir:= |
92 |
+ dev-ml/num:= |
93 |
+ dev-ml/yojson:= |
94 |
+ coq? ( |
95 |
+ sci-mathematics/coq |
96 |
+ ) |
97 |
+ doc? ( |
98 |
+ dev-tex/rubber |
99 |
+ dev-python/sphinx |
100 |
+ media-gfx/graphviz |
101 |
+ dev-python/sphinxcontrib-bibtex |
102 |
+ ) |
103 |
+ gtk? ( dev-ml/lablgtk:=[sourceview] ) |
104 |
+ emacs? ( app-editors/emacs:* ) |
105 |
+ html? ( dev-tex/hevea:= ) |
106 |
+ zarith? ( dev-ml/zarith:= ) |
107 |
+ zip? ( dev-ml/camlzip:= )" |
108 |
+RDEPEND="${DEPEND}" |
109 |
+ |
110 |
+S="${WORKDIR}"/${MYP} |
111 |
+ |
112 |
+PATCHES=( |
113 |
+ "${FILESDIR}"/${PN}-2020-gentoo.patch |
114 |
+ "${FILESDIR}"/${P}-flags.patch |
115 |
+ "${FILESDIR}"/${PN}-2020-bibtex.patch |
116 |
+) |
117 |
+ |
118 |
+QA_FLAGS_IGNORED=( |
119 |
+ /usr/lib64/why3/commands/why3shell |
120 |
+ /usr/lib64/why3/commands/why3extract |
121 |
+ /usr/lib64/why3/commands/why3execute |
122 |
+ /usr/lib64/why3/commands/why3prove |
123 |
+ /usr/lib64/why3/commands/why3wc |
124 |
+ /usr/lib64/why3/commands/why3doc |
125 |
+ /usr/lib64/why3/commands/why3replay |
126 |
+ /usr/lib64/why3/commands/why3webserver |
127 |
+ /usr/lib64/why3/plugins/'.*'.cmxs |
128 |
+ /usr/lib64/ocaml/why3/why3.cmxs |
129 |
+ /usr/lib64/ocaml/why3/why3extract.cmxs |
130 |
+ /usr/bin/why3 |
131 |
+ /usr/bin/why3config |
132 |
+ /usr/bin/why3session |
133 |
+ /usr/bin/gnat_server |
134 |
+ /usr/bin/gnatwhy3 |
135 |
+ /usr/bin/why3realize |
136 |
+) |
137 |
+ |
138 |
+REQUIRED_USE="html? ( doc )" |
139 |
+ |
140 |
+src_prepare() { |
141 |
+ find examples -name \*gz | xargs gunzip |
142 |
+ default |
143 |
+ eautoreconf |
144 |
+} |
145 |
+ |
146 |
+src_configure() { |
147 |
+ econf \ |
148 |
+ --disable-pvs-libs \ |
149 |
+ --disable-isabelle-libs \ |
150 |
+ --enable-verbose-make \ |
151 |
+ $(use_enable coq coq-libs) \ |
152 |
+ $(use_enable doc) \ |
153 |
+ $(use_enable emacs emacs-compilation) \ |
154 |
+ $(use_enable gtk ide) \ |
155 |
+ $(use_enable html html-pdf) \ |
156 |
+ $(use_enable ocamlopt native-code) \ |
157 |
+ $(use_enable zarith) \ |
158 |
+ $(use_enable zip) |
159 |
+} |
160 |
+ |
161 |
+src_compile() { |
162 |
+ emake -j1 |
163 |
+ if use ocamlopt; then |
164 |
+ emake byte |
165 |
+ fi |
166 |
+ use doc && emake doc |
167 |
+} |
168 |
+ |
169 |
+src_install() { |
170 |
+ emake DESTDIR="${D}" -j1 install |
171 |
+ emake DESTDIR="${D}" -j1 install-lib |
172 |
+ emake DESTDIR="${D}" install_spark2014_dev |
173 |
+ local cmdPath=/usr/$(get_libdir)/why3/commands |
174 |
+ dosym ../why3server ${cmdPath}/why3server |
175 |
+ # Remove duplicated files |
176 |
+ for filename in config ide realize server session; do |
177 |
+ if [[ -e "${D}"${cmdPath}/why3${filename} ]]; then |
178 |
+ rm "${D}"${cmdPath}/why3${filename} |
179 |
+ dosym ../../../bin/why3${filename} ${cmdPath}/why3${filename} |
180 |
+ fi |
181 |
+ done |
182 |
+ rm "${D}"/usr/$(get_libdir)/why3/why3cpulimit |
183 |
+ dosym ../../bin/why3cpulimit /usr/$(get_libdir)/why3/why3cpulimit |
184 |
+ |
185 |
+ einstalldocs |
186 |
+ docompress -x /usr/share/doc/${PF}/examples |
187 |
+ dodoc -r examples |
188 |
+ if use doc; then |
189 |
+ use html && dodoc -r doc/html |
190 |
+ fi |
191 |
+} |