1 |
commit: 0ceb76e690bd355afa6d84a9d2f2ebcaec422baa |
2 |
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org> |
3 |
AuthorDate: Fri Nov 26 14:04:04 2021 +0000 |
4 |
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org> |
5 |
CommitDate: Fri Nov 26 14:16:41 2021 +0000 |
6 |
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0ceb76e6 |
7 |
|
8 |
sci-mathematics/lean: always use non-hardcoded MAJOR; use readme.gentoo |
9 |
|
10 |
Package-Manager: Portage-3.0.28, Repoman-3.0.3 |
11 |
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org> |
12 |
|
13 |
.../{lean-3.35.1.ebuild => lean-3.35.1-r1.ebuild} | 25 ++++++++++++++-------- |
14 |
1 file changed, 16 insertions(+), 9 deletions(-) |
15 |
|
16 |
diff --git a/sci-mathematics/lean/lean-3.35.1.ebuild b/sci-mathematics/lean/lean-3.35.1-r1.ebuild |
17 |
similarity index 69% |
18 |
rename from sci-mathematics/lean/lean-3.35.1.ebuild |
19 |
rename to sci-mathematics/lean/lean-3.35.1-r1.ebuild |
20 |
index 71e0662ac80e..cc208dc27850 100644 |
21 |
--- a/sci-mathematics/lean/lean-3.35.1.ebuild |
22 |
+++ b/sci-mathematics/lean/lean-3.35.1-r1.ebuild |
23 |
@@ -3,19 +3,18 @@ |
24 |
|
25 |
EAPI=8 |
26 |
|
27 |
+MAJOR=$(ver_cut 1) |
28 |
CMAKE_IN_SOURCE_BUILD="ON" |
29 |
|
30 |
-inherit cmake optfeature |
31 |
+inherit cmake optfeature readme.gentoo-r1 |
32 |
|
33 |
DESCRIPTION="The Lean Theorem Prover" |
34 |
HOMEPAGE="https://leanprover-community.github.io/" |
35 |
|
36 |
if [[ "${PV}" == *9999* ]]; then |
37 |
- MAJOR=3 # sync this periodically for the live version |
38 |
inherit git-r3 |
39 |
EGIT_REPO_URI="https://github.com/leanprover-community/lean.git" |
40 |
else |
41 |
- MAJOR=$(ver_cut 1) |
42 |
SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz" |
43 |
KEYWORDS="~amd64 ~x86" |
44 |
fi |
45 |
@@ -58,11 +57,19 @@ src_test() { |
46 |
cmake_src_test |
47 |
} |
48 |
|
49 |
+src_install() { |
50 |
+ cmake_src_install |
51 |
+ |
52 |
+ local DISABLE_AUTOFORMATTING="yes" |
53 |
+ local DOC_CONTENTS="You probably want to use lean with mathlib, you can either: |
54 |
+ - Do not install mathlib globally and use local versions |
55 |
+ - Use leanproject from sci-mathematics/mathlib-tools |
56 |
+ $ leanproject global-install |
57 |
+ - Use leanpkg and compile mathlib (which will take some time) |
58 |
+ $ leanpkg install https://github.com/leanprover-community/mathlib" |
59 |
+ readme.gentoo_create_doc |
60 |
+} |
61 |
+ |
62 |
pkg_postinst() { |
63 |
- elog "You probably want to use lean with mathlib, you can either:" |
64 |
- elog " - Do not install mathlib globally and use local versions" |
65 |
- elog " - Use leanproject from sci-mathematics/mathlib-tools" |
66 |
- elog " $ leanproject global-install" |
67 |
- elog " - Use leanpkg and compile mathlib (which will take some time)" |
68 |
- elog " $ leanpkg install https://github.com/leanprover-community/mathlib" |
69 |
+ readme.gentoo_print_elog |
70 |
} |