1 |
jlec 14/01/23 08:17:49 |
2 |
|
3 |
Modified: coq-8.3_p1.ebuild coq-8.4_p1.ebuild metadata.xml |
4 |
coq-8.4_p2.ebuild ChangeLog |
5 |
Added: coq-8.4_p3.ebuild |
6 |
Log: |
7 |
sci-mathematics/coq: Version Bump, fixes problems with make-4, #493144 |
8 |
|
9 |
(Portage version: 2.2.8-r1/cvs/Linux x86_64, signed Manifest commit with key B9D4F231BD1558AB!) |
10 |
|
11 |
Revision Changes Path |
12 |
1.7 sci-mathematics/coq/coq-8.3_p1.ebuild |
13 |
|
14 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.3_p1.ebuild?rev=1.7&view=markup |
15 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.3_p1.ebuild?rev=1.7&content-type=text/plain |
16 |
diff : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.3_p1.ebuild?r1=1.6&r2=1.7 |
17 |
|
18 |
Index: coq-8.3_p1.ebuild |
19 |
=================================================================== |
20 |
RCS file: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.3_p1.ebuild,v |
21 |
retrieving revision 1.6 |
22 |
retrieving revision 1.7 |
23 |
diff -u -r1.6 -r1.7 |
24 |
--- coq-8.3_p1.ebuild 5 Oct 2011 18:54:43 -0000 1.6 |
25 |
+++ coq-8.3_p1.ebuild 23 Jan 2014 08:17:49 -0000 1.7 |
26 |
@@ -1,6 +1,6 @@ |
27 |
-# Copyright 1999-2011 Gentoo Foundation |
28 |
+# Copyright 1999-2014 Gentoo Foundation |
29 |
# Distributed under the terms of the GNU General Public License v2 |
30 |
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.3_p1.ebuild,v 1.6 2011/10/05 18:54:43 aballier Exp $ |
31 |
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.3_p1.ebuild,v 1.7 2014/01/23 08:17:49 jlec Exp $ |
32 |
|
33 |
EAPI="2" |
34 |
|
35 |
@@ -9,7 +9,7 @@ |
36 |
MY_PV=${PV/_p/pl} |
37 |
MY_P=${PN}-${MY_PV} |
38 |
|
39 |
-DESCRIPTION="Coq is a proof assistant written in O'Caml" |
40 |
+DESCRIPTION="Proof assistant written in O'Caml" |
41 |
HOMEPAGE="http://coq.inria.fr/" |
42 |
SRC_URI="http://${PN}.inria.fr/V${MY_PV}/files/${MY_P}.tar.gz" |
43 |
|
44 |
|
45 |
|
46 |
|
47 |
1.6 sci-mathematics/coq/coq-8.4_p1.ebuild |
48 |
|
49 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.4_p1.ebuild?rev=1.6&view=markup |
50 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.4_p1.ebuild?rev=1.6&content-type=text/plain |
51 |
diff : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.4_p1.ebuild?r1=1.5&r2=1.6 |
52 |
|
53 |
Index: coq-8.4_p1.ebuild |
54 |
=================================================================== |
55 |
RCS file: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.4_p1.ebuild,v |
56 |
retrieving revision 1.5 |
57 |
retrieving revision 1.6 |
58 |
diff -u -r1.5 -r1.6 |
59 |
--- coq-8.4_p1.ebuild 19 Aug 2013 15:06:15 -0000 1.5 |
60 |
+++ coq-8.4_p1.ebuild 23 Jan 2014 08:17:49 -0000 1.6 |
61 |
@@ -1,6 +1,6 @@ |
62 |
-# Copyright 1999-2013 Gentoo Foundation |
63 |
+# Copyright 1999-2014 Gentoo Foundation |
64 |
# Distributed under the terms of the GNU General Public License v2 |
65 |
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.4_p1.ebuild,v 1.5 2013/08/19 15:06:15 aballier Exp $ |
66 |
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.4_p1.ebuild,v 1.6 2014/01/23 08:17:49 jlec Exp $ |
67 |
|
68 |
EAPI="5" |
69 |
|
70 |
@@ -9,7 +9,7 @@ |
71 |
MY_PV=${PV/_p/pl} |
72 |
MY_P=${PN}-${MY_PV} |
73 |
|
74 |
-DESCRIPTION="Coq is a proof assistant written in O'Caml" |
75 |
+DESCRIPTION="Proof assistant written in O'Caml" |
76 |
HOMEPAGE="http://coq.inria.fr/" |
77 |
SRC_URI="http://${PN}.inria.fr/V${MY_PV}/files/${MY_P}.tar.gz" |
78 |
|
79 |
|
80 |
|
81 |
|
82 |
1.10 sci-mathematics/coq/metadata.xml |
83 |
|
84 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/metadata.xml?rev=1.10&view=markup |
85 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/metadata.xml?rev=1.10&content-type=text/plain |
86 |
diff : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/metadata.xml?r1=1.9&r2=1.10 |
87 |
|
88 |
Index: metadata.xml |
89 |
=================================================================== |
90 |
RCS file: /var/cvsroot/gentoo-x86/sci-mathematics/coq/metadata.xml,v |
91 |
retrieving revision 1.9 |
92 |
retrieving revision 1.10 |
93 |
diff -u -r1.9 -r1.10 |
94 |
--- metadata.xml 6 Oct 2012 21:07:26 -0000 1.9 |
95 |
+++ metadata.xml 23 Jan 2014 08:17:49 -0000 1.10 |
96 |
@@ -1,9 +1,9 @@ |
97 |
<?xml version="1.0" encoding="UTF-8"?> |
98 |
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd"> |
99 |
<pkgmetadata> |
100 |
-<herd>ml</herd> |
101 |
-<herd>sci-mathematics</herd> |
102 |
-<longdescription lang='en'> |
103 |
+ <herd>ml</herd> |
104 |
+ <herd>sci-mathematics</herd> |
105 |
+ <longdescription lang="en"> |
106 |
Developed in the LogiCal project, the Coq tool is a formal proof |
107 |
management system: a proof done with Coq is mechanically checked |
108 |
by the machine. |
109 |
@@ -16,7 +16,7 @@ |
110 |
Constructions" extended by a modular development system for |
111 |
theories. |
112 |
</longdescription> |
113 |
-<use> |
114 |
- <flag name='camlp5'>Build using camlp5. This is required for some plugins like Ssreflect.</flag> |
115 |
-</use> |
116 |
+ <use> |
117 |
+ <flag name="camlp5">Build using camlp5. This is required for some plugins like Ssreflect.</flag> |
118 |
+ </use> |
119 |
</pkgmetadata> |
120 |
|
121 |
|
122 |
|
123 |
1.3 sci-mathematics/coq/coq-8.4_p2.ebuild |
124 |
|
125 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.4_p2.ebuild?rev=1.3&view=markup |
126 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.4_p2.ebuild?rev=1.3&content-type=text/plain |
127 |
diff : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.4_p2.ebuild?r1=1.2&r2=1.3 |
128 |
|
129 |
Index: coq-8.4_p2.ebuild |
130 |
=================================================================== |
131 |
RCS file: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.4_p2.ebuild,v |
132 |
retrieving revision 1.2 |
133 |
retrieving revision 1.3 |
134 |
diff -u -r1.2 -r1.3 |
135 |
--- coq-8.4_p2.ebuild 19 Aug 2013 15:06:15 -0000 1.2 |
136 |
+++ coq-8.4_p2.ebuild 23 Jan 2014 08:17:49 -0000 1.3 |
137 |
@@ -1,6 +1,6 @@ |
138 |
-# Copyright 1999-2013 Gentoo Foundation |
139 |
+# Copyright 1999-2014 Gentoo Foundation |
140 |
# Distributed under the terms of the GNU General Public License v2 |
141 |
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.4_p2.ebuild,v 1.2 2013/08/19 15:06:15 aballier Exp $ |
142 |
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.4_p2.ebuild,v 1.3 2014/01/23 08:17:49 jlec Exp $ |
143 |
|
144 |
EAPI="5" |
145 |
|
146 |
@@ -9,7 +9,7 @@ |
147 |
MY_PV=${PV/_p/pl} |
148 |
MY_P=${PN}-${MY_PV} |
149 |
|
150 |
-DESCRIPTION="Coq is a proof assistant written in O'Caml" |
151 |
+DESCRIPTION="Proof assistant written in O'Caml" |
152 |
HOMEPAGE="http://coq.inria.fr/" |
153 |
SRC_URI="http://${PN}.inria.fr/V${MY_PV}/files/${MY_P}.tar.gz" |
154 |
|
155 |
@@ -18,7 +18,8 @@ |
156 |
KEYWORDS="~amd64 ~ppc ~x86" |
157 |
IUSE="gtk debug +ocamlopt doc camlp5" |
158 |
|
159 |
-RDEPEND=">=dev-lang/ocaml-3.11.2:=[ocamlopt?] |
160 |
+RDEPEND=" |
161 |
+ >=dev-lang/ocaml-3.11.2:=[ocamlopt?] |
162 |
camlp5? ( >=dev-ml/camlp5-6.02.3:=[ocamlopt?] ) |
163 |
gtk? ( >=dev-ml/lablgtk-2.10.1:=[ocamlopt?] )" |
164 |
DEPEND="${RDEPEND} |
165 |
@@ -66,11 +67,11 @@ |
166 |
} |
167 |
|
168 |
src_compile() { |
169 |
- emake STRIP="true" -j1 || die "make failed" |
170 |
+ emake STRIP="true" -j1 |
171 |
} |
172 |
|
173 |
src_install() { |
174 |
- emake STRIP="true" COQINSTALLPREFIX="${D}" install || die |
175 |
+ emake STRIP="true" COQINSTALLPREFIX="${D}" install |
176 |
dodoc README CREDITS CHANGES |
177 |
|
178 |
use gtk && make_desktop_entry "/usr/bin/coqide" "Coq IDE" "/usr/share/coq/coq.png" |
179 |
|
180 |
|
181 |
|
182 |
1.82 sci-mathematics/coq/ChangeLog |
183 |
|
184 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/ChangeLog?rev=1.82&view=markup |
185 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/ChangeLog?rev=1.82&content-type=text/plain |
186 |
diff : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/ChangeLog?r1=1.81&r2=1.82 |
187 |
|
188 |
Index: ChangeLog |
189 |
=================================================================== |
190 |
RCS file: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v |
191 |
retrieving revision 1.81 |
192 |
retrieving revision 1.82 |
193 |
diff -u -r1.81 -r1.82 |
194 |
--- ChangeLog 19 Aug 2013 15:06:15 -0000 1.81 |
195 |
+++ ChangeLog 23 Jan 2014 08:17:49 -0000 1.82 |
196 |
@@ -1,6 +1,12 @@ |
197 |
# ChangeLog for sci-mathematics/coq |
198 |
-# Copyright 1999-2013 Gentoo Foundation; Distributed under the GPL v2 |
199 |
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.81 2013/08/19 15:06:15 aballier Exp $ |
200 |
+# Copyright 1999-2014 Gentoo Foundation; Distributed under the GPL v2 |
201 |
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.82 2014/01/23 08:17:49 jlec Exp $ |
202 |
+ |
203 |
+*coq-8.4_p3 (23 Jan 2014) |
204 |
+ |
205 |
+ 23 Jan 2014; Justin Lecher <jlec@g.o> coq-8.3_p1.ebuild, |
206 |
+ coq-8.4_p1.ebuild, coq-8.4_p2.ebuild, +coq-8.4_p3.ebuild, metadata.xml: |
207 |
+ Version Bump, fixes problems with make-4, #493144 |
208 |
|
209 |
19 Aug 2013; Alexis Ballier <aballier@g.o> coq-8.4_p1.ebuild, |
210 |
coq-8.4_p2.ebuild: |
211 |
|
212 |
|
213 |
|
214 |
1.1 sci-mathematics/coq/coq-8.4_p3.ebuild |
215 |
|
216 |
file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.4_p3.ebuild?rev=1.1&view=markup |
217 |
plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/coq/coq-8.4_p3.ebuild?rev=1.1&content-type=text/plain |
218 |
|
219 |
Index: coq-8.4_p3.ebuild |
220 |
=================================================================== |
221 |
# Copyright 1999-2014 Gentoo Foundation |
222 |
# Distributed under the terms of the GNU General Public License v2 |
223 |
# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.4_p3.ebuild,v 1.1 2014/01/23 08:17:49 jlec Exp $ |
224 |
|
225 |
EAPI="5" |
226 |
|
227 |
inherit eutils multilib |
228 |
|
229 |
MY_PV=${PV/_p/pl} |
230 |
MY_P=${PN}-${MY_PV} |
231 |
|
232 |
DESCRIPTION="Proof assistant written in O'Caml" |
233 |
HOMEPAGE="http://coq.inria.fr/" |
234 |
SRC_URI="http://${PN}.inria.fr/V${MY_PV}/files/${MY_P}.tar.gz" |
235 |
|
236 |
LICENSE="LGPL-2.1" |
237 |
SLOT="0" |
238 |
KEYWORDS="~amd64 ~ppc ~x86" |
239 |
IUSE="gtk debug +ocamlopt doc camlp5" |
240 |
|
241 |
RDEPEND=" |
242 |
>=dev-lang/ocaml-3.11.2:=[ocamlopt?] |
243 |
camlp5? ( >=dev-ml/camlp5-6.02.3:=[ocamlopt?] ) |
244 |
gtk? ( >=dev-ml/lablgtk-2.10.1:=[ocamlopt?] )" |
245 |
DEPEND="${RDEPEND} |
246 |
doc? ( |
247 |
media-libs/netpbm[png,zlib] |
248 |
virtual/latex-base |
249 |
dev-tex/hevea |
250 |
dev-tex/xcolor |
251 |
dev-texlive/texlive-pictures |
252 |
dev-texlive/texlive-mathextra |
253 |
dev-texlive/texlive-latexextra |
254 |
)" |
255 |
|
256 |
S=${WORKDIR}/${MY_P} |
257 |
|
258 |
src_configure() { |
259 |
ocaml_lib=$(ocamlc -where) |
260 |
local myconf=( |
261 |
--prefix /usr |
262 |
--bindir /usr/bin |
263 |
--libdir /usr/$(get_libdir)/coq |
264 |
--mandir /usr/share/man |
265 |
--emacslib /usr/share/emacs/site-lisp |
266 |
--coqdocdir /usr/$(get_libdir)/coq/coqdoc |
267 |
--docdir /usr/share/doc/${PF} |
268 |
--configdir /etc/xdg/${PN} |
269 |
--lablgtkdir ${ocaml_lib}/lablgtk2 |
270 |
) |
271 |
|
272 |
use debug && myconf+=( --debug ) |
273 |
use doc || myconf+=( --with-doc no ) |
274 |
|
275 |
if use gtk; then |
276 |
if use ocamlopt; then |
277 |
myconf+=( --coqide opt ) |
278 |
else |
279 |
myconf+=( --coqide byte ) |
280 |
fi |
281 |
else |
282 |
myconf+=( --coqide no ) |
283 |
fi |
284 |
|
285 |
if use ocamlopt; then |
286 |
myconf+=( --opt ) |
287 |
else |
288 |
myconf+=( -byte-only ) |
289 |
fi |
290 |
|
291 |
if use camlp5; then |
292 |
myconf+=( --camlp5dir ${ocaml_lib}/camlp5 ) |
293 |
else |
294 |
myconf+=( --usecamlp4 ) |
295 |
fi |
296 |
|
297 |
export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/" |
298 |
./configure ${myconf[@]} || die "configure failed" |
299 |
} |
300 |
|
301 |
src_compile() { |
302 |
emake STRIP="true" -j1 |
303 |
} |
304 |
|
305 |
src_install() { |
306 |
emake STRIP="true" COQINSTALLPREFIX="${D}" install |
307 |
dodoc README CREDITS CHANGES |
308 |
|
309 |
use gtk && make_desktop_entry "coqide" "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png" |
310 |
} |