summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaciej Barć <xgqt@gentoo.org>2021-11-26 15:04:04 +0100
committerMaciej Barć <xgqt@gentoo.org>2021-11-26 15:16:41 +0100
commit0ceb76e690bd355afa6d84a9d2f2ebcaec422baa (patch)
tree5565b5ca24b0e78050bee3fb7c297ac82550b4d8 /sci-mathematics
parentnet-mail/dovecot: bump to 2.3.17 (diff)
downloadgentoo-0ceb76e690bd355afa6d84a9d2f2ebcaec422baa.tar.gz
gentoo-0ceb76e690bd355afa6d84a9d2f2ebcaec422baa.tar.bz2
gentoo-0ceb76e690bd355afa6d84a9d2f2ebcaec422baa.zip
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@gentoo.org>
Diffstat (limited to 'sci-mathematics')
-rw-r--r--sci-mathematics/lean/lean-3.35.1-r1.ebuild (renamed from sci-mathematics/lean/lean-3.35.1.ebuild)25
1 files 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
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
}