From b038a4290cbc6143e645af48154875918cc98be9 Mon Sep 17 00:00:00 2001 From: saundersp Date: Fri, 31 Oct 2025 20:12:00 +0100 Subject: [PATCH] Added sci-mathematics/lean-4.25.0_rc2 --- .../md5-cache/sci-mathematics/lean-4.25.0_rc2 | 15 +++ sci-mathematics/lean/Manifest | 3 + sci-mathematics/lean/lean-4.25.0_rc2.ebuild | 103 ++++++++++++++++++ sci-mathematics/lean/metadata.xml | 22 ++++ 4 files changed, 143 insertions(+) create mode 100644 metadata/md5-cache/sci-mathematics/lean-4.25.0_rc2 create mode 100644 sci-mathematics/lean/Manifest create mode 100644 sci-mathematics/lean/lean-4.25.0_rc2.ebuild create mode 100644 sci-mathematics/lean/metadata.xml diff --git a/metadata/md5-cache/sci-mathematics/lean-4.25.0_rc2 b/metadata/md5-cache/sci-mathematics/lean-4.25.0_rc2 new file mode 100644 index 0000000..9318735 --- /dev/null +++ b/metadata/md5-cache/sci-mathematics/lean-4.25.0_rc2 @@ -0,0 +1,15 @@ +BDEPEND=|| ( dev-lang/python:3.14 dev-lang/python:3.13 dev-lang/python:3.12 ) dev-build/make >=dev-build/cmake-3.28.5 +DEFINED_PHASES=compile configure install prepare pretend setup test +DEPEND=dev-libs/gmp:= dev-libs/libuv:= sci-mathematics/cadical +DESCRIPTION=The Lean Theorem Prover +EAPI=8 +HOMEPAGE=https://leanprover-community.github.io/ https://github.com/leanprover/lean4/ +INHERIT=check-reqs cmake flag-o-matic python-any-r1 +IUSE=debug source +KEYWORDS=~amd64 +LICENSE=Apache-2.0 +RDEPEND=dev-libs/gmp:= dev-libs/libuv:= sci-mathematics/cadical +SLOT=0/4 +SRC_URI=https://github.com/leanprover/lean4/archive/refs/tags/v4.25.0-rc2.tar.gz -> lean-4.25.0_rc2.tar.gz +_eclasses_=check-reqs 2a9731073c152554078a9a8df8fc0f1b toolchain-funcs 98d9f464d912ae6b7316fb8a3721f5db flag-o-matic a7afe42e95fb46ce9691605acfb24672 multiprocessing 1e32df7deee68372153dca65f4a7c21f ninja-utils 2df4e452cea39a9ec8fb543ce059f8d6 xdg-utils 42869b3c8d86a70ef3cf75165a395e09 cmake 2d36accef058c00889b1f93ea4bc4061 python-utils-r1 dbb8c4d794033ad7e7221eaf567a6c90 python-any-r1 891415dfe39ad9b41b461f2b86354af0 +_md5_=48760dee67524d93db9a50cffcacb957 diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest new file mode 100644 index 0000000..0cd96f7 --- /dev/null +++ b/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 diff --git a/sci-mathematics/lean/lean-4.25.0_rc2.ebuild b/sci-mathematics/lean/lean-4.25.0_rc2.ebuild new file mode 100644 index 0000000..96bbb51 --- /dev/null +++ b/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 +} diff --git a/sci-mathematics/lean/metadata.xml b/sci-mathematics/lean/metadata.xml new file mode 100644 index 0000000..c43ac3a --- /dev/null +++ b/sci-mathematics/lean/metadata.xml @@ -0,0 +1,22 @@ + + + + + + sci-mathematics@gentoo.org + Gentoo Mathematics Project + + + 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. + + + https://github.com/leanprover/lean4/issues + leanprover/lean4 + +