diff options
author | Maciej Barć <xgqt@riseup.net> | 2021-11-05 09:29:34 +0100 |
---|---|---|
committer | Maciej Barć <xgqt@riseup.net> | 2021-11-05 09:30:48 +0100 |
commit | be2c39fcdaa2101aaae7b14c17b337bf82b97186 (patch) | |
tree | e7bbbff39c496d8be705652dcfe3e9887a45e9ba | |
parent | media-libs/libjxl: add 0.6.1 (diff) | |
download | guru-be2c39fc.tar.gz guru-be2c39fc.tar.bz2 guru-be2c39fc.zip |
dev-lang/lean: bump to 3.35.0
Package-Manager: Portage-3.0.28, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt@riseup.net>
-rw-r--r-- | dev-lang/lean/Manifest | 1 | ||||
-rw-r--r-- | dev-lang/lean/lean-3.35.0.ebuild | 70 |
2 files changed, 71 insertions, 0 deletions
diff --git a/dev-lang/lean/Manifest b/dev-lang/lean/Manifest index b5cb6ec03..c9c3a7261 100644 --- a/dev-lang/lean/Manifest +++ b/dev-lang/lean/Manifest @@ -1,2 +1,3 @@ DIST lean-3.33.0.tar.gz 1890511 BLAKE2B 93fed81409a5d2fc31fd0963e00262ffbf7ce177954501e01d988666bf55bd4e0243488139f34eb4322055a5512565c6770749f793a8b7a8c7eb6e3045c5c2e7 SHA512 813f21f57913c15ca52b3a40bb0493d156b714ea26c5dcf4d159ee7aedf05dd6259ff57c05aa278bc72a3bfb9a531835387fc8cfbaca7d8341e0f2fbe9535bf3 DIST lean-3.34.0.tar.gz 1891710 BLAKE2B 53c25b93c2e720187bfa5980a6bf3c9790aebb757b732704f6f5ad250b333c192417a938bc1cd6274a45f5b5f49f8e275da1f5c5597ffd7bc2da7bbe8b0371f7 SHA512 bc3f81ffbfa3291675d3c09c28c3eacccc2d44d021fb7e9923c7116091046b57f388589074e984f257842757c77972ef3b354d8690cccbebf6d3e2aae1f811a5 +DIST lean-3.35.0.tar.gz 1872221 BLAKE2B 8cdcaa65eb49ad6ed8b6961912d162a5832d45d5f8855ea62334010a1af647cd2aa4906d83317ee16c95cdb44522c1f7cb8f62ece6abda12354e18534e560e6e SHA512 b48a8134bdc39dc098a49303549ed4b96a2ca9e69043b9dca12c4789f60462b94374a184aee6fa33abd5a8f1acce9553b8144e935e539833c853e2384c41c2e7 diff --git a/dev-lang/lean/lean-3.35.0.ebuild b/dev-lang/lean/lean-3.35.0.ebuild new file mode 100644 index 000000000..3ab4b15f4 --- /dev/null +++ b/dev-lang/lean/lean-3.35.0.ebuild @@ -0,0 +1,70 @@ +# Copyright 1999-2021 Gentoo Authors +# Distributed under the terms of the GNU General Public License v2 + +EAPI=8 + +CMAKE_IN_SOURCE_BUILD="ON" + +inherit cmake optfeature + +DESCRIPTION="The Lean Theorem Prover" +HOMEPAGE="https://leanprover-community.github.io/" + +if [[ "${PV}" == *9999* ]]; then + MAJOR=3 # sync this periodically for the live version + inherit git-r3 + EGIT_REPO_URI="https://github.com/leanprover-community/lean.git" +else + MAJOR=$(ver_cut 1) + SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz" + KEYWORDS="~amd64" +fi +S="${WORKDIR}/lean-${PV}/src" + +LICENSE="Apache-2.0" +SLOT="0/${MAJOR}" +IUSE="debug +json +threads" + +RDEPEND="dev-libs/gmp" +DEPEND="${RDEPEND}" + +PATCHES=( "${FILESDIR}/fix_flags.patch" ) + +src_configure() { + local CMAKE_BUILD_TYPE + if use debug; then + CMAKE_BUILD_TYPE="Debug" + else + CMAKE_BUILD_TYPE="Release" + fi + + local mycmakeargs=( + -DALPHA=ON + -DAUTO_THREAD_FINALIZATION=ON + -DJSON=$(usex json) + -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 python test dependency + --exclude-regex style_check + ) + cmake_src_test +} + +pkg_postinst() { + elog "You probably want to use lean with mathlib, to install it you can either:" + elog " - Do not install mathlib globally and use local versions" + elog " - Use leanproject from sci-mathematics/mathlib-tools" + elog " $ leanproject global-install" + elog " - Use leanpkg and compile mathlib (which will take long time)" + elog " $ leanpkg install https://github.com/leanprover-community/mathlib" + + optfeature "project management with leanproject" sci-mathematics/mathlib-tools +} |