[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/

[Maciej Barć]

commit:     0ceb76e690bd355afa6d84a9d2f2ebcaec422baa
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Fri Nov 26 14:04:04 2021 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Fri Nov 26 14:16:41 2021 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0ceb76e6

sci-mathematics/lean: always use non-hardcoded MAJOR; use readme.gentoo

Package-Manager: Portage-3.0.28, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 .../{lean-3.35.1.ebuild => lean-3.35.1-r1.ebuild}  | 25 ++++++++++++++--------
 1 file changed, 16 insertions(+), 9 deletions(-)

diff --git a/sci-mathematics/lean/lean-3.35.1.ebuild 
b/sci-mathematics/lean/lean-3.35.1-r1.ebuild
similarity index 69%
rename from sci-mathematics/lean/lean-3.35.1.ebuild
rename to sci-mathematics/lean/lean-3.35.1-r1.ebuild
index 71e0662ac80e..cc208dc27850 100644
--- a/sci-mathematics/lean/lean-3.35.1.ebuild
+++ b/sci-mathematics/lean/lean-3.35.1-r1.ebuild
@@ -3,19 +3,18 @@
 
 EAPI=8
 
+MAJOR=$(ver_cut 1)
 CMAKE_IN_SOURCE_BUILD="ON"
 
-inherit cmake optfeature
+inherit cmake optfeature readme.gentoo-r1
 
 DESCRIPTION="The Lean Theorem Prover"
 HOMEPAGE="https://leanprover-community.github.io/";
 
 if [[ "${PV}" == *9999* ]]; then
-       MAJOR=3  # sync this periodically for the live version
        inherit git-r3
        EGIT_REPO_URI="https://github.com/leanprover-community/lean.git";
 else
-       MAJOR=$(ver_cut 1)
        
SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz
 -> ${P}.tar.gz"
        KEYWORDS="~amd64 ~x86"
 fi
@@ -58,11 +57,19 @@ src_test() {
        cmake_src_test
 }
 
+src_install() {
+       cmake_src_install
+
+       local DISABLE_AUTOFORMATTING="yes"
+       local DOC_CONTENTS="You probably want to use lean with mathlib, you can 
either:
+       - Do not install mathlib globally and use local versions
+       - Use leanproject from sci-mathematics/mathlib-tools
+               $ leanproject global-install
+       - Use leanpkg and compile mathlib (which will take some time)
+               $ leanpkg install 
https://github.com/leanprover-community/mathlib";
+       readme.gentoo_create_doc
+}
+
 pkg_postinst() {
-       elog "You probably want to use lean with mathlib, 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 some time)"
-       elog "   $ leanpkg install 
https://github.com/leanprover-community/mathlib";
+       readme.gentoo_print_elog
 }