summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlexis Ballier <aballier@gentoo.org>2008-01-03 17:41:59 +0000
committerAlexis Ballier <aballier@gentoo.org>2008-01-03 17:41:59 +0000
commit44e70e5132246a832d86e28c7c9299477d2e457c (patch)
tree3ae772e71e81689b55f40342f81bfddcfb0035fd /sci-mathematics
parentMarking cyrus-imap-dev-2.3.9 ppc64 for bug 201684 (diff)
downloadhistorical-44e70e5132246a832d86e28c7c9299477d2e457c.tar.gz
historical-44e70e5132246a832d86e28c7c9299477d2e457c.tar.bz2
historical-44e70e5132246a832d86e28c7c9299477d2e457c.zip
Add support for building without ocamlopt, import smimou's patches from debian to allow it. Fix desktop entry categories.
Package-Manager: portage-2.1.4_rc14
Diffstat (limited to 'sci-mathematics')
-rw-r--r--sci-mathematics/coq/ChangeLog10
-rw-r--r--sci-mathematics/coq/Manifest40
-rw-r--r--sci-mathematics/coq/coq-8.1_p3.ebuild36
-rw-r--r--sci-mathematics/coq/files/coq-8.1_p3-cmxa-install.dpatch23
-rw-r--r--sci-mathematics/coq/files/coq-8.1_p3-noocamlopt.patch13
-rw-r--r--sci-mathematics/coq/files/coqide.desktop2
6 files changed, 101 insertions, 23 deletions
diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog
index 282635095fe4..2ac2058a1870 100644
--- a/sci-mathematics/coq/ChangeLog
+++ b/sci-mathematics/coq/ChangeLog
@@ -1,6 +1,12 @@
# ChangeLog for sci-mathematics/coq
-# Copyright 2000-2007 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.23 2007/12/19 20:08:01 aballier Exp $
+# Copyright 2000-2008 Gentoo Foundation; Distributed under the GPL v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.24 2008/01/03 17:41:59 aballier Exp $
+
+ 03 Jan 2008; Alexis Ballier <aballier@gentoo.org>
+ +files/coq-8.1_p3-cmxa-install.dpatch, +files/coq-8.1_p3-noocamlopt.patch,
+ files/coqide.desktop, coq-8.1_p3.ebuild:
+ Add support for building without ocamlopt, import smimou's patches from
+ debian to allow it. Fix desktop entry categories.
19 Dec 2007; Alexis Ballier <aballier@gentoo.org> coq-8.1_p2.ebuild,
coq-8.1_p3.ebuild:
diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest
index e954a645fbbc..9dfe347c3655 100644
--- a/sci-mathematics/coq/Manifest
+++ b/sci-mathematics/coq/Manifest
@@ -1,10 +1,18 @@
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
-AUX coqide.desktop 242 RMD160 78d55202099015b63459b8d1366befc26dc0f259 SHA1 fefc588252399b33f34ff8a1f15bdcf13e5d4d0b SHA256 8444a5bdcf66303265c6fbaba67c0f1b6b06a97bd31929d91ca9742da6961a71
-MD5 e5491c930f8f944ed9c3590fdc8492c1 files/coqide.desktop 242
-RMD160 78d55202099015b63459b8d1366befc26dc0f259 files/coqide.desktop 242
-SHA256 8444a5bdcf66303265c6fbaba67c0f1b6b06a97bd31929d91ca9742da6961a71 files/coqide.desktop 242
+AUX coq-8.1_p3-cmxa-install.dpatch 782 RMD160 b3977ef5ba2acad230973cb0bfd350f644068105 SHA1 399d3e235744ddb2f40088f5d55e84e5aa2f260d SHA256 799cedbe003c9ff4becf46896f0a0971d160a8075c4979f8ba40577229b3223c
+MD5 8af37f492e015307524c531134391d74 files/coq-8.1_p3-cmxa-install.dpatch 782
+RMD160 b3977ef5ba2acad230973cb0bfd350f644068105 files/coq-8.1_p3-cmxa-install.dpatch 782
+SHA256 799cedbe003c9ff4becf46896f0a0971d160a8075c4979f8ba40577229b3223c files/coq-8.1_p3-cmxa-install.dpatch 782
+AUX coq-8.1_p3-noocamlopt.patch 640 RMD160 dce43c53544a7c4d3437841a89b53e4349627ceb SHA1 a149f74e58999a594b7119c9daab3931ab468920 SHA256 c831fa7ecd2eac30964b61e8f3fddc8f34020833eabeca665984776ccbceb8e6
+MD5 10c48cfefc9291b4b5fe138f76910fe6 files/coq-8.1_p3-noocamlopt.patch 640
+RMD160 dce43c53544a7c4d3437841a89b53e4349627ceb files/coq-8.1_p3-noocamlopt.patch 640
+SHA256 c831fa7ecd2eac30964b61e8f3fddc8f34020833eabeca665984776ccbceb8e6 files/coq-8.1_p3-noocamlopt.patch 640
+AUX coqide.desktop 233 RMD160 3f9d112d7f55454f72c42b427005b37971c6e928 SHA1 40571b86c25793e7d4e9bef80f637d7440b03704 SHA256 dba2e81a408ae51e187c2a164794f9505c4abfa0b92f47a44d0e9f96e2b6dfac
+MD5 5eb1768f9a170be4ff272ff0720e14c3 files/coqide.desktop 233
+RMD160 3f9d112d7f55454f72c42b427005b37971c6e928 files/coqide.desktop 233
+SHA256 dba2e81a408ae51e187c2a164794f9505c4abfa0b92f47a44d0e9f96e2b6dfac files/coqide.desktop 233
DIST coq-8.0_p3-ocaml-3.09.patch.gz 5256 RMD160 17dd484a71ddcf5724435ef7386db070b9840949 SHA1 cf270ee2002f3d0f14802fdfc84dbf2d09c5434e SHA256 6eacae4a27de43e5cef2ef8c5971f869bf0df291436aa1ac573fd8bf7ae698fc
DIST coq-8.0pl3-translator.tar.gz 233228 RMD160 7dd748ee5929faf93ca75bec94b443573405b0fe SHA1 4a62e60759c8bbbf454febc47da0c92a0e9f862e SHA256 78def7e2998526db8c5740580113802a821c31de65bb12a7c74c512f6a9328f7
DIST coq-8.0pl3.tar.gz 2309002 RMD160 925a65fdd0c96f4fe6082bc7bfb8483c83b5fea7 SHA1 b182f25b8e6591139281f7078d049aaa7f0408d8 SHA256 03d02b39873197f5365aad9bc2b917f4db234dcfd4bcff79febd8525770fb84c
@@ -23,14 +31,14 @@ EBUILD coq-8.1_p2.ebuild 1725 RMD160 148b357bf5ea699e22469a375ce6d3149ac75218 SH
MD5 0931e7f0be585a64a2a3defb96b7ab66 coq-8.1_p2.ebuild 1725
RMD160 148b357bf5ea699e22469a375ce6d3149ac75218 coq-8.1_p2.ebuild 1725
SHA256 328b25de69f8a2741b83bb3225c8c22ead842e307634c2f248432317d8b0d2ad coq-8.1_p2.ebuild 1725
-EBUILD coq-8.1_p3.ebuild 1725 RMD160 4f2d42d2cb2f9449d638e808bf4dce387613044f SHA1 ef5feb43d194e9c1ac1fc584103ec749491cbc12 SHA256 514aa85ad44baaddbc205c7905cfcdd27048e4908d8b67827eab0bc2542610f1
-MD5 c3bbc4a95facc64b5cb3bdb3d0f69c08 coq-8.1_p3.ebuild 1725
-RMD160 4f2d42d2cb2f9449d638e808bf4dce387613044f coq-8.1_p3.ebuild 1725
-SHA256 514aa85ad44baaddbc205c7905cfcdd27048e4908d8b67827eab0bc2542610f1 coq-8.1_p3.ebuild 1725
-MISC ChangeLog 4841 RMD160 3c52002aaab02e1837c4445148dfa1e5eb1fe4ae SHA1 4fea83d1e8c5b87729f0997817c37e9a45a7f5c9 SHA256 94f0bf3dcfa38d242eb7ad5d4fc9d747f045b5a4a72df4dab8a9f64626b0cc1c
-MD5 297d4206b69dcc2517b892d343ace1ad ChangeLog 4841
-RMD160 3c52002aaab02e1837c4445148dfa1e5eb1fe4ae ChangeLog 4841
-SHA256 94f0bf3dcfa38d242eb7ad5d4fc9d747f045b5a4a72df4dab8a9f64626b0cc1c ChangeLog 4841
+EBUILD coq-8.1_p3.ebuild 2534 RMD160 61cf5893ba0b004f3e171609a06f7b446eafcf1f SHA1 c8e80117ccfef9aa6495aee4cfa648ded23d2ebd SHA256 b257293c5f408b7fbd1336a86d17be86c0c577eea40baba3ccb580177663bba6
+MD5 5b973ba1d4b34f082b1358225a28a7aa coq-8.1_p3.ebuild 2534
+RMD160 61cf5893ba0b004f3e171609a06f7b446eafcf1f coq-8.1_p3.ebuild 2534
+SHA256 b257293c5f408b7fbd1336a86d17be86c0c577eea40baba3ccb580177663bba6 coq-8.1_p3.ebuild 2534
+MISC ChangeLog 5140 RMD160 29e77f17a7a411d3683f0ac85503d81e49a010ee SHA1 1dcfde3a7c5c6aea3239ff39da677af3dfa7329e SHA256 c8308733581fcaef63c02503a79ef9d5d3168e7c035d6b9796ac031dbf73bcb1
+MD5 4b28601189d768931bf44d5a99d2cd0f ChangeLog 5140
+RMD160 29e77f17a7a411d3683f0ac85503d81e49a010ee ChangeLog 5140
+SHA256 c8308733581fcaef63c02503a79ef9d5d3168e7c035d6b9796ac031dbf73bcb1 ChangeLog 5140
MISC metadata.xml 174 RMD160 b6d9f7a487e305c44a47ffaa8d982731b5825a19 SHA1 70e63d5e68a5449b129f8f91f2554e8406e212a0 SHA256 3c931940a18c0692dd36b609c3026ce41dcde08cdc9e2d0d7bc0a0cf774e8c5b
MD5 587dfb99f9b1ef3ef6a79733b24811cc metadata.xml 174
RMD160 b6d9f7a487e305c44a47ffaa8d982731b5825a19 metadata.xml 174
@@ -48,9 +56,9 @@ MD5 ee73692d684c6e166f565e21e48cbb84 files/digest-coq-8.1_p3 235
RMD160 f3768c38ca8e57dcf832134a54d7e778858781dc files/digest-coq-8.1_p3 235
SHA256 73bd61ecaed8280418c5ffe57c15b20f1cb66ccfb78630fb9c87c30e2a4a8fe6 files/digest-coq-8.1_p3 235
-----BEGIN PGP SIGNATURE-----
-Version: GnuPG v2.0.7 (GNU/Linux)
+Version: GnuPG v2.0.8 (GNU/Linux)
-iD8DBQFHaXotvFcC4BYPU0oRAgxXAJwORvHIV5J8CS3oOEcSisnmicEsjACgmO6V
-BlozLVwRarZy3uFWSnPPtD4=
-=asbp
+iEYEARECAAYFAkd9HnAACgkQvFcC4BYPU0oMmgCfROy66YJLklD2LJuOYEQwfKWj
+tvsAoJIzczLeqoi+UfEwA/ElPJl+kzEk
+=obFY
-----END PGP SIGNATURE-----
diff --git a/sci-mathematics/coq/coq-8.1_p3.ebuild b/sci-mathematics/coq/coq-8.1_p3.ebuild
index a18a2d63d89c..3c0425b31247 100644
--- a/sci-mathematics/coq/coq-8.1_p3.ebuild
+++ b/sci-mathematics/coq/coq-8.1_p3.ebuild
@@ -1,10 +1,12 @@
-# Copyright 1999-2007 Gentoo Foundation
+# Copyright 1999-2008 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.1_p3.ebuild,v 1.2 2007/12/19 20:08:01 aballier Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.1_p3.ebuild,v 1.3 2008/01/03 17:41:59 aballier Exp $
inherit eutils multilib
-IUSE="norealanalysis ide debug"
+EAPI="1"
+
+IUSE="norealanalysis ide debug +ocamlopt"
RESTRICT="strip"
@@ -25,6 +27,30 @@ ide? ( >=dev-ml/lablgtk-2.2.0 )"
S="${WORKDIR}/${MY_P}"
+coq_need_ocamlopt() {
+ if use ocamlopt && ! built_with_use --missing true $1 ocamlopt; then
+ eerror "In order to build ${PN} with native code support from ocaml"
+ eerror "You first need to have a native code ocaml compiler and the related libraries."
+ eerror "You need to install $1 with ocamlopt useflag on."
+ die "Please install $1 with ocamlopt useflag"
+ fi
+}
+
+
+pkg_setup() {
+ coq_need_ocamlopt 'dev-lang/ocaml'
+ use ide && coq_need_ocamlopt 'dev-ml/lablgtk'
+ has_version '>=dev-lang/ocaml-3.10.0' && coq_need_ocamlopt 'dev-ml/camlp5'
+}
+
+src_unpack() {
+ unpack ${A}
+ cd "${S}"
+
+ epatch "${FILESDIR}/${P}-noocamlopt.patch"
+ epatch "${FILESDIR}/${P}-cmxa-install.dpatch"
+}
+
src_compile() {
local myconf="--prefix /usr \
--bindir /usr/bin \
@@ -38,10 +64,12 @@ src_compile() {
use norealanalysis || myconf="$myconf --reals all"
if use ide; then
- myconf="$myconf --coqide opt"
+ use ocamlopt && myconf="$myconf --coqide opt"
+ use ocamlopt || myconf="$myconf --coqide byte"
else
myconf="$myconf --coqide no"
fi
+ use ocamlopt || myconf="$myconf -byte-only"
./configure $myconf || die "configure failed"
diff --git a/sci-mathematics/coq/files/coq-8.1_p3-cmxa-install.dpatch b/sci-mathematics/coq/files/coq-8.1_p3-cmxa-install.dpatch
new file mode 100644
index 000000000000..7e8d2ffbb92e
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.1_p3-cmxa-install.dpatch
@@ -0,0 +1,23 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## cmxa-install.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: .cmxa are not generated on non-native archs, so don't install them.
+
+@DPATCH@
+diff -urNad coq-8.1+dfsg~/Makefile coq-8.1+dfsg/Makefile
+--- coq-8.1+dfsg~/Makefile 2007-02-18 13:25:29.000000000 +0100
++++ coq-8.1+dfsg/Makefile 2007-02-18 13:27:28.000000000 +0100
+@@ -1272,7 +1272,11 @@
+ parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
+ parsing/highparsing.cma tactics/hightactics.cma contrib/contrib.cma
+
+-OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
++ifeq ($(BEST),opt)
++ OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
++else
++ OBJECTCMXA=
++endif
+
+ install-library:
+ $(MKDIR) $(FULLCOQLIB)
diff --git a/sci-mathematics/coq/files/coq-8.1_p3-noocamlopt.patch b/sci-mathematics/coq/files/coq-8.1_p3-noocamlopt.patch
new file mode 100644
index 000000000000..fc954d5900cf
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.1_p3-noocamlopt.patch
@@ -0,0 +1,13 @@
+Index: coq-8.1pl3/Makefile
+===================================================================
+--- coq-8.1pl3.orig/Makefile
++++ coq-8.1pl3/Makefile
+@@ -1481,7 +1481,7 @@ dev/printers.cma: $(PRINTERSCMO)
+ parsing/grammar.cma: $(GRAMMARCMO)
+ $(SHOW)'Testing $@'
+ @touch test.ml4
+- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
++ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
+ @rm -f test-grammar test.*
+ $(SHOW)'OCAMLC -a $@'
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
diff --git a/sci-mathematics/coq/files/coqide.desktop b/sci-mathematics/coq/files/coqide.desktop
index 08b5b6918cd0..91954772c3a2 100644
--- a/sci-mathematics/coq/files/coqide.desktop
+++ b/sci-mathematics/coq/files/coqide.desktop
@@ -7,4 +7,4 @@ Name=CoqIDE
GenericName=Coq IDE
Terminal=false
Type=Application
-Categories=Application;Edutainment;Mathematics;
+Categories=Application;Education;Math;