commit: a98873df4c825acc382e40752d25a28a1c440936 Author: Maciej Barć <xgqt <AT> riseup <DOT> net> AuthorDate: Wed Oct 20 21:31:05 2021 +0000 Commit: Maciej Barć <xgqt <AT> riseup <DOT> net> CommitDate: Wed Oct 20 21:35:14 2021 +0000 URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=a98873df
dev-lang/lean: add info about mathlib-tools Package-Manager: Portage-3.0.20, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt <AT> riseup.net> dev-lang/lean/lean-3.33.0.ebuild | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/dev-lang/lean/lean-3.33.0.ebuild b/dev-lang/lean/lean-3.33.0.ebuild index 120a2ac2e..ade8a9dae 100644 --- a/dev-lang/lean/lean-3.33.0.ebuild +++ b/dev-lang/lean/lean-3.33.0.ebuild @@ -5,7 +5,7 @@ EAPI=7 CMAKE_IN_SOURCE_BUILD="ON" -inherit cmake +inherit cmake optfeature DESCRIPTION="The Lean Theorem Prover" HOMEPAGE="https://leanprover-community.github.io/"; @@ -40,6 +40,12 @@ 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"; + elog "You probably want to use lean with mathlib, to install it you can either:" + elog " - Do not install mathlib globally and use local versions" + elog " - Use leanproject from sci-mathematics/mathlib-tools" + elog " $ leanproject global-install" + elog " - Use leanpkg and compile mathlib (which will take long time)" + elog " $ leanpkg install https://github.com/leanprover-community/mathlib"; + + optfeature "project management with leanproject" sci-mathematics/mathlib-tools }
