sci-mathematics/lean: bump to 3.49.1

Signed-off-by: Maciej Barć <xgqt@gentoo.org>

2 files changed, 78 insertions, 0 deletions

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index bd291d742f31..0f3179c248a3 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.47.0.tar.gz 1917990 BLAKE2B 1249654b3a71d1a3b601c79915232d5f53335cd4a5b3c41f97dd5cb39e86bc5ea3c4208b5ebca9fae43c01b7da64579cdf6bcec12b8861ca69339277efe7431d SHA512 11879e4bc324e036b917af0761d918eb393aa3226a36b305dbcd233988504178082290dab2d2e25bc3b7732cb5246a397e29fbd4c956efa9ea454cb46568d942
 DIST lean-3.48.0.tar.gz 1918012 BLAKE2B 4616af2e4d66c56866f321797d6bb05049925f62c2c62c72a3a5552d39cc83c48c1dc2e59b9d81a7341346ed6f3173ef6e69902b8e8a5a24c4af86dace76360b SHA512 9e017484f88fac40e35604643c972d5f316df70c18b00f90b107d994f5e58eeb0637033354c1e0159a9dfc8c72fe3ea9d3b70569b46fc37b22a94c3d7445cdac
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
+DIST lean-3.49.1.tar.gz 1918165 BLAKE2B bebb29023f7d8979dae19d7c5ef6503be03012366c8a4f21a69244a1daadf90c73e8a8754656d7b1a6eccb1123f0905f3dcaa15885b0307399979024d2c5a051 SHA512 6648ab84840099495df5bec9432c75c40fc0920ac2a18297b42c35de593ec4eaee8bcf807cb6e273c2715090e5d1ab6c59652f482016af68d758e7e6e55dd87f
diff --git a/sci-mathematics/lean/lean-3.49.1.ebuild b/sci-mathematics/lean/lean-3.49.1.ebuild
new file mode 100644
index 000000000000..e008b81cf582
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.49.1.ebuild
@@ -0,0 +1,77 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+MAJOR=$(ver_cut 1)
+CMAKE_IN_SOURCE_BUILD="ON"
+
+inherit flag-o-matic cmake readme.gentoo-r1
+
+DESCRIPTION="The Lean Theorem Prover"
+HOMEPAGE="https://leanprover-community.github.io/"
+
+if [[ ${PV} == *9999* ]] ; then
+	inherit git-r3
+	EGIT_REPO_URI="https://github.com/leanprover-community/lean.git"
+else
+	SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz"
+	KEYWORDS="~amd64 ~x86"
+fi
+S="${S}/src"
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug +threads"
+
+RDEPEND="dev-libs/gmp:="
+DEPEND="${RDEPEND}"
+
+PATCHES=( "${FILESDIR}"/${PN}-CMakeLists-fix_flags.patch )
+
+src_configure() {
+	local CMAKE_BUILD_TYPE
+	if use debug; then
+		CMAKE_BUILD_TYPE="Debug"
+	else
+		CMAKE_BUILD_TYPE="Release"
+	fi
+
+	filter-lto
+
+	local mycmakeargs=(
+		-DALPHA=ON
+		-DAUTO_THREAD_FINALIZATION=ON
+		-DJSON=ON  # bug 833900
+		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
+		-DMULTI_THREAD=$(usex threads)
+		-DUSE_GITHASH=OFF
+	)
+	cmake_src_configure
+}
+
+src_test() {
+	local myctestargs=(
+		# Disable problematic "style_check" cpplint test,
+		# this also removes the python test dependency
+		--exclude-regex style_check
+	)
+	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() {
+	readme.gentoo_print_elog
+}