From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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)) (No client certificate requested) by finch.gentoo.org (Postfix) with ESMTPS id 21194158B20 for ; Sun, 02 Feb 2025 17:28:05 +0000 (UTC) Received: from lists.gentoo.org (bobolink.gentoo.org [140.211.166.189]) (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) (Authenticated sender: relay-lists.gentoo.org@gentoo.org) by smtp.gentoo.org (Postfix) with ESMTPSA id 073DC343075 for ; Sun, 02 Feb 2025 17:28:05 +0000 (UTC) Received: from bobolink.gentoo.org (localhost [127.0.0.1]) by bobolink.gentoo.org (Postfix) with ESMTP id 3C860110471; Sun, 02 Feb 2025 17:28:00 +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 bobolink.gentoo.org (Postfix) with ESMTPS id 32D71110471 for ; Sun, 02 Feb 2025 17:28:00 +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) server-digest SHA256) (No client certificate requested) by smtp.gentoo.org (Postfix) with ESMTPS id D747434301C for ; Sun, 02 Feb 2025 17:27:59 +0000 (UTC) Received: from localhost.localdomain (localhost [IPv6:::1]) by oystercatcher.gentoo.org (Postfix) with ESMTP id 1A15D2532 for ; Sun, 02 Feb 2025 17:27:58 +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: <1738517264.330f97cf5cc6e728931a94f8b4cc5b9ae100505c.xgqt@gentoo> Subject: [gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/, profiles/ X-VCS-Repository: repo/gentoo X-VCS-Files: profiles/package.mask sci-mathematics/lean/Manifest sci-mathematics/lean/lean-3.51.1.ebuild X-VCS-Directories: sci-mathematics/lean/ profiles/ X-VCS-Committer: xgqt X-VCS-Committer-Name: Maciej Barć X-VCS-Revision: 330f97cf5cc6e728931a94f8b4cc5b9ae100505c X-VCS-Branch: master Date: Sun, 02 Feb 2025 17:27:58 +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: 7fe46ee7-ead0-4144-871b-3221f6c6c261 X-Archives-Hash: 70564f6975464c82e4ddf807f1efc14c commit: 330f97cf5cc6e728931a94f8b4cc5b9ae100505c Author: Maciej Barć gentoo org> AuthorDate: Sun Feb 2 17:12:42 2025 +0000 Commit: Maciej Barć gentoo org> CommitDate: Sun Feb 2 17:27:44 2025 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=330f97cf sci-mathematics/lean: treeclean SLOT 0/3 Closes: https://bugs.gentoo.org/939854 Closes: https://bugs.gentoo.org/937429 Closes: https://bugs.gentoo.org/936618 Signed-off-by: Maciej Barć gentoo.org> profiles/package.mask | 6 --- sci-mathematics/lean/Manifest | 1 - sci-mathematics/lean/lean-3.51.1.ebuild | 80 --------------------------------- 3 files changed, 87 deletions(-) diff --git a/profiles/package.mask b/profiles/package.mask index 89445aba3469..337352ac1a0a 100644 --- a/profiles/package.mask +++ b/profiles/package.mask @@ -282,12 +282,6 @@ media-plugins/gst-plugins-kate # Removal on 2025-03-03 unless upstream fixes the issue net-im/whatsie -# Maciej Barć (2025-01-02) -# Deprecated LEAN 3 packages. The "mathlib-tools" repo is archived -# (https://github.com/leanprover-community/mathlib-tools). Migrate to LEAN 4. -# Removal on 2025-02-02 -sci-mathematics/lean:0/3 - # Maciej Barć (2025-01-02) # Upstream dead, repo archived (https://github.com/mono/xsp). Uses deprecated # "dotnet" eclass. Depends on old mono. As a replacement one can use official diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest index 449b3b8f1ae1..feb08a28faf2 100644 --- a/sci-mathematics/lean/Manifest +++ b/sci-mathematics/lean/Manifest @@ -1,3 +1,2 @@ -DIST lean-3.51.1.tar.gz 1918894 BLAKE2B 9a240fe73193794a57001582c0623052cfc1c08ef3b155cac2d9dfc029202cb79b85e844fdf068e454498a35522ec3e18330da8c644bba3c6f708cbde04816f7 SHA512 dccdf6c3fbcd98115e62b9944645af6a2ce21412d63baa9565871807862e8d83cc6f29d1fb687f19b802240a5f9c019443caa00412ecfabe621744dff900e3ee DIST lean-4.11.0.tar.gz 25790812 BLAKE2B d9a4eb15199f81c6757acf35fb17c795bb9d69158c7e7deb11d98a45bebf569dcda5f7733b2effd2be0eea879a6c7c24b270d97159e5898215e82e853320918c SHA512 2314659910b4d872c4ae0dda648a9cab9e1cc44cd4c55486a494b65b20fdae236ab9db99a42d7fb1a80030e300e95606065ee7dd27578b12a4c47fc8c102e2bb DIST lean-4.14.0.tar.gz 28508743 BLAKE2B 692972402726a77ca9255edbecfc2bd30033d5c7137b00e85821d5bb74f7ed77398b19e7e3098eeecf6812ad9ca568a4076b11a91456b84f4ad78be8f6441286 SHA512 871169b3d7951934990a86a2b5d1741b00f4559c53c69ecdf0ca1c091426f1d7a6baa5ce69029dbecfc4a9dc9da9ee36b327cbef0ab28e80a9f64d34a2666c78 diff --git a/sci-mathematics/lean/lean-3.51.1.ebuild b/sci-mathematics/lean/lean-3.51.1.ebuild deleted file mode 100644 index 6c8c7551d8ef..000000000000 --- a/sci-mathematics/lean/lean-3.51.1.ebuild +++ /dev/null @@ -1,80 +0,0 @@ -# Copyright 1999-2023 Gentoo Authors -# Distributed under the terms of the GNU General Public License v2 - -EAPI=8 - -MAJOR=$(ver_cut 1) -CMAKE_IN_SOURCE_BUILD="ON" - -inherit flag-o-matic cmake readme.gentoo-r1 - -DESCRIPTION="The Lean Theorem Prover" -HOMEPAGE="https://leanprover-community.github.io/" - -if [[ ${PV} == *9999* ]] ; then - inherit git-r3 - EGIT_REPO_URI="https://github.com/leanprover-community/lean.git" -else - SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz" - KEYWORDS="amd64 ~x86" -fi -S="${S}/src" - -LICENSE="Apache-2.0" -SLOT="0/${MAJOR}" -IUSE="debug +threads" - -RDEPEND="dev-libs/gmp:=" -DEPEND="${RDEPEND}" - -PATCHES=( - "${FILESDIR}"/${PN}-3.50.3-gcc-13.patch - "${FILESDIR}"/${PN}-CMakeLists-fix_flags.patch -) - -src_configure() { - local CMAKE_BUILD_TYPE - if use debug; then - CMAKE_BUILD_TYPE="Debug" - else - CMAKE_BUILD_TYPE="Release" - fi - - filter-lto - - local -a mycmakeargs=( - -DALPHA=ON - -DAUTO_THREAD_FINALIZATION=ON - -DJSON=ON # bug 833900 - -DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}" - -DMULTI_THREAD=$(usex threads) - -DUSE_GITHASH=OFF - ) - cmake_src_configure -} - -src_test() { - local -a myctestargs=( - # Disable problematic "style_check" cpplint test, - # this also removes the python test dependency - --exclude-regex style_check - ) - cmake_src_test -} - -src_install() { - cmake_src_install - - local DISABLE_AUTOFORMATTING="yes" - local DOC_CONTENTS="You probably want to use lean with mathlib, you can either: - - Do not install mathlib globally and use local versions - - Use leanproject from sci-mathematics/mathlib-tools - $ leanproject global-install - - Use leanpkg and compile mathlib (which will take some time) - $ leanpkg install https://github.com/leanprover-community/mathlib" - readme.gentoo_create_doc -} - -pkg_postinst() { - readme.gentoo_print_elog -}