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 679C3158083 for ; Mon, 9 Sep 2024 00:06:11 +0000 (UTC) Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 2FCD7E2A38; Mon, 9 Sep 2024 00:06:10 +0000 (UTC) Received: from smtp.gentoo.org (dev.gentoo.org [IPv6:2001:470:ea4a:1:5054:ff:fec7:86e4]) (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 pigeon.gentoo.org (Postfix) with ESMTPS id 19E5DE2A38 for ; Mon, 9 Sep 2024 00:06:10 +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 4EB2A340C33 for ; Mon, 9 Sep 2024 00:06:09 +0000 (UTC) Received: from localhost.localdomain (localhost [IPv6:::1]) by oystercatcher.gentoo.org (Postfix) with ESMTP id D50C61D79 for ; Mon, 9 Sep 2024 00:06:07 +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: <1725840365.8a7d012aa6b62a229e09a731b172b64ace75a0e0.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.20.0.ebuild X-VCS-Directories: sci-mathematics/coq/ X-VCS-Committer: xgqt X-VCS-Committer-Name: Maciej Barć X-VCS-Revision: 8a7d012aa6b62a229e09a731b172b64ace75a0e0 X-VCS-Branch: master Date: Mon, 9 Sep 2024 00:06:07 +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: 34105f97-64ee-4915-b97d-a0963e8b868c X-Archives-Hash: c96a8c57cdcbb146d3f868cc16a7e112 commit: 8a7d012aa6b62a229e09a731b172b64ace75a0e0 Author: Maciej Barć gentoo org> AuthorDate: Sun Sep 8 22:56:29 2024 +0000 Commit: Maciej Barć gentoo org> CommitDate: Mon Sep 9 00:06:05 2024 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=8a7d012a sci-mathematics/coq: bump to 8.20.0 Signed-off-by: Maciej Barć gentoo.org> sci-mathematics/coq/Manifest | 1 + sci-mathematics/coq/coq-8.20.0.ebuild | 139 ++++++++++++++++++++++++++++++++++ 2 files changed, 140 insertions(+) diff --git a/sci-mathematics/coq/Manifest b/sci-mathematics/coq/Manifest index d12fee666b04..e860b25a99cb 100644 --- a/sci-mathematics/coq/Manifest +++ b/sci-mathematics/coq/Manifest @@ -1,3 +1,4 @@ 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 +DIST coq-8.20.0.tar.gz 7839432 BLAKE2B 9b489db0cc6874b0a629f3bdb4b503201005ec95a3375441538cd7e51d371a39561b9d0ab23ac485652782fdc7ae8d90c97ca1ff4d9a85fb8727a39ed4a6f48c SHA512 1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b diff --git a/sci-mathematics/coq/coq-8.20.0.ebuild b/sci-mathematics/coq/coq-8.20.0.ebuild new file mode 100644 index 000000000000..18989f3cf9d5 --- /dev/null +++ b/sci-mathematics/coq/coq-8.20.0.ebuild @@ -0,0 +1,139 @@ +# Copyright 1999-2024 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +inherit check-reqs desktop dune edo + +DESCRIPTION="Proof assistant written in O'Caml" +HOMEPAGE="http://coq.inria.fr/ + https://github.com/coq/coq/" + +if [[ "${PV}" == *9999* ]] ; then + inherit git-r3 + + EGIT_REPO_URI="https://github.com/coq/coq.git" +else + SRC_URI="https://github.com/coq/coq/archive/V${MY_PV}.tar.gz + -> ${P}.tar.gz" + + KEYWORDS="~amd64 ~x86" +fi + +LICENSE="LGPL-2.1" +SLOT="0/${PV}" +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 bad tests (recursive). + local -a bad_tests=( + coq-makefile/timing-aggregate + coq-makefile/timing-error + coq-makefile/timing-per-file + coq-makefile/timing-per-line + coq-makefile/timing-template + ) + local bad_test="" + for bad_test in "${bad_tests[@]}" ; do + if [[ -e "test-suite/${bad_test}" ]] ; then + rm -r "test-suite/${bad_test}" || die "failed to remove test ${bad_test}" + else + ewarn "Test file ${bad_test} does not exist" + fi + done + + 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)" + + # 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 +}