Adding metadata

2 files changed, 104 insertions, 0 deletions

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 4e7de681fe75..281d8ec7ca8e 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,2 +1,3 @@
 DIST lean-4.14.0.tar.gz 28508743 BLAKE2B 692972402726a77ca9255edbecfc2bd30033d5c7137b00e85821d5bb74f7ed77398b19e7e3098eeecf6812ad9ca568a4076b11a91456b84f4ad78be8f6441286 SHA512 871169b3d7951934990a86a2b5d1741b00f4559c53c69ecdf0ca1c091426f1d7a6baa5ce69029dbecfc4a9dc9da9ee36b327cbef0ab28e80a9f64d34a2666c78
 DIST lean-4.23.0.tar.gz 45087678 BLAKE2B f71b2f14d42471aea9eb2cc0bf03450afa8007ae7867f8ac9803031184ea0e7213bb9ac2a73d45153fe2b72b308552dd66868b846c9fcea20bb7abbe697aca37 SHA512 1f45448a28e2762ba071fabb0b217d2f96591bdfc7205600cc46ef4192941f7b9e15d86c703bd7e8ae3a92026f93ae5b2039ad5dc0c45abf2907e8ec14adb39d
+DIST lean-4.24.0.tar.gz 46435872 BLAKE2B 6e5b40006a48976419ab31beadd24f98fd589972cec45053d11890301d317ffcc79493befa77dceda6fbc5f9238457aa31a3bc26fe06d95840130ef9a58dc80d SHA512 a8f407bdf581833b8cdf386fb7a8b89c0c52578af601f9a715b1ea604badc235bdb66fad96ace7592fcf5831b3c62eca6a843c3acb7907360725f992a37363eb
diff --git a/sci-mathematics/lean/lean-4.24.0.ebuild b/sci-mathematics/lean/lean-4.24.0.ebuild
new file mode 100644
index 000000000000..822ac428d67b
--- /dev/null
+++ b/sci-mathematics/lean/lean-4.24.0.ebuild
@@ -0,0 +1,103 @@
+# Copyright 1999-2026 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_{10..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
+}