Removed sci-mathematics/lean-4.25.2
This commit is contained in:
saundersp
@@ -1,15 +0,0 @@
|
||||
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.2.tar.gz -> lean-4.25.2.tar.gz
|
||||
_eclasses_=check-reqs 2a9731073c152554078a9a8df8fc0f1b toolchain-funcs 98d9f464d912ae6b7316fb8a3721f5db flag-o-matic a7afe42e95fb46ce9691605acfb24672 multiprocessing 1e32df7deee68372153dca65f4a7c21f ninja-utils 3a59a39e97af0f7c03f49cf3c22f262b xdg-utils 42869b3c8d86a70ef3cf75165a395e09 cmake a36a2a340635cb293524229ee6d2ef7a python-utils-r1 dbb8c4d794033ad7e7221eaf567a6c90 python-any-r1 891415dfe39ad9b41b461f2b86354af0
|
||||
_md5_=48760dee67524d93db9a50cffcacb957
|
||||
@@ -1,3 +0,0 @@
|
||||
DIST lean-4.25.2.tar.gz 50069767 BLAKE2B ebf5b578cf5956a196049e3cde2c52f3dcc6b18078e556e096b3f47c399f4fef629eaa245716b795ad88f981fcc7dc3573e5a973a1c558e13d7c56fda206275b SHA512 cb9d43814a2e7ae8a33aed6fcaf8e64d834905c43846d310a74b1ed3215b20aa0585631a5e9e39df4c499b5de355b644f706e740e8a02572faf1626f1510c08b
|
||||
EBUILD lean-4.25.2.ebuild 1843 BLAKE2B 5e4da67180c9b7d801cbe490001316001d145a682852352f30c17a52f8e7ae3519c1958a99c1b2a19ab5f841827d73ee1753d75dc02cadde3cd2516941209007 SHA512 f37a1c87668396b8bfdd0c724e84dd26778f7a7ae26408265f3d3ebe8382e55876ff4248a9c912b68af05816704094f492f895d61a8e87ed4c094f87fc049a59
|
||||
MISC metadata.xml 954 BLAKE2B 338f64bbe848dca10f77fb7d5b7503684d36742139a4fd45f7a4c48250a11af6a78e40f5304d44166ce56f7fe4d22c6f980b55cab411bb7be93cc279694e9b66 SHA512 ec7c25a75237d2d54704e2d7b1811489a95780885c748a832643760d012eaceaeb5bfec9fc80509d5699940e749e770e841880cca1361848244b5031636e48b2
|
||||
@@ -1,103 +0,0 @@
|
||||
# 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
|
||||
}
|
||||
@@ -1,22 +0,0 @@
|
||||
<?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>
|
||||
Reference in New Issue
Block a user