commit: b5dd196eb69a20afced12e16dfdb0235ed590f52 Author: Maciej Barć <xgqt <AT> gentoo <DOT> org> AuthorDate: Mon Aug 8 23:59:11 2022 +0000 Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org> CommitDate: Mon Aug 8 23:59:11 2022 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=b5dd196e
sci-mathematics/lean: bump to 3.46.0 Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org> sci-mathematics/lean/Manifest | 1 + sci-mathematics/lean/lean-3.46.0.ebuild | 77 +++++++++++++++++++++++++++++++++ 2 files changed, 78 insertions(+) diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest index a86db5365be7..d61351695e7e 100644 --- a/sci-mathematics/lean/Manifest +++ b/sci-mathematics/lean/Manifest @@ -1,3 +1,4 @@ DIST lean-3.43.0.tar.gz 1909158 BLAKE2B 587995afb123e6c74a730f9709a001bab6b2ac82471dcf8b1219dda782853fcdb9735d16038b95a7950f6530dd3cf1e0b13e4d1044d723d3662217951b809928 SHA512 25cbad94b869bb39edaf9ed2478ffc298b130f22cb4db7c116212546583d670079ddde1b524a33499d00ac43fc82b6928e6801c83d613597aae255db9c45d9f3 DIST lean-3.44.1.tar.gz 1911708 BLAKE2B 33dc94fb1f1eac2684b7a37fda3545ad6d4f6d703e7914c44b9a05fb57e55d4b9bef484ff1f6608f9bb0fe453ca28b7fa5c74e6bce135df06fb25ad6d9d3a37b SHA512 69ffd1a8519b476dd1879bfe2f8f8f4268a5490f11b581ee1e583382e6f03f947d958e8b5ee8ceead562945a406ee2dc9b0ae2da6f29f03a38828eadab88a4f8 DIST lean-3.45.0.tar.gz 1913638 BLAKE2B f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f7241844ffff69400ec354a194cc345feca8f0dbcb06a673cc2d3d4 SHA512 c97c1dc6004823c73d8e40b5587ebbee7bd7a90b65ecdd3a976510d0d335b6df9a26916eedd5524f7137a32254a59dd5a6f15ce67f77d500926c9bc781aa5526 +DIST lean-3.46.0.tar.gz 1913857 BLAKE2B de0a48ab3cff934d6a9583833a94a409a6351bd8433dbf47dbb510620a6c27aae26891472b4f1443e0f833b1c13de8653f0ea4edf61d14d43cfdb1aa25a555bf SHA512 d4487154cf6364b49ce19d1946a0bf0af6faeb1276ef08754a3dbed9bf071c2873eebdb1d6bcbe39ab2aaf5e93a97007ce954fd7c1ca4062fb2e6214e75e3b2b diff --git a/sci-mathematics/lean/lean-3.46.0.ebuild b/sci-mathematics/lean/lean-3.46.0.ebuild new file mode 100644 index 000000000000..6623228581a0 --- /dev/null +++ b/sci-mathematics/lean/lean-3.46.0.ebuild @@ -0,0 +1,77 @@ +# Copyright 1999-2022 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="${WORKDIR}/lean-${PV}/src" + +LICENSE="Apache-2.0" +SLOT="0/${MAJOR}" +IUSE="debug +threads" + +RDEPEND="dev-libs/gmp:=" +DEPEND="${RDEPEND}" + +PATCHES=( "${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 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 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 +}
