mirror of
https://github.com/gentoo-mirror/gentoo.git
synced 2026-09-24 04:59:14 -07:00
sci-mathematics/lean: bump to 4.23.0
Closes: https://bugs.gentoo.org/959310 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
This commit is contained in:
@@ -1 +1,2 @@
|
||||
DIST lean-4.14.0.tar.gz 28508743 BLAKE2B 692972402726a77ca9255edbecfc2bd30033d5c7137b00e85821d5bb74f7ed77398b19e7e3098eeecf6812ad9ca568a4076b11a91456b84f4ad78be8f6441286 SHA512 871169b3d7951934990a86a2b5d1741b00f4559c53c69ecdf0ca1c091426f1d7a6baa5ce69029dbecfc4a9dc9da9ee36b327cbef0ab28e80a9f64d34a2666c78
|
||||
DIST lean-4.23.0.tar.gz 45087678 BLAKE2B f71b2f14d42471aea9eb2cc0bf03450afa8007ae7867f8ac9803031184ea0e7213bb9ac2a73d45153fe2b72b308552dd66868b846c9fcea20bb7abbe697aca37 SHA512 1f45448a28e2762ba071fabb0b217d2f96591bdfc7205600cc46ef4192941f7b9e15d86c703bd7e8ae3a92026f93ae5b2039ad5dc0c45abf2907e8ec14adb39d
|
||||
|
||||
103
sci-mathematics/lean/lean-4.23.0.ebuild
Normal file
103
sci-mathematics/lean/lean-4.23.0.ebuild
Normal file
@@ -0,0 +1,103 @@
|
||||
# Copyright 1999-2025 Gentoo Authors
|
||||
# Distributed under the terms of the GNU General Public License v2
|
||||
|
||||
EAPI=8
|
||||
|
||||
MAJOR="$(ver_cut 1)"
|
||||
|
||||
CMAKE_MAKEFILE_GENERATOR="emake"
|
||||
PYTHON_COMPAT=( python3_{12..14} )
|
||||
|
||||
inherit check-reqs cmake flag-o-matic python-any-r1
|
||||
|
||||
DESCRIPTION="The Lean Theorem Prover"
|
||||
HOMEPAGE="https://leanprover-community.github.io/
|
||||
https://github.com/leanprover/lean4/"
|
||||
|
||||
if [[ "${PV}" == *9999* ]] ; then
|
||||
inherit git-r3
|
||||
|
||||
EGIT_REPO_URI="https://github.com/leanprover/${PN}${MAJOR}"
|
||||
else
|
||||
SRC_URI="https://github.com/leanprover/${PN}${MAJOR}/archive/refs/tags/v${PV/_/-}.tar.gz
|
||||
-> ${P}.tar.gz"
|
||||
S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"
|
||||
|
||||
KEYWORDS="~amd64"
|
||||
fi
|
||||
|
||||
LICENSE="Apache-2.0"
|
||||
SLOT="0/${MAJOR}"
|
||||
IUSE="debug source"
|
||||
|
||||
RDEPEND="
|
||||
dev-libs/gmp:=
|
||||
dev-libs/libuv:=
|
||||
sci-mathematics/cadical
|
||||
"
|
||||
DEPEND="
|
||||
${RDEPEND}
|
||||
"
|
||||
BDEPEND="
|
||||
${PYTHON_DEPS}
|
||||
"
|
||||
|
||||
CHECKREQS_DISK_BUILD="4G"
|
||||
CHECKREQS_DISK_USR="2G"
|
||||
|
||||
# Built by lean's build tool.
|
||||
QA_FLAGS_IGNORED="
|
||||
usr/lib/lean/libInit_shared.so
|
||||
usr/lib/lean/libleanshared_1.so
|
||||
"
|
||||
|
||||
pkg_setup() {
|
||||
python-any-r1_pkg_setup
|
||||
}
|
||||
|
||||
src_prepare() {
|
||||
filter-lto
|
||||
|
||||
sed -e "s|-O[23]|${CFLAGS}|g" -i ./src/CMakeLists.txt || die
|
||||
|
||||
cmake_src_prepare
|
||||
}
|
||||
|
||||
src_configure() {
|
||||
local CMAKE_BUILD_TYPE=""
|
||||
|
||||
if use debug ; then
|
||||
CMAKE_BUILD_TYPE="Debug"
|
||||
else
|
||||
CMAKE_BUILD_TYPE="Release"
|
||||
fi
|
||||
|
||||
local -a mycmakeargs=(
|
||||
-DCCACHE="OFF"
|
||||
-DGIT_HASH="OFF"
|
||||
|
||||
-DUSE_MIMALLOC="OFF"
|
||||
-DINSTALL_LICENSE="OFF"
|
||||
-DINSTALL_CADICAL="OFF"
|
||||
|
||||
-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
|
||||
-DLEAN_EXTRA_LINKER_FLAGS="${LDFLAGS}"
|
||||
-DLEAN_EXTRA_MAKE_OPTS="-s 262144"
|
||||
-DLEANC_EXTRA_FLAGS="${CFLAGS}"
|
||||
)
|
||||
cmake_src_configure
|
||||
}
|
||||
|
||||
src_compile() {
|
||||
ulimit -s 30000000 || eerror "Failed to set required ulimit. Build may fail!"
|
||||
|
||||
cmake_src_compile
|
||||
}
|
||||
|
||||
src_install() {
|
||||
cmake_src_install
|
||||
|
||||
if ! use source ; then
|
||||
rm -r "${ED}/usr/src" || die
|
||||
fi
|
||||
}
|
||||
Reference in New Issue
Block a user