diff options
| author |   Maciej Barć <xgqt@riseup.net> | 2021-10-19 23:41:00 +0200 |
|---|---|---|
| committer | Maciej Barć <xgqt@riseup.net> | 2021-10-19 23:41:00 +0200 |
| commit | b206aa4fe3a4c1c45600674a0a55626d80014e19 (patch) | |
| tree | b475cb024ca285c9aa13b942aeabed94b4be48c4 /dev-lang | |
| parent | dev-cpp/cli11: add 2.1.2, drop 2.0.0 (diff) | |
| download | guru-b206aa4fe3a4c1c45600674a0a55626d80014e19.tar.gz guru-b206aa4fe3a4c1c45600674a0a55626d80014e19.tar.bz2 guru-b206aa4fe3a4c1c45600674a0a55626d80014e19.zip | |
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>
Diffstat (limited to 'dev-lang')
| -rw-r--r-- | dev-lang/lean/Manifest | 1 | ||||
| -rw-r--r-- | dev-lang/lean/lean-3.33.0.ebuild | 45 | ||||
| -rw-r--r-- | dev-lang/lean/metadata.xml | 20 |
3 files changed, 66 insertions, 0 deletions
diff --git a/dev-lang/lean/Manifest b/dev-lang/lean/Manifest new file mode 100644 index 000000000..fd42aa380 --- /dev/null +++ b/dev-lang/lean/Manifest @@ -0,0 +1 @@ +DIST lean-3.33.0.tar.gz 1890511 BLAKE2B 93fed81409a5d2fc31fd0963e00262ffbf7ce177954501e01d988666bf55bd4e0243488139f34eb4322055a5512565c6770749f793a8b7a8c7eb6e3045c5c2e7 SHA512 813f21f57913c15ca52b3a40bb0493d156b714ea26c5dcf4d159ee7aedf05dd6259ff57c05aa278bc72a3bfb9a531835387fc8cfbaca7d8341e0f2fbe9535bf3 diff --git a/dev-lang/lean/lean-3.33.0.ebuild b/dev-lang/lean/lean-3.33.0.ebuild new file mode 100644 index 000000000..120a2ac2e --- /dev/null +++ b/dev-lang/lean/lean-3.33.0.ebuild @@ -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" +} diff --git a/dev-lang/lean/metadata.xml b/dev-lang/lean/metadata.xml new file mode 100644 index 000000000..9e03d53ad --- /dev/null +++ b/dev-lang/lean/metadata.xml @@ -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> |