From 0ceb76e690bd355afa6d84a9d2f2ebcaec422baa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maciej=20Bar=C4=87?= <xgqt@gentoo.org>
Date: Fri, 26 Nov 2021 15:04:04 +0100
Subject: [PATCH] sci-mathematics/lean: always use non-hardcoded MAJOR; use
 readme.gentoo
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Package-Manager: Portage-3.0.28, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
---
 ...an-3.35.1.ebuild => lean-3.35.1-r1.ebuild} | 27 ++++++++++++-------
 1 file changed, 17 insertions(+), 10 deletions(-)
 rename sci-mathematics/lean/{lean-3.35.1.ebuild => lean-3.35.1-r1.ebuild} (69%)

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 71e0662ac80e9..cc208dc278500 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
 }
 
-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"
+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() {
+	readme.gentoo_print_elog
 }