1 |
commit: a98873df4c825acc382e40752d25a28a1c440936 |
2 |
Author: Maciej Barć <xgqt <AT> riseup <DOT> net> |
3 |
AuthorDate: Wed Oct 20 21:31:05 2021 +0000 |
4 |
Commit: Maciej Barć <xgqt <AT> riseup <DOT> net> |
5 |
CommitDate: Wed Oct 20 21:35:14 2021 +0000 |
6 |
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=a98873df |
7 |
|
8 |
dev-lang/lean: add info about mathlib-tools |
9 |
|
10 |
Package-Manager: Portage-3.0.20, Repoman-3.0.3 |
11 |
Signed-off-by: Maciej Barć <xgqt <AT> riseup.net> |
12 |
|
13 |
dev-lang/lean/lean-3.33.0.ebuild | 12 +++++++++--- |
14 |
1 file changed, 9 insertions(+), 3 deletions(-) |
15 |
|
16 |
diff --git a/dev-lang/lean/lean-3.33.0.ebuild b/dev-lang/lean/lean-3.33.0.ebuild |
17 |
index 120a2ac2e..ade8a9dae 100644 |
18 |
--- a/dev-lang/lean/lean-3.33.0.ebuild |
19 |
+++ b/dev-lang/lean/lean-3.33.0.ebuild |
20 |
@@ -5,7 +5,7 @@ EAPI=7 |
21 |
|
22 |
CMAKE_IN_SOURCE_BUILD="ON" |
23 |
|
24 |
-inherit cmake |
25 |
+inherit cmake optfeature |
26 |
|
27 |
DESCRIPTION="The Lean Theorem Prover" |
28 |
HOMEPAGE="https://leanprover-community.github.io/" |
29 |
@@ -40,6 +40,12 @@ src_configure() { |
30 |
} |
31 |
|
32 |
pkg_postinst() { |
33 |
- elog "You probably want to use lean with mathlib, to install it use leanpkg." |
34 |
- elog "For example: leanpkg install https://github.com/leanprover-community/mathlib" |
35 |
+ elog "You probably want to use lean with mathlib, to install it you can either:" |
36 |
+ elog " - Do not install mathlib globally and use local versions" |
37 |
+ elog " - Use leanproject from sci-mathematics/mathlib-tools" |
38 |
+ elog " $ leanproject global-install" |
39 |
+ elog " - Use leanpkg and compile mathlib (which will take long time)" |
40 |
+ elog " $ leanpkg install https://github.com/leanprover-community/mathlib" |
41 |
+ |
42 |
+ optfeature "project management with leanproject" sci-mathematics/mathlib-tools |
43 |
} |