Added sci-mathematics/lean-4.25.0_rc2

sci-mathematics/lean/Manifest

@@ -0,0 +1,3 @@
+DIST lean-4.25.0_rc2.tar.gz 50072895 BLAKE2B bf081912fd8896a3916ef95af97cfd63646f13cc3c0b397966a8195d34e60ca500562c48565fb27eeca5b51d90a3dcd1f5dd20507b1f3bae83d7d16b6c1c2d78 SHA512 1f99b0c85188ad66d4d161f1ef886449999d891e09c92af6018937e4fdbc56cfb05de3eee6e666ae0cec85075f8d517dbd27fc14361854f7f1a939b6c9d41687
+EBUILD lean-4.25.0_rc2.ebuild 1843 BLAKE2B 5e4da67180c9b7d801cbe490001316001d145a682852352f30c17a52f8e7ae3519c1958a99c1b2a19ab5f841827d73ee1753d75dc02cadde3cd2516941209007 SHA512 f37a1c87668396b8bfdd0c724e84dd26778f7a7ae26408265f3d3ebe8382e55876ff4248a9c912b68af05816704094f492f895d61a8e87ed4c094f87fc049a59
+MISC metadata.xml 954 BLAKE2B 338f64bbe848dca10f77fb7d5b7503684d36742139a4fd45f7a4c48250a11af6a78e40f5304d44166ce56f7fe4d22c6f980b55cab411bb7be93cc279694e9b66 SHA512 ec7c25a75237d2d54704e2d7b1811489a95780885c748a832643760d012eaceaeb5bfec9fc80509d5699940e749e770e841880cca1361848244b5031636e48b2

sci-mathematics/lean/lean-4.25.0_rc2.ebuild

@@ -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
+}

sci-mathematics/lean/metadata.xml

@@ -0,0 +1,22 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <longdescription>
+    The Lean theorem prover is a proof assistant developed principally
+    by Leonardo de Moura at Microsoft Research.  Lean is a functional
+    programming language that makes it easy to write correct and
+    maintainable code. You can also use Lean as an interactive theorem
+    prover. Lean programming primarily involves defining types and
+    functions. This allows your focus to remain on the problem domain and
+    manipulating its data, rather than the details of programming.
+  </longdescription>
+  <upstream>
+    <bugs-to>https://github.com/leanprover/lean4/issues</bugs-to>
+    <remote-id type="github">leanprover/lean4</remote-id>
+  </upstream>
+</pkgmetadata>