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.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits)) (No client certificate requested) by finch.gentoo.org (Postfix) with ESMTPS id 57E10158004 for ; Mon, 10 Jun 2024 13:59:48 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 5E03AE2AE0; Mon, 10 Jun 2024 13:59:47 +0000 (UTC) Received: from smtp.gentoo.org (woodpecker.gentoo.org [140.211.166.183]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by pigeon.gentoo.org (Postfix) with ESMTPS id 387C4E2AE0 for ; Mon, 10 Jun 2024 13:59:47 +0000 (UTC) Received: from oystercatcher.gentoo.org (oystercatcher.gentoo.org [148.251.78.52]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits)) (No client certificate requested) by smtp.gentoo.org (Postfix) with ESMTPS id 3395733BEEE for ; Mon, 10 Jun 2024 13:59:46 +0000 (UTC) Received: from localhost.localdomain (localhost [IPv6:::1]) by oystercatcher.gentoo.org (Postfix) with ESMTP id BC56B1769 for ; Mon, 10 Jun 2024 13:59:44 +0000 (UTC) From: "Maciej Barć" To: gentoo-commits@lists.gentoo.org Content-Transfer-Encoding: 8bit Content-type: text/plain; charset=UTF-8 Reply-To: gentoo-dev@lists.gentoo.org, "Maciej Barć" Message-ID: <1718027982.cc52d8257b700044a2900d8c0413607491f4e93a.xgqt@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.19.2.ebuild X-VCS-Directories: sci-mathematics/coq/ X-VCS-Committer: xgqt X-VCS-Committer-Name: Maciej Barć X-VCS-Revision: cc52d8257b700044a2900d8c0413607491f4e93a X-VCS-Branch: master Date: Mon, 10 Jun 2024 13:59:44 +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: a7ffc4dc-7ad8-4a29-a020-b33bee150619 X-Archives-Hash: 2fe57fe0623014675d7f0ad103045634 commit: cc52d8257b700044a2900d8c0413607491f4e93a Author: Maciej Barć gentoo org> AuthorDate: Mon Jun 10 13:25:06 2024 +0000 Commit: Maciej Barć gentoo org> CommitDate: Mon Jun 10 13:59:42 2024 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=cc52d825 sci-mathematics/coq: bump to 8.19.2 Signed-off-by: Maciej Barć gentoo.org> sci-mathematics/coq/Manifest | 1 + sci-mathematics/coq/coq-8.19.2.ebuild | 122 ++++++++++++++++++++++++++++++++++ 2 files changed, 123 insertions(+) diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest index 5bb33b14f551..d12fee666b04 100644 --- a/sci-mathematics/coq/Manifest +++ b/sci-mathematics/coq/Manifest @@ -1,2 +1,3 @@ DIST coq-8.19.0.tar.gz 7674352 BLAKE2B 195040c01797ac9ce67611e0c96a4601e0a48966e094e868b9f3644aa9f75fa85adf0e2e6340a14ae0a0598b746f5ad989d8f10736cd2d3852a449f6f79d2c93 SHA512 02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b DIST coq-8.19.1.tar.gz 7675945 BLAKE2B 62ee346f50d0a22ab217a8e689c3078347519d159619b75f20a8decace356b49c60bcd5b2cec5fbcaffc758a8944f8a7940298df1c0ddddfbd858ed9269c12f3 SHA512 ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42 +DIST coq-8.19.2.tar.gz 7678311 BLAKE2B 5f9617fbe0127b0c8357c63f331ba3e9fb5a931be9a4a8e8de2e27820a0d986bf99ed9a512740a0f721c742504225ae56e240af893510aa0e449931499d10aab SHA512 91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c diff --git a/sci-mathematics/coq/coq-8.19.2.ebuild b/sci-mathematics/coq/coq-8.19.2.ebuild new file mode 100644 index 000000000000..f61b2d0f54da --- /dev/null +++ b/sci-mathematics/coq/coq-8.19.2.ebuild @@ -0,0 +1,122 @@ +# Copyright 1999-2024 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +MY_PV="${PV/_p/pl}" +MY_P="${PN}-${MY_PV}" + +inherit check-reqs desktop dune edo + +DESCRIPTION="Proof assistant written in O'Caml" +HOMEPAGE="http://coq.inria.fr/ + https://github.com/coq/coq/" +SRC_URI="https://github.com/coq/coq/archive/V${MY_PV}.tar.gz + -> ${P}.tar.gz" +S="${WORKDIR}/${MY_P}" + +LICENSE="LGPL-2.1" +SLOT="0/${PV}" +KEYWORDS="~amd64 ~x86" +IUSE="debug doc gui +ocamlopt test" + +# TODO: Lots of failing tests. Maybe investigate later. +# RESTRICT="!test? ( test )" +RESTRICT="test" + +RDEPEND=" + dev-ml/num:= + dev-ml/zarith:= + gui? ( + >=dev-ml/lablgtk-3.1.2:3=[sourceview,ocamlopt?] + >=dev-ml/lablgtk-sourceview-3.1.2:3=[ocamlopt?] + ) +" +DEPEND=" + ${RDEPEND} +" +BDEPEND=" + dev-ml/findlib + doc? ( + >=dev-java/antlr-4.7:4 + dev-python/antlr4-python3-runtime + dev-python/beautifulsoup4 + dev-python/pexpect + dev-python/sphinx-rtd-theme + dev-python/sphinxcontrib-bibtex + dev-tex/latexmk + dev-texlive/texlive-fontsextra + dev-texlive/texlive-latexextra + dev-texlive/texlive-xetex + media-fonts/freefont + ) + test? ( + dev-ml/ounit2 + ) +" + +CHECKREQS_DISK_BUILD="2G" + +DOCS=( CODE_OF_CONDUCT.md CONTRIBUTING.md CREDITS INSTALL.md README.md ) +DUNE_PACKAGES=() + +src_prepare() { + # Remove failing tests. bug #904186 + rm -r test-suite/coq-makefile/timing || die + + default +} + +src_configure() { + export CAML_LD_LIBRARY_PATH="${S}/kernel/byterun/" + + DUNE_PACKAGES=( + coq-core + coq-stdlib + coqide-server + coq + ) + use gui && DUNE_PACKAGES+=( coqide ) + + emake clean + + local -a myconf=( + -prefix /usr + -libdir "/usr/$(get_libdir)/coq" + -mandir /usr/share/man + -docdir "/usr/share/doc/${PF}" + -datadir /usr/share/coq + -configdir "/etc/xdg/${PN}" + -native-compiler "$(usex ocamlopt yes no)" + ) + use debug && myconf+=( -debug ) + edo sh ./configure "${myconf[@]}" +} + +src_compile() { + emake DUNEOPT="--display=short --profile release" VERBOSE=1 dunestrap + + dune-compile "${DUNE_PACKAGES[@]}" + + use doc && emake refman-html +} + +src_install() { + dune-install "${DUNE_PACKAGES[@]}" + + if use gui ; then + make_desktop_entry coqide "Coq IDE" "${EPREFIX}/usr/share/coq/coq.png" + fi + + local ocamlc_where + ocamlc_where="$(ocamlc -where)" + + # Dune installs into /usr//ocaml/ but + # Coq wants /usr// ; symlink those directories + local sym + for sym in "${DUNE_PACKAGES[@]}" ; do + dosym "${ocamlc_where}/${sym}" "/usr/$(get_libdir)/${sym}" + done + + einstalldocs +}