commit: 330f97cf5cc6e728931a94f8b4cc5b9ae100505c Author: Maciej Barć <xgqt <AT> gentoo <DOT> org> AuthorDate: Sun Feb 2 17:12:42 2025 +0000 Commit: Maciej Barć <xgqt <AT> gentoo <DOT> 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ć <xgqt <AT> 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ć <[email protected]> (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ć <[email protected]> (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 -}
