From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from lists.gentoo.org (pigeon.gentoo.org [208.92.234.80]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by finch.gentoo.org (Postfix) with ESMTPS id 735E5138334 for ; Tue, 24 Sep 2019 09:46:26 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 9E702E08A8; Tue, 24 Sep 2019 09:46:25 +0000 (UTC) Received: from smtp.gentoo.org (dev.gentoo.org [IPv6:2001:470:ea4a:1:5054:ff:fec7:86e4]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by pigeon.gentoo.org (Postfix) with ESMTPS id 766A2E08A8 for ; Tue, 24 Sep 2019 09:46:25 +0000 (UTC) Received: from oystercatcher.gentoo.org (oystercatcher.gentoo.org [148.251.78.52]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.gentoo.org (Postfix) with ESMTPS id B30C134B4F6 for ; Tue, 24 Sep 2019 09:46:22 +0000 (UTC) Received: from localhost.localdomain (localhost [IPv6:::1]) by oystercatcher.gentoo.org (Postfix) with ESMTP id 3D6E4775 for ; Tue, 24 Sep 2019 09:46:20 +0000 (UTC) From: "Mark Wright" To: gentoo-commits@lists.gentoo.org Content-Transfer-Encoding: 8bit Content-type: text/plain; charset=UTF-8 Reply-To: gentoo-dev@lists.gentoo.org, "Mark Wright" Message-ID: <1569318323.983a017561dee1f3d28f9e3cc71f40ffdccbec41.gienah@gentoo> Subject: [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/coq/ X-VCS-Repository: repo/gentoo X-VCS-Files: sci-mathematics/coq/Manifest sci-mathematics/coq/coq-8.9.1.ebuild X-VCS-Directories: sci-mathematics/coq/ X-VCS-Committer: gienah X-VCS-Committer-Name: Mark Wright X-VCS-Revision: 983a017561dee1f3d28f9e3cc71f40ffdccbec41 X-VCS-Branch: master Date: Tue, 24 Sep 2019 09:46:20 +0000 (UTC) Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-commits@lists.gentoo.org X-Auto-Response-Suppress: DR, RN, NRN, OOF, AutoReply X-Archives-Salt: 076b2dad-4f31-4ed9-977e-6a07b9b12d50 X-Archives-Hash: 520e964b7c3a542dd5bbd4eb9c765ceb commit: 983a017561dee1f3d28f9e3cc71f40ffdccbec41 Author: Mark Wright gentoo org> AuthorDate: Tue Sep 24 09:45:23 2019 +0000 Commit: Mark Wright gentoo org> CommitDate: Tue Sep 24 09:45:23 2019 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=983a0175 sci-mathematics/coq: Bump to 8.9.1 Thanks to Han and Anton Kochkov for requesting the bump. Closes: https://bugs.gentoo.org/653864 Closes: https://bugs.gentoo.org/672038 Package-Manager: Portage-2.3.76, Repoman-2.3.17 Signed-off-by: Mark Wright gentoo.org> sci-mathematics/coq/Manifest | 1 + sci-mathematics/coq/coq-8.9.1.ebuild | 86 ++++++++++++++++++++++++++++++++++++ 2 files changed, 87 insertions(+) diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest index 7e3dbefa8fc..758414ac5b9 100644 --- a/sci-mathematics/coq/Manifest +++ b/sci-mathematics/coq/Manifest @@ -1,2 +1,3 @@ DIST coq-8.6.1.tar.gz 5588811 BLAKE2B 1016e54ef9b42a8534add55ab057454fad35b3fe103ba877689489c7d9cf43d76c1fbee123801d91035d353a882120650f94c433d9ee1daa878b8c819609c949 SHA512 814ab76a06ca15f927081428da74add4bc67290199fa011853b9c68a00cdefaf813b10fbac18a434f4504fce8f2173eb544080bf6f50d62caa41bb8724b13083 DIST coq-8.6.tar.gz 5538848 BLAKE2B 025d6598a5155712662ce20a56804b75c236f1d1dc4ed81e779aaf2916d5cb525acfcbef9b5960fc5b8b44f2e2290c9f7e5c2d6e84726400a9888587ee29cd16 SHA512 9f5f4913fda8cf83683fec9398b42d4567207c3d4b52b4638d5e09a24ed25a43905fb57a9fac1bb9f9d681bd47f3560e1da74e79348b3a3fd93e2e8c686cebae +DIST coq-8.9.1.tar.gz 6001970 BLAKE2B f65498e2485c59f4f95d2afeac35750ebf85b5af6db7c269a11635f2414df483d4cb159557060c9118de25f4922176f54d2e5c6f12174599371348341cb4d80f SHA512 66344f801b955d1b6daf3ab1d704551070c95cf9032ae74f15fb33f7ec313812b3e05c0ec277a2eb448e3fdfd9721df06d36612e2fb4928b6530d70147f1d983 diff --git a/sci-mathematics/coq/coq-8.9.1.ebuild b/sci-mathematics/coq/coq-8.9.1.ebuild new file mode 100644 index 00000000000..a7de5198ee4 --- /dev/null +++ b/sci-mathematics/coq/coq-8.9.1.ebuild @@ -0,0 +1,86 @@ +# Copyright 1999-2019 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI="7" + +inherit eutils multilib + +MY_PV=${PV/_p/pl} +MY_P=${PN}-${MY_PV} + +DESCRIPTION="Proof assistant written in O'Caml" +HOMEPAGE="http://coq.inria.fr/" +SRC_URI="https://github.com/coq/coq/archive/V${MY_PV}.tar.gz -> ${P}.tar.gz" + +LICENSE="LGPL-2.1" +SLOT="0" +KEYWORDS="~amd64 ~ppc ~x86" +IUSE="gtk debug +ocamlopt doc" + +RESTRICT=test + +# Note: RDEPEND will require dev-ml/num:= for >=dev-lang/ocaml-4.0.7 +RDEPEND=" + >=dev-lang/ocaml-4.0.5:=[ocamlopt?] + dev-ml/camlp5:=[ocamlopt?] + gtk? ( dev-ml/lablgtk:=[sourceview,ocamlopt?] )" +DEPEND="${RDEPEND} + dev-ml/findlib + doc? ( + media-libs/netpbm[png,zlib] + virtual/latex-base + dev-tex/hevea + dev-tex/xcolor + dev-texlive/texlive-pictures + dev-texlive/texlive-mathscience + dev-texlive/texlive-latexextra + )" + +S=${WORKDIR}/${MY_P} + +src_configure() { + ocaml_lib=$(ocamlc -where) + local myconf=( + -prefix /usr + -bindir /usr/bin + -libdir /usr/$(get_libdir)/coq + -mandir /usr/share/man + -coqdocdir /usr/$(get_libdir)/coq/coqdoc + -docdir /usr/share/doc/${PF} + -configdir /etc/xdg/${PN} + -lablgtkdir ${ocaml_lib}/lablgtk2 + ) + + use debug && myconf+=( -debug ) + use doc || myconf+=( -with-doc no ) + + if use gtk; then + if use ocamlopt; then + myconf+=( -coqide opt ) + else + myconf+=( -coqide byte ) + fi + else + myconf+=( -coqide no ) + fi + + use ocamlopt || myconf+=( -byte-only ) + + export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/" + ./configure ${myconf[@]} || die "configure failed" +} + +src_compile() { + emake STRIP="true" -j1 world VERBOSE=1 +} + +src_test() { + emake STRIP="true" check VERBOSE=1 +} + +src_install() { + emake STRIP="true" COQINSTALLPREFIX="${D}" install VERBOSE=1 + dodoc README.md CREDITS CHANGES.md + + use gtk && make_desktop_entry "coqide" "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png" +}