commit: b206aa4fe3a4c1c45600674a0a55626d80014e19 Author: Maciej Barć <xgqt <AT> riseup <DOT> net> AuthorDate: Tue Oct 19 21:41:00 2021 +0000 Commit: Maciej Barć <xgqt <AT> riseup <DOT> net> CommitDate: Tue Oct 19 21:41:00 2021 +0000 URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=b206aa4f
dev-lang/lean: add version 3.33.0 Package-Manager: Portage-3.0.20, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt <AT> riseup.net> dev-lang/lean/Manifest | 1 + dev-lang/lean/lean-3.33.0.ebuild | 45 ++++++++++++++++++++++++++++++++++++++++ dev-lang/lean/metadata.xml | 20 ++++++++++++++++++ 3 files changed, 66 insertions(+) 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>[email protected]</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>
