diff options
author | Alexis Ballier <aballier@gentoo.org> | 2008-01-03 17:41:59 +0000 |
---|---|---|
committer | Alexis Ballier <aballier@gentoo.org> | 2008-01-03 17:41:59 +0000 |
commit | 44e70e5132246a832d86e28c7c9299477d2e457c (patch) | |
tree | 3ae772e71e81689b55f40342f81bfddcfb0035fd /sci-mathematics | |
parent | Marking cyrus-imap-dev-2.3.9 ppc64 for bug 201684 (diff) | |
download | historical-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/ChangeLog | 10 | ||||
-rw-r--r-- | sci-mathematics/coq/Manifest | 40 | ||||
-rw-r--r-- | sci-mathematics/coq/coq-8.1_p3.ebuild | 36 | ||||
-rw-r--r-- | sci-mathematics/coq/files/coq-8.1_p3-cmxa-install.dpatch | 23 | ||||
-rw-r--r-- | sci-mathematics/coq/files/coq-8.1_p3-noocamlopt.patch | 13 | ||||
-rw-r--r-- | sci-mathematics/coq/files/coqide.desktop | 2 |
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; |