mirror of
https://github.com/gentoo-mirror/guru.git
synced 2026-07-21 04:53:07 -04:00
dev-lang/lean: add version 3.33.0
Package-Manager: Portage-3.0.20, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt@riseup.net>
This commit is contained in:
1
dev-lang/lean/Manifest
Normal file
1
dev-lang/lean/Manifest
Normal file
@@ -0,0 +1 @@
|
||||
DIST lean-3.33.0.tar.gz 1890511 BLAKE2B 93fed81409a5d2fc31fd0963e00262ffbf7ce177954501e01d988666bf55bd4e0243488139f34eb4322055a5512565c6770749f793a8b7a8c7eb6e3045c5c2e7 SHA512 813f21f57913c15ca52b3a40bb0493d156b714ea26c5dcf4d159ee7aedf05dd6259ff57c05aa278bc72a3bfb9a531835387fc8cfbaca7d8341e0f2fbe9535bf3
|
||||
45
dev-lang/lean/lean-3.33.0.ebuild
Normal file
45
dev-lang/lean/lean-3.33.0.ebuild
Normal file
@@ -0,0 +1,45 @@
|
||||
# Copyright 1999-2021 Gentoo Authors
|
||||
# Distributed under the terms of the GNU General Public License v2
|
||||
|
||||
EAPI=7
|
||||
|
||||
CMAKE_IN_SOURCE_BUILD="ON"
|
||||
|
||||
inherit cmake
|
||||
|
||||
DESCRIPTION="The Lean Theorem Prover"
|
||||
HOMEPAGE="https://leanprover-community.github.io/"
|
||||
|
||||
if [[ "${PV}" == *9999* ]]; then
|
||||
inherit git-r3
|
||||
EGIT_REPO_URI="https://github.com/leanprover-community/lean.git"
|
||||
else
|
||||
SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz"
|
||||
KEYWORDS="~amd64"
|
||||
fi
|
||||
S="${WORKDIR}/lean-${PV}/src"
|
||||
|
||||
RESTRICT="!test? ( test )"
|
||||
LICENSE="Apache-2.0"
|
||||
SLOT="0"
|
||||
IUSE="+json test +threads"
|
||||
|
||||
RDEPEND="dev-libs/gmp"
|
||||
DEPEND="${RDEPEND}"
|
||||
|
||||
src_configure() {
|
||||
local mycmakeargs=(
|
||||
-DALPHA=ON
|
||||
-DAUTO_THREAD_FINALIZATION=ON
|
||||
-DJSON=$(usex json)
|
||||
-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
|
||||
-DMULTI_THREAD=$(usex threads)
|
||||
-DUSE_GITHASH=OFF
|
||||
)
|
||||
cmake_src_configure
|
||||
}
|
||||
|
||||
pkg_postinst() {
|
||||
elog "You probably want to use lean with mathlib, to install it use leanpkg."
|
||||
elog "For example: leanpkg install https://github.com/leanprover-community/mathlib"
|
||||
}
|
||||
20
dev-lang/lean/metadata.xml
Normal file
20
dev-lang/lean/metadata.xml
Normal file
@@ -0,0 +1,20 @@
|
||||
<?xml version="1.0" encoding="UTF-8"?>
|
||||
<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
|
||||
|
||||
<pkgmetadata>
|
||||
<maintainer type="person">
|
||||
<email>xgqt@riseup.net</email>
|
||||
<name>Maciej Barć</name>
|
||||
</maintainer>
|
||||
<longdescription lang="en">
|
||||
The Lean theorem prover is a proof assistant developed principally
|
||||
by Leonardo de Moura at Microsoft Research.
|
||||
</longdescription>
|
||||
<upstream>
|
||||
<bugs-to>https://github.com/leanprover-community/lean/issues</bugs-to>
|
||||
<remote-id type="github">leanprover-community/lean</remote-id>
|
||||
</upstream>
|
||||
<use>
|
||||
<flag name="json"> Enable JSON support</flag>
|
||||
</use>
|
||||
</pkgmetadata>
|
||||
Reference in New Issue
Block a user