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

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

[Maciej Barć]

commit:     2d71d221298ddf5a54541872cfdb99799e1246d6
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Wed May 18 19:13:55 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Wed May 18 19:29:55 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2d71d221

sci-mathematics/lean: bump to 3.43.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.43.0.ebuild | 75 +++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 41cd0f0901a9..8821361f03b5 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -2,3 +2,4 @@ DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0e
 DIST lean-3.41.0.tar.gz 1905966 BLAKE2B 1921ba4a975ed8fc6001695151bb366341e0895989a570bb7fbef1e719685945d0b7c51ed0716ff29daaf81af24ce2e289cab41b251c686a286cd94a0cf708f8 SHA512 855a56812ba5dc7cf431490957570d0fcbc4760faa1602095e708ddcc4e5a3c6aeac42133c210375d4538d97c8ae90df3ab3c7e7840e8896b8d0db439e925fbf
 DIST lean-3.42.0.tar.gz 1908134 BLAKE2B 7b6403786cc1a3a2b974f8df4c2bf2921e4e374ead4290a0e263c8464a9c009fd2f62e7cf5bdbc5087d0c9bb4c57f798b9d1a4b8ee2d66152714ec2af649e196 SHA512 2f1fc1bf3aff7fa806e1cd4647380d6896d98a9191f2035d5a37cc35938de42b243188984aa2fced37bdbee3b2c3c6ef25d27bf2428bf9a0307cc3237c80560f
 DIST lean-3.42.1.tar.gz 1908398 BLAKE2B 7a83269deb3dc7ee60bf7a09b36df332355d9caf575b8435345956697121e95e1fb44cada1237e44bab04a56af4fb40c0d01e49f4cb3e4896e616f2bc58bf9ef SHA512 ab266e385e3026ce3219eef6ef171e243576e291fb26cef3d97ca4cc5190988e3bd6fe93c37a1192b8d2eec0ae7620131826ee1073a038f5a024e706953242d1
+DIST lean-3.43.0.tar.gz 1909158 BLAKE2B 587995afb123e6c74a730f9709a001bab6b2ac82471dcf8b1219dda782853fcdb9735d16038b95a7950f6530dd3cf1e0b13e4d1044d723d3662217951b809928 SHA512 25cbad94b869bb39edaf9ed2478ffc298b130f22cb4db7c116212546583d670079ddde1b524a33499d00ac43fc82b6928e6801c83d613597aae255db9c45d9f3

diff --git a/sci-mathematics/lean/lean-3.43.0.ebuild b/sci-mathematics/lean/lean-3.43.0.ebuild
new file mode 100644
index 000000000000..5d8ee8eecd4b
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.43.0.ebuild
@@ -0,0 +1,75 @@
+# 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 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="${WORKDIR}/lean-${PV}/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
+
+	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
+}

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

[Maciej Barć]

commit:     77d2f42c3147d7db0e30b8d0b1483bd512e9861f
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Sep 19 14:39:00 2024 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Sep 19 22:01:39 2024 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=77d2f42c

sci-mathematics/lean: drop ~x86 KEYWORD

Closes: https://bugs.gentoo.org/917789
Closes: https://bugs.gentoo.org/928093
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 sci-mathematics/lean/lean-4.2.0.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/lean/lean-4.2.0.ebuild b/sci-mathematics/lean/lean-4.2.0.ebuild
index a19134fbaf2e..4f9f3b199ff1 100644
--- a/sci-mathematics/lean/lean-4.2.0.ebuild
+++ b/sci-mathematics/lean/lean-4.2.0.ebuild
@@ -22,7 +22,7 @@ else
 		-> ${P}.tar.gz"
 	S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"
 
-	KEYWORDS="amd64 ~x86"
+	KEYWORDS="amd64"
 fi
 
 LICENSE="Apache-2.0"

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

[Maciej Barć]

commit:     d88a1ae9ef4b750d5fc037faf997dd5c55a75500
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Sep 19 22:00:38 2024 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Sep 19 22:01:39 2024 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=d88a1ae9

sci-mathematics/lean: bump to 4.11.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-4.11.0.ebuild | 81 +++++++++++++++++++++++++++++++++
 2 files changed, 82 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 9354c00ca642..0a4a177afa1f 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,2 +1,3 @@
 DIST lean-3.51.1.tar.gz 1918894 BLAKE2B 9a240fe73193794a57001582c0623052cfc1c08ef3b155cac2d9dfc029202cb79b85e844fdf068e454498a35522ec3e18330da8c644bba3c6f708cbde04816f7 SHA512 dccdf6c3fbcd98115e62b9944645af6a2ce21412d63baa9565871807862e8d83cc6f29d1fb687f19b802240a5f9c019443caa00412ecfabe621744dff900e3ee
+DIST lean-4.11.0.tar.gz 25790812 BLAKE2B d9a4eb15199f81c6757acf35fb17c795bb9d69158c7e7deb11d98a45bebf569dcda5f7733b2effd2be0eea879a6c7c24b270d97159e5898215e82e853320918c SHA512 2314659910b4d872c4ae0dda648a9cab9e1cc44cd4c55486a494b65b20fdae236ab9db99a42d7fb1a80030e300e95606065ee7dd27578b12a4c47fc8c102e2bb
 DIST lean-4.2.0.tar.gz 16382466 BLAKE2B 3a8770d92ae89041f3e12089c3bb9171a993e8a1c702162925b569e13ed8d8819b3e9aa3c00e314a80a118ff8e4b18fb6df8b8a0e85a21fcb1daa5c0bfc29d4f SHA512 b0bd91f39319c1c6fd6851732d9dcb8758734500abc8faf0648c03582a81d51f2d942fa5deecedf81116b894d0b65e93eccab557bf155e69d65bda83eccaf7bb

diff --git a/sci-mathematics/lean/lean-4.11.0.ebuild b/sci-mathematics/lean/lean-4.11.0.ebuild
new file mode 100644
index 000000000000..88456a89f156
--- /dev/null
+++ b/sci-mathematics/lean/lean-4.11.0.ebuild
@@ -0,0 +1,81 @@
+# Copyright 1999-2024 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+MAJOR="$(ver_cut 1)"
+
+CMAKE_MAKEFILE_GENERATOR="emake"
+PYTHON_COMPAT=( python3_{10..13} )
+
+inherit cmake flag-o-matic python-any-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/${PN}${MAJOR}.git"
+else
+	SRC_URI="https://github.com/leanprover/${PN}${MAJOR}/archive/refs/tags/v${PV/_/-}.tar.gz
+		-> ${P}.tar.gz"
+	S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"
+
+	KEYWORDS="~amd64"
+fi
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug source"
+
+RDEPEND="
+	dev-libs/gmp:=
+"
+DEPEND="
+	${RDEPEND}
+"
+BDEPEND="
+	${PYTHON_DEPS}
+"
+
+# Built by lean's build tool.
+QA_FLAGS_IGNORED="usr/lib/lean/libInit_shared.so"
+
+pkg_setup() {
+	python-any-r1_pkg_setup
+}
+
+src_prepare() {
+	filter-lto
+
+	sed -e "s|-O[23]|${CFLAGS}|g" -i src/CMakeLists.txt || die
+
+	cmake_src_prepare
+}
+
+src_configure() {
+	local CMAKE_BUILD_TYPE
+
+	if use debug ; then
+		CMAKE_BUILD_TYPE="Debug"
+	else
+		CMAKE_BUILD_TYPE="Release"
+	fi
+
+	local -a mycmakeargs=(
+		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
+		-DLEAN_EXTRA_LINKER_FLAGS="${LDFLAGS}"
+	)
+	cmake_src_configure
+}
+
+src_install() {
+	cmake_src_install
+
+	rm "${ED}/usr/LICENSE"* || die
+
+	if ! use source ; then
+		rm -r "${ED}/usr/src" || die
+	fi
+}

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

[Sam James]

commit:     15dff3a1f5bd74ef84c1f6679be0a464418c60ff
Author:     Sam James <sam <AT> gentoo <DOT> org>
AuthorDate: Thu Jan 18 17:23:39 2024 +0000
Commit:     Sam James <sam <AT> gentoo <DOT> org>
CommitDate: Thu Jan 18 17:23:39 2024 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=15dff3a1

sci-mathematics/lean: Stabilize 4.2.0 amd64, #922367

Signed-off-by: Sam James <sam <AT> gentoo.org>

 sci-mathematics/lean/lean-4.2.0.ebuild | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/lean/lean-4.2.0.ebuild b/sci-mathematics/lean/lean-4.2.0.ebuild
index 30fd5379373b..a19134fbaf2e 100644
--- a/sci-mathematics/lean/lean-4.2.0.ebuild
+++ b/sci-mathematics/lean/lean-4.2.0.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2023 Gentoo Authors
+# Copyright 1999-2024 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=8
@@ -22,7 +22,7 @@ else
 		-> ${P}.tar.gz"
 	S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"
 
-	KEYWORDS="~amd64 ~x86"
+	KEYWORDS="amd64 ~x86"
 fi
 
 LICENSE="Apache-2.0"

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

[Maciej Barć]

commit:     c424b1a0464033e5499ea963860773dbf0fea6a0
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Mon Jan 15 20:10:03 2024 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Mon Jan 15 21:20:41 2024 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c424b1a0

sci-mathematics/lean: drop old 4.2.0_rc4

Closes: https://bugs.gentoo.org/916306
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 sci-mathematics/lean/Manifest              |  1 -
 sci-mathematics/lean/lean-4.2.0_rc4.ebuild | 78 ------------------------------
 2 files changed, 79 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index c1fe00f2288d..9354c00ca642 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,2 @@
 DIST lean-3.51.1.tar.gz 1918894 BLAKE2B 9a240fe73193794a57001582c0623052cfc1c08ef3b155cac2d9dfc029202cb79b85e844fdf068e454498a35522ec3e18330da8c644bba3c6f708cbde04816f7 SHA512 dccdf6c3fbcd98115e62b9944645af6a2ce21412d63baa9565871807862e8d83cc6f29d1fb687f19b802240a5f9c019443caa00412ecfabe621744dff900e3ee
 DIST lean-4.2.0.tar.gz 16382466 BLAKE2B 3a8770d92ae89041f3e12089c3bb9171a993e8a1c702162925b569e13ed8d8819b3e9aa3c00e314a80a118ff8e4b18fb6df8b8a0e85a21fcb1daa5c0bfc29d4f SHA512 b0bd91f39319c1c6fd6851732d9dcb8758734500abc8faf0648c03582a81d51f2d942fa5deecedf81116b894d0b65e93eccab557bf155e69d65bda83eccaf7bb
-DIST lean-4.2.0_rc4.tar.gz 16386559 BLAKE2B 4eb0bb47cd09ec7ccb04870a08b13c8b9c73a296b42e9c92c9f9885dfe416e75352db7c41725446dd27a0a9a68f3979fa91dadb93aba1af1321df94312d7fa99 SHA512 4d08bf182eb3822f12ec69af9aa0527581fe7f3ff4a10836b866622146b3572ced3635fdf0179a8764d233de427094f47219d619d205971794b41f1c1fc4b06d

diff --git a/sci-mathematics/lean/lean-4.2.0_rc4.ebuild b/sci-mathematics/lean/lean-4.2.0_rc4.ebuild
deleted file mode 100644
index 30fd5379373b..000000000000
--- a/sci-mathematics/lean/lean-4.2.0_rc4.ebuild
+++ /dev/null
@@ -1,78 +0,0 @@
-# Copyright 1999-2023 Gentoo Authors
-# Distributed under the terms of the GNU General Public License v2
-
-EAPI=8
-
-MAJOR="$(ver_cut 1)"
-
-CMAKE_MAKEFILE_GENERATOR="emake"
-PYTHON_COMPAT=( python3_{10..12} )
-
-inherit cmake flag-o-matic python-any-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/${PN}${MAJOR}.git"
-else
-	SRC_URI="https://github.com/leanprover/${PN}${MAJOR}/archive/refs/tags/v${PV/_/-}.tar.gz
-		-> ${P}.tar.gz"
-	S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"
-
-	KEYWORDS="~amd64 ~x86"
-fi
-
-LICENSE="Apache-2.0"
-SLOT="0/${MAJOR}"
-IUSE="debug source"
-
-RDEPEND="
-	dev-libs/gmp:=
-"
-DEPEND="
-	${RDEPEND}
-"
-BDEPEND="
-	${PYTHON_DEPS}
-"
-
-pkg_setup() {
-	python-any-r1_pkg_setup
-}
-
-src_prepare() {
-	filter-lto
-
-	sed -e "s|-O[23]|${CFLAGS}|g" -i src/CMakeLists.txt || die
-
-	cmake_src_prepare
-}
-
-src_configure() {
-	local CMAKE_BUILD_TYPE
-
-	if use debug ; then
-		CMAKE_BUILD_TYPE="Debug"
-	else
-		CMAKE_BUILD_TYPE="Release"
-	fi
-
-	local -a mycmakeargs=(
-		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
-		-DLEAN_EXTRA_LINKER_FLAGS="${LDFLAGS}"
-	)
-	cmake_src_configure
-}
-
-src_install() {
-	cmake_src_install
-
-	rm "${ED}/usr/LICENSE"* || die
-
-	if ! use source ; then
-		rm -r "${ED}/usr/src" || die
-	fi
-}

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

[Maciej Barć]

commit:     b6d29d865fb76d54ffbae7eefa32b2ac04a5cff1
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Nov 30 09:46:49 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Nov 30 16:52:25 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=b6d29d86

sci-mathematics/lean: bump to 4.2.0

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

 sci-mathematics/lean/Manifest          |  1 +
 sci-mathematics/lean/lean-4.2.0.ebuild | 78 ++++++++++++++++++++++++++++++++++
 2 files changed, 79 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 68f2783a3dfd..c1fe00f2288d 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,2 +1,3 @@
 DIST lean-3.51.1.tar.gz 1918894 BLAKE2B 9a240fe73193794a57001582c0623052cfc1c08ef3b155cac2d9dfc029202cb79b85e844fdf068e454498a35522ec3e18330da8c644bba3c6f708cbde04816f7 SHA512 dccdf6c3fbcd98115e62b9944645af6a2ce21412d63baa9565871807862e8d83cc6f29d1fb687f19b802240a5f9c019443caa00412ecfabe621744dff900e3ee
+DIST lean-4.2.0.tar.gz 16382466 BLAKE2B 3a8770d92ae89041f3e12089c3bb9171a993e8a1c702162925b569e13ed8d8819b3e9aa3c00e314a80a118ff8e4b18fb6df8b8a0e85a21fcb1daa5c0bfc29d4f SHA512 b0bd91f39319c1c6fd6851732d9dcb8758734500abc8faf0648c03582a81d51f2d942fa5deecedf81116b894d0b65e93eccab557bf155e69d65bda83eccaf7bb
 DIST lean-4.2.0_rc4.tar.gz 16386559 BLAKE2B 4eb0bb47cd09ec7ccb04870a08b13c8b9c73a296b42e9c92c9f9885dfe416e75352db7c41725446dd27a0a9a68f3979fa91dadb93aba1af1321df94312d7fa99 SHA512 4d08bf182eb3822f12ec69af9aa0527581fe7f3ff4a10836b866622146b3572ced3635fdf0179a8764d233de427094f47219d619d205971794b41f1c1fc4b06d

diff --git a/sci-mathematics/lean/lean-4.2.0.ebuild b/sci-mathematics/lean/lean-4.2.0.ebuild
new file mode 100644
index 000000000000..30fd5379373b
--- /dev/null
+++ b/sci-mathematics/lean/lean-4.2.0.ebuild
@@ -0,0 +1,78 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+MAJOR="$(ver_cut 1)"
+
+CMAKE_MAKEFILE_GENERATOR="emake"
+PYTHON_COMPAT=( python3_{10..12} )
+
+inherit cmake flag-o-matic python-any-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/${PN}${MAJOR}.git"
+else
+	SRC_URI="https://github.com/leanprover/${PN}${MAJOR}/archive/refs/tags/v${PV/_/-}.tar.gz
+		-> ${P}.tar.gz"
+	S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"
+
+	KEYWORDS="~amd64 ~x86"
+fi
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug source"
+
+RDEPEND="
+	dev-libs/gmp:=
+"
+DEPEND="
+	${RDEPEND}
+"
+BDEPEND="
+	${PYTHON_DEPS}
+"
+
+pkg_setup() {
+	python-any-r1_pkg_setup
+}
+
+src_prepare() {
+	filter-lto
+
+	sed -e "s|-O[23]|${CFLAGS}|g" -i src/CMakeLists.txt || die
+
+	cmake_src_prepare
+}
+
+src_configure() {
+	local CMAKE_BUILD_TYPE
+
+	if use debug ; then
+		CMAKE_BUILD_TYPE="Debug"
+	else
+		CMAKE_BUILD_TYPE="Release"
+	fi
+
+	local -a mycmakeargs=(
+		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
+		-DLEAN_EXTRA_LINKER_FLAGS="${LDFLAGS}"
+	)
+	cmake_src_configure
+}
+
+src_install() {
+	cmake_src_install
+
+	rm "${ED}/usr/LICENSE"* || die
+
+	if ! use source ; then
+		rm -r "${ED}/usr/src" || die
+	fi
+}

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

[Maciej Barć]

commit:     2ebcc7f39c3ec50ee080478c0651a13b753b0e90
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Oct 26 10:06:36 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Oct 26 13:11:35 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2ebcc7f3

sci-mathematics/lean: bump to 4.2.0_rc4

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

 sci-mathematics/lean/Manifest              |  1 +
 sci-mathematics/lean/lean-4.2.0_rc4.ebuild | 78 ++++++++++++++++++++++++++++++
 2 files changed, 79 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index e1665cbf90b6..68f2783a3dfd 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1 +1,2 @@
 DIST lean-3.51.1.tar.gz 1918894 BLAKE2B 9a240fe73193794a57001582c0623052cfc1c08ef3b155cac2d9dfc029202cb79b85e844fdf068e454498a35522ec3e18330da8c644bba3c6f708cbde04816f7 SHA512 dccdf6c3fbcd98115e62b9944645af6a2ce21412d63baa9565871807862e8d83cc6f29d1fb687f19b802240a5f9c019443caa00412ecfabe621744dff900e3ee
+DIST lean-4.2.0_rc4.tar.gz 16386559 BLAKE2B 4eb0bb47cd09ec7ccb04870a08b13c8b9c73a296b42e9c92c9f9885dfe416e75352db7c41725446dd27a0a9a68f3979fa91dadb93aba1af1321df94312d7fa99 SHA512 4d08bf182eb3822f12ec69af9aa0527581fe7f3ff4a10836b866622146b3572ced3635fdf0179a8764d233de427094f47219d619d205971794b41f1c1fc4b06d

diff --git a/sci-mathematics/lean/lean-4.2.0_rc4.ebuild b/sci-mathematics/lean/lean-4.2.0_rc4.ebuild
new file mode 100644
index 000000000000..30fd5379373b
--- /dev/null
+++ b/sci-mathematics/lean/lean-4.2.0_rc4.ebuild
@@ -0,0 +1,78 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+MAJOR="$(ver_cut 1)"
+
+CMAKE_MAKEFILE_GENERATOR="emake"
+PYTHON_COMPAT=( python3_{10..12} )
+
+inherit cmake flag-o-matic python-any-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/${PN}${MAJOR}.git"
+else
+	SRC_URI="https://github.com/leanprover/${PN}${MAJOR}/archive/refs/tags/v${PV/_/-}.tar.gz
+		-> ${P}.tar.gz"
+	S="${WORKDIR}/${PN}${MAJOR}-${PV/_/-}"
+
+	KEYWORDS="~amd64 ~x86"
+fi
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug source"
+
+RDEPEND="
+	dev-libs/gmp:=
+"
+DEPEND="
+	${RDEPEND}
+"
+BDEPEND="
+	${PYTHON_DEPS}
+"
+
+pkg_setup() {
+	python-any-r1_pkg_setup
+}
+
+src_prepare() {
+	filter-lto
+
+	sed -e "s|-O[23]|${CFLAGS}|g" -i src/CMakeLists.txt || die
+
+	cmake_src_prepare
+}
+
+src_configure() {
+	local CMAKE_BUILD_TYPE
+
+	if use debug ; then
+		CMAKE_BUILD_TYPE="Debug"
+	else
+		CMAKE_BUILD_TYPE="Release"
+	fi
+
+	local -a mycmakeargs=(
+		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
+		-DLEAN_EXTRA_LINKER_FLAGS="${LDFLAGS}"
+	)
+	cmake_src_configure
+}
+
+src_install() {
+	cmake_src_install
+
+	rm "${ED}/usr/LICENSE"* || die
+
+	if ! use source ; then
+		rm -r "${ED}/usr/src" || die
+	fi
+}

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

[Maciej Barć]

commit:     0a9f17ccefbfe98fa6b5d3698f412e4def72048b
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Wed Oct 25 20:03:32 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Oct 26 13:11:35 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0a9f17cc

sci-mathematics/lean: drop old 3.9999

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

 sci-mathematics/lean/lean-3.9999.ebuild | 80 ---------------------------------
 1 file changed, 80 deletions(-)

diff --git a/sci-mathematics/lean/lean-3.9999.ebuild b/sci-mathematics/lean/lean-3.9999.ebuild
deleted file mode 100644
index 72a23985077c..000000000000
--- a/sci-mathematics/lean/lean-3.9999.ebuild
+++ /dev/null
@@ -1,80 +0,0 @@
-# Copyright 1999-2023 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}-3.50.3-gcc-13.patch
-	"${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 -a 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 -a 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
-}

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

[Maciej Barć]

commit:     fa16ba57a6b933ac4c43fb6cffa5c3299fafa616
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Oct  7 14:53:08 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Oct  7 14:57:43 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=fa16ba57

sci-mathematics/lean: drop old 3.50.3

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.50.3.ebuild | 80 ---------------------------------
 2 files changed, 81 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 2feb241896bf..6b3c53361c64 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,2 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
-DIST lean-3.50.3.tar.gz 1918462 BLAKE2B f8cb3857989e4966c12a9b4f4a13403ceab0ae9d33ddf81970ef886fb1f46bfd14bfc15aea498ea360cc801224c60489f0ce3b33fe10bead4dcbf3f6a06eee93 SHA512 849b9e8854585ce119f87e8bea655bcb834f1f986bccbf5ffa148fd4a1aae2030b6be938adbf377f0076361a3d9338802e1af8965f01b9c4d2a0517be330beef
 DIST lean-3.51.1.tar.gz 1918894 BLAKE2B 9a240fe73193794a57001582c0623052cfc1c08ef3b155cac2d9dfc029202cb79b85e844fdf068e454498a35522ec3e18330da8c644bba3c6f708cbde04816f7 SHA512 dccdf6c3fbcd98115e62b9944645af6a2ce21412d63baa9565871807862e8d83cc6f29d1fb687f19b802240a5f9c019443caa00412ecfabe621744dff900e3ee

diff --git a/sci-mathematics/lean/lean-3.50.3.ebuild b/sci-mathematics/lean/lean-3.50.3.ebuild
deleted file mode 100644
index 6c8c7551d8ef..000000000000
--- a/sci-mathematics/lean/lean-3.50.3.ebuild
+++ /dev/null
@@ -1,80 +0,0 @@
-# Copyright 1999-2023 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}-3.50.3-gcc-13.patch
-	"${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 -a 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 -a 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
-}

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

[Maciej Barć]

commit:     a34aff2a52124ee5a1ff2c7d8e01aadbc9a55254
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Oct  7 14:53:12 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Oct  7 14:57:43 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=a34aff2a

sci-mathematics/lean: drop old 3.49.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.49.0.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 6b3c53361c64..e1665cbf90b6 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,2 +1 @@
-DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
 DIST lean-3.51.1.tar.gz 1918894 BLAKE2B 9a240fe73193794a57001582c0623052cfc1c08ef3b155cac2d9dfc029202cb79b85e844fdf068e454498a35522ec3e18330da8c644bba3c6f708cbde04816f7 SHA512 dccdf6c3fbcd98115e62b9944645af6a2ce21412d63baa9565871807862e8d83cc6f29d1fb687f19b802240a5f9c019443caa00412ecfabe621744dff900e3ee

diff --git a/sci-mathematics/lean/lean-3.49.0.ebuild b/sci-mathematics/lean/lean-3.49.0.ebuild
deleted file mode 100644
index 08920adac95a..000000000000
--- a/sci-mathematics/lean/lean-3.49.0.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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
-}

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

[Maciej Barć]

commit:     479d6e498b77704daeaa13b6643c00bb1915aea5
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Oct  7 14:53:03 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Oct  7 14:57:42 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=479d6e49

sci-mathematics/lean: drop old 3.51.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.51.0.ebuild | 80 ---------------------------------
 2 files changed, 81 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index a7e68689fb92..2feb241896bf 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
 DIST lean-3.50.3.tar.gz 1918462 BLAKE2B f8cb3857989e4966c12a9b4f4a13403ceab0ae9d33ddf81970ef886fb1f46bfd14bfc15aea498ea360cc801224c60489f0ce3b33fe10bead4dcbf3f6a06eee93 SHA512 849b9e8854585ce119f87e8bea655bcb834f1f986bccbf5ffa148fd4a1aae2030b6be938adbf377f0076361a3d9338802e1af8965f01b9c4d2a0517be330beef
-DIST lean-3.51.0.tar.gz 1918905 BLAKE2B 83131417011d89846084608fc9b6b5b8254584da63b2e2d7626064a170c3bd3780973483ce60afc49713df840e150c4ed92951bfd7fbdeb520791e58164313cd SHA512 712c5520d298cf7098f5e5d787ba91096d73ba08a15581f4478836c7790679950a1a0b0d7d9c876b1557ae7dc56b10430ac1b4227b5d30ac1ad398e196c2fb11
 DIST lean-3.51.1.tar.gz 1918894 BLAKE2B 9a240fe73193794a57001582c0623052cfc1c08ef3b155cac2d9dfc029202cb79b85e844fdf068e454498a35522ec3e18330da8c644bba3c6f708cbde04816f7 SHA512 dccdf6c3fbcd98115e62b9944645af6a2ce21412d63baa9565871807862e8d83cc6f29d1fb687f19b802240a5f9c019443caa00412ecfabe621744dff900e3ee

diff --git a/sci-mathematics/lean/lean-3.51.0.ebuild b/sci-mathematics/lean/lean-3.51.0.ebuild
deleted file mode 100644
index 72a23985077c..000000000000
--- a/sci-mathematics/lean/lean-3.51.0.ebuild
+++ /dev/null
@@ -1,80 +0,0 @@
-# Copyright 1999-2023 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}-3.50.3-gcc-13.patch
-	"${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 -a 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 -a 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
-}

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

[Arthur Zamarin]

commit:     ae428f64fdaf392bc0ed57cef1ec5915fdd4d5c2
Author:     Arthur Zamarin <arthurzam <AT> gentoo <DOT> org>
AuthorDate: Tue Aug 15 15:45:33 2023 +0000
Commit:     Arthur Zamarin <arthurzam <AT> gentoo <DOT> org>
CommitDate: Tue Aug 15 15:45:33 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ae428f64

sci-mathematics/lean: Stabilize 3.51.1 amd64, #912297

Signed-off-by: Arthur Zamarin <arthurzam <AT> gentoo.org>

 sci-mathematics/lean/lean-3.51.1.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/lean/lean-3.51.1.ebuild b/sci-mathematics/lean/lean-3.51.1.ebuild
index 72a23985077c..6c8c7551d8ef 100644
--- a/sci-mathematics/lean/lean-3.51.1.ebuild
+++ b/sci-mathematics/lean/lean-3.51.1.ebuild
@@ -16,7 +16,7 @@ if [[ ${PV} == *9999* ]] ; then
 	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"
+	KEYWORDS="amd64 ~x86"
 fi
 S="${S}/src"
 

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

[Sam James]

commit:     0a01120cbca04b48ee8e276775bca1d68184ad51
Author:     Sam James <sam <AT> gentoo <DOT> org>
AuthorDate: Fri May 26 07:14:40 2023 +0000
Commit:     Sam James <sam <AT> gentoo <DOT> org>
CommitDate: Fri May 26 07:14:47 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0a01120c

sci-mathematics/lean: Stabilize 3.50.3 amd64, #907180

Signed-off-by: Sam James <sam <AT> gentoo.org>

 sci-mathematics/lean/lean-3.50.3.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/lean/lean-3.50.3.ebuild b/sci-mathematics/lean/lean-3.50.3.ebuild
index 72a23985077c..6c8c7551d8ef 100644
--- a/sci-mathematics/lean/lean-3.50.3.ebuild
+++ b/sci-mathematics/lean/lean-3.50.3.ebuild
@@ -16,7 +16,7 @@ if [[ ${PV} == *9999* ]] ; then
 	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"
+	KEYWORDS="amd64 ~x86"
 fi
 S="${S}/src"
 

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

[Maciej Barć]

commit:     fe3cf754c1e7031e14cfbe8491fc00e6de38ab81
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Wed May 24 23:15:06 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Wed May 24 23:15:06 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=fe3cf754

sci-mathematics/lean: bump to 3.51.1

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.51.1.ebuild | 80 +++++++++++++++++++++++++++++++++
 2 files changed, 81 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 065df8cd90b3..a7e68689fb92 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
 DIST lean-3.50.3.tar.gz 1918462 BLAKE2B f8cb3857989e4966c12a9b4f4a13403ceab0ae9d33ddf81970ef886fb1f46bfd14bfc15aea498ea360cc801224c60489f0ce3b33fe10bead4dcbf3f6a06eee93 SHA512 849b9e8854585ce119f87e8bea655bcb834f1f986bccbf5ffa148fd4a1aae2030b6be938adbf377f0076361a3d9338802e1af8965f01b9c4d2a0517be330beef
 DIST lean-3.51.0.tar.gz 1918905 BLAKE2B 83131417011d89846084608fc9b6b5b8254584da63b2e2d7626064a170c3bd3780973483ce60afc49713df840e150c4ed92951bfd7fbdeb520791e58164313cd SHA512 712c5520d298cf7098f5e5d787ba91096d73ba08a15581f4478836c7790679950a1a0b0d7d9c876b1557ae7dc56b10430ac1b4227b5d30ac1ad398e196c2fb11
+DIST lean-3.51.1.tar.gz 1918894 BLAKE2B 9a240fe73193794a57001582c0623052cfc1c08ef3b155cac2d9dfc029202cb79b85e844fdf068e454498a35522ec3e18330da8c644bba3c6f708cbde04816f7 SHA512 dccdf6c3fbcd98115e62b9944645af6a2ce21412d63baa9565871807862e8d83cc6f29d1fb687f19b802240a5f9c019443caa00412ecfabe621744dff900e3ee

diff --git a/sci-mathematics/lean/lean-3.51.1.ebuild b/sci-mathematics/lean/lean-3.51.1.ebuild
new file mode 100644
index 000000000000..72a23985077c
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.51.1.ebuild
@@ -0,0 +1,80 @@
+# Copyright 1999-2023 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}-3.50.3-gcc-13.patch
+	"${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 -a 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 -a 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
+}

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

[Maciej Barć]

commit:     2700367b2e05b7d45e0400d13a6d1256206a2300
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Wed May 17 20:21:02 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Wed May 17 20:45:10 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2700367b

sci-mathematics/lean: bump to 3.51.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.51.0.ebuild | 80 +++++++++++++++++++++++++++++++++
 2 files changed, 81 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 38d4ce5c1bcf..065df8cd90b3 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,2 +1,3 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
 DIST lean-3.50.3.tar.gz 1918462 BLAKE2B f8cb3857989e4966c12a9b4f4a13403ceab0ae9d33ddf81970ef886fb1f46bfd14bfc15aea498ea360cc801224c60489f0ce3b33fe10bead4dcbf3f6a06eee93 SHA512 849b9e8854585ce119f87e8bea655bcb834f1f986bccbf5ffa148fd4a1aae2030b6be938adbf377f0076361a3d9338802e1af8965f01b9c4d2a0517be330beef
+DIST lean-3.51.0.tar.gz 1918905 BLAKE2B 83131417011d89846084608fc9b6b5b8254584da63b2e2d7626064a170c3bd3780973483ce60afc49713df840e150c4ed92951bfd7fbdeb520791e58164313cd SHA512 712c5520d298cf7098f5e5d787ba91096d73ba08a15581f4478836c7790679950a1a0b0d7d9c876b1557ae7dc56b10430ac1b4227b5d30ac1ad398e196c2fb11

diff --git a/sci-mathematics/lean/lean-3.51.0.ebuild b/sci-mathematics/lean/lean-3.51.0.ebuild
new file mode 100644
index 000000000000..72a23985077c
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.51.0.ebuild
@@ -0,0 +1,80 @@
+# Copyright 1999-2023 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}-3.50.3-gcc-13.patch
+	"${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 -a 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 -a 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
+}

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

[Maciej Barć]

commit:     0821d9165c3618576c8658be0545906e3b85d9a5
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Apr 18 13:08:13 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Apr 18 13:55:10 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0821d916

sci-mathematics/lean: drop old 3.50.1

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.50.1.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 5e1584ea3d0d..7946cc412e1b 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
-DIST lean-3.50.1.tar.gz 1918323 BLAKE2B 3a26a6481a8472941a928a7b33b24231239e553cd4a4af5671f6a05f1fa68a54657518c4775b641239aa55401100e44c2797d7ae572405225657f1f7da8e193c SHA512 df2e5915e8a7f7e278e2d3472afe6cc23fec5de808b0cc1b20365ad41cfd03b1efda80523059a96c6b3d9b8b0ccab311700ee6a5d6c9751454ebe3b2f168cf77
 DIST lean-3.50.2.tar.gz 1918353 BLAKE2B 2a8c41eef0cc3c2d3e1b45ccd2383279a1a91c0de772c5fe3f1ffafc808db4b6e7342f2f72bd4c4120ed4248d60359c6e331f4adc1d26c6328b284549861c4de SHA512 58d085deb0354db0067e86e6097dad7f1543f356d4e50607b8cc049a19d867aa7ea03553bab3799c6ad18d0ef4fa468b0f966512d8bf0076526f90e93195a407
 DIST lean-3.50.3.tar.gz 1918462 BLAKE2B f8cb3857989e4966c12a9b4f4a13403ceab0ae9d33ddf81970ef886fb1f46bfd14bfc15aea498ea360cc801224c60489f0ce3b33fe10bead4dcbf3f6a06eee93 SHA512 849b9e8854585ce119f87e8bea655bcb834f1f986bccbf5ffa148fd4a1aae2030b6be938adbf377f0076361a3d9338802e1af8965f01b9c4d2a0517be330beef

diff --git a/sci-mathematics/lean/lean-3.50.1.ebuild b/sci-mathematics/lean/lean-3.50.1.ebuild
deleted file mode 100644
index e008b81cf582..000000000000
--- a/sci-mathematics/lean/lean-3.50.1.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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
-}

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

[Maciej Barć]

commit:     794b21a627436b9189d5ac0caede74e2936c5de8
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Apr 18 13:08:18 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Apr 18 13:55:10 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=794b21a6

sci-mathematics/lean: drop old 3.50.2

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.50.2.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 7946cc412e1b..38d4ce5c1bcf 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,2 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
-DIST lean-3.50.2.tar.gz 1918353 BLAKE2B 2a8c41eef0cc3c2d3e1b45ccd2383279a1a91c0de772c5fe3f1ffafc808db4b6e7342f2f72bd4c4120ed4248d60359c6e331f4adc1d26c6328b284549861c4de SHA512 58d085deb0354db0067e86e6097dad7f1543f356d4e50607b8cc049a19d867aa7ea03553bab3799c6ad18d0ef4fa468b0f966512d8bf0076526f90e93195a407
 DIST lean-3.50.3.tar.gz 1918462 BLAKE2B f8cb3857989e4966c12a9b4f4a13403ceab0ae9d33ddf81970ef886fb1f46bfd14bfc15aea498ea360cc801224c60489f0ce3b33fe10bead4dcbf3f6a06eee93 SHA512 849b9e8854585ce119f87e8bea655bcb834f1f986bccbf5ffa148fd4a1aae2030b6be938adbf377f0076361a3d9338802e1af8965f01b9c4d2a0517be330beef

diff --git a/sci-mathematics/lean/lean-3.50.2.ebuild b/sci-mathematics/lean/lean-3.50.2.ebuild
deleted file mode 100644
index e008b81cf582..000000000000
--- a/sci-mathematics/lean/lean-3.50.2.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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
-}

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

[Maciej Barć]

commit:     6ae7758296c1aeb975019f0d0b72ce3aac209512
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Dec 27 02:01:24 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Dec 27 02:01:24 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=6ae77582

sci-mathematics/lean: drop old 3.50.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.50.0.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 02c8c71ff07b..b6598339993f 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
-DIST lean-3.50.0.tar.gz 1918549 BLAKE2B 79827ffb9f825dff040e41e9bcbd8306e2f3a116b74fc6e0831450765d5b896fad2a86ec5dd9e63bf0f8777b575d4ab7ae8d158c233364fad6d4437bc0767452 SHA512 2b8d730ef9d808a24a9708f2b33409510bd6b7350f515679ba0395a45fc2dea2125639cdeb867bec4ac9c8114e448fb9777a69f8859e172f6e694ecacbb07f56
 DIST lean-3.50.1.tar.gz 1918323 BLAKE2B 3a26a6481a8472941a928a7b33b24231239e553cd4a4af5671f6a05f1fa68a54657518c4775b641239aa55401100e44c2797d7ae572405225657f1f7da8e193c SHA512 df2e5915e8a7f7e278e2d3472afe6cc23fec5de808b0cc1b20365ad41cfd03b1efda80523059a96c6b3d9b8b0ccab311700ee6a5d6c9751454ebe3b2f168cf77
 DIST lean-3.50.2.tar.gz 1918353 BLAKE2B 2a8c41eef0cc3c2d3e1b45ccd2383279a1a91c0de772c5fe3f1ffafc808db4b6e7342f2f72bd4c4120ed4248d60359c6e331f4adc1d26c6328b284549861c4de SHA512 58d085deb0354db0067e86e6097dad7f1543f356d4e50607b8cc049a19d867aa7ea03553bab3799c6ad18d0ef4fa468b0f966512d8bf0076526f90e93195a407

diff --git a/sci-mathematics/lean/lean-3.50.0.ebuild b/sci-mathematics/lean/lean-3.50.0.ebuild
deleted file mode 100644
index e008b81cf582..000000000000
--- a/sci-mathematics/lean/lean-3.50.0.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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
-}

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

[Maciej Barć]

commit:     ca603043a7b48df6477fe7addee7dddadfad2664
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Dec 27 02:14:07 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Dec 27 02:14:07 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ca603043

sci-mathematics/lean: bump to 3.50.3

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.50.3.ebuild | 77 +++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index b6598339993f..5e1584ea3d0d 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
 DIST lean-3.50.1.tar.gz 1918323 BLAKE2B 3a26a6481a8472941a928a7b33b24231239e553cd4a4af5671f6a05f1fa68a54657518c4775b641239aa55401100e44c2797d7ae572405225657f1f7da8e193c SHA512 df2e5915e8a7f7e278e2d3472afe6cc23fec5de808b0cc1b20365ad41cfd03b1efda80523059a96c6b3d9b8b0ccab311700ee6a5d6c9751454ebe3b2f168cf77
 DIST lean-3.50.2.tar.gz 1918353 BLAKE2B 2a8c41eef0cc3c2d3e1b45ccd2383279a1a91c0de772c5fe3f1ffafc808db4b6e7342f2f72bd4c4120ed4248d60359c6e331f4adc1d26c6328b284549861c4de SHA512 58d085deb0354db0067e86e6097dad7f1543f356d4e50607b8cc049a19d867aa7ea03553bab3799c6ad18d0ef4fa468b0f966512d8bf0076526f90e93195a407
+DIST lean-3.50.3.tar.gz 1918462 BLAKE2B f8cb3857989e4966c12a9b4f4a13403ceab0ae9d33ddf81970ef886fb1f46bfd14bfc15aea498ea360cc801224c60489f0ce3b33fe10bead4dcbf3f6a06eee93 SHA512 849b9e8854585ce119f87e8bea655bcb834f1f986bccbf5ffa148fd4a1aae2030b6be938adbf377f0076361a3d9338802e1af8965f01b9c4d2a0517be330beef

diff --git a/sci-mathematics/lean/lean-3.50.3.ebuild b/sci-mathematics/lean/lean-3.50.3.ebuild
new file mode 100644
index 000000000000..e008b81cf582
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.50.3.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
+}

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

[Maciej Barć]

commit:     fb75aa659ac9fd8c44cb96b3c45441cca6ff58a0
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Dec 24 02:45:46 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Dec 24 02:47:21 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=fb75aa65

sci-mathematics/lean: bump to 3.50.2

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.50.2.ebuild | 77 +++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 92f7b6631413..02c8c71ff07b 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
 DIST lean-3.50.0.tar.gz 1918549 BLAKE2B 79827ffb9f825dff040e41e9bcbd8306e2f3a116b74fc6e0831450765d5b896fad2a86ec5dd9e63bf0f8777b575d4ab7ae8d158c233364fad6d4437bc0767452 SHA512 2b8d730ef9d808a24a9708f2b33409510bd6b7350f515679ba0395a45fc2dea2125639cdeb867bec4ac9c8114e448fb9777a69f8859e172f6e694ecacbb07f56
 DIST lean-3.50.1.tar.gz 1918323 BLAKE2B 3a26a6481a8472941a928a7b33b24231239e553cd4a4af5671f6a05f1fa68a54657518c4775b641239aa55401100e44c2797d7ae572405225657f1f7da8e193c SHA512 df2e5915e8a7f7e278e2d3472afe6cc23fec5de808b0cc1b20365ad41cfd03b1efda80523059a96c6b3d9b8b0ccab311700ee6a5d6c9751454ebe3b2f168cf77
+DIST lean-3.50.2.tar.gz 1918353 BLAKE2B 2a8c41eef0cc3c2d3e1b45ccd2383279a1a91c0de772c5fe3f1ffafc808db4b6e7342f2f72bd4c4120ed4248d60359c6e331f4adc1d26c6328b284549861c4de SHA512 58d085deb0354db0067e86e6097dad7f1543f356d4e50607b8cc049a19d867aa7ea03553bab3799c6ad18d0ef4fa468b0f966512d8bf0076526f90e93195a407

diff --git a/sci-mathematics/lean/lean-3.50.2.ebuild b/sci-mathematics/lean/lean-3.50.2.ebuild
new file mode 100644
index 000000000000..e008b81cf582
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.50.2.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
+}

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

[Maciej Barć]

commit:     9c2a388c47e62f982dd56125265afec2ceac9de7
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Dec 24 02:35:51 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Dec 24 02:47:21 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=9c2a388c

sci-mathematics/lean: drop old 3.49.1

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.49.1.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 4394832e7ba6..92f7b6631413 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
-DIST lean-3.49.1.tar.gz 1918165 BLAKE2B bebb29023f7d8979dae19d7c5ef6503be03012366c8a4f21a69244a1daadf90c73e8a8754656d7b1a6eccb1123f0905f3dcaa15885b0307399979024d2c5a051 SHA512 6648ab84840099495df5bec9432c75c40fc0920ac2a18297b42c35de593ec4eaee8bcf807cb6e273c2715090e5d1ab6c59652f482016af68d758e7e6e55dd87f
 DIST lean-3.50.0.tar.gz 1918549 BLAKE2B 79827ffb9f825dff040e41e9bcbd8306e2f3a116b74fc6e0831450765d5b896fad2a86ec5dd9e63bf0f8777b575d4ab7ae8d158c233364fad6d4437bc0767452 SHA512 2b8d730ef9d808a24a9708f2b33409510bd6b7350f515679ba0395a45fc2dea2125639cdeb867bec4ac9c8114e448fb9777a69f8859e172f6e694ecacbb07f56
 DIST lean-3.50.1.tar.gz 1918323 BLAKE2B 3a26a6481a8472941a928a7b33b24231239e553cd4a4af5671f6a05f1fa68a54657518c4775b641239aa55401100e44c2797d7ae572405225657f1f7da8e193c SHA512 df2e5915e8a7f7e278e2d3472afe6cc23fec5de808b0cc1b20365ad41cfd03b1efda80523059a96c6b3d9b8b0ccab311700ee6a5d6c9751454ebe3b2f168cf77

diff --git a/sci-mathematics/lean/lean-3.49.1.ebuild b/sci-mathematics/lean/lean-3.49.1.ebuild
deleted file mode 100644
index e008b81cf582..000000000000
--- a/sci-mathematics/lean/lean-3.49.1.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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
-}

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

[Sam James]

commit:     b9d8d9bfb9a22e7736057a5aa9d7a83876caa5d9
Author:     Sam James <sam <AT> gentoo <DOT> org>
AuthorDate: Wed Dec 21 23:51:55 2022 +0000
Commit:     Sam James <sam <AT> gentoo <DOT> org>
CommitDate: Wed Dec 21 23:52:01 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=b9d8d9bf

sci-mathematics/lean: Stabilize 3.49.0 amd64, #887811

Signed-off-by: Sam James <sam <AT> gentoo.org>

 sci-mathematics/lean/lean-3.49.0.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/lean/lean-3.49.0.ebuild b/sci-mathematics/lean/lean-3.49.0.ebuild
index e008b81cf582..08920adac95a 100644
--- a/sci-mathematics/lean/lean-3.49.0.ebuild
+++ b/sci-mathematics/lean/lean-3.49.0.ebuild
@@ -16,7 +16,7 @@ if [[ ${PV} == *9999* ]] ; then
 	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"
+	KEYWORDS="amd64 ~x86"
 fi
 S="${S}/src"
 

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

[Maciej Barć]

commit:     9d57ecf9103a6e6d1a83e9c066531624660345ca
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Wed Dec 21 23:32:02 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Wed Dec 21 23:49:28 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=9d57ecf9

sci-mathematics/lean: bump to 3.50.1

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.50.1.ebuild | 77 +++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 334759fa7784..4394832e7ba6 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
 DIST lean-3.49.1.tar.gz 1918165 BLAKE2B bebb29023f7d8979dae19d7c5ef6503be03012366c8a4f21a69244a1daadf90c73e8a8754656d7b1a6eccb1123f0905f3dcaa15885b0307399979024d2c5a051 SHA512 6648ab84840099495df5bec9432c75c40fc0920ac2a18297b42c35de593ec4eaee8bcf807cb6e273c2715090e5d1ab6c59652f482016af68d758e7e6e55dd87f
 DIST lean-3.50.0.tar.gz 1918549 BLAKE2B 79827ffb9f825dff040e41e9bcbd8306e2f3a116b74fc6e0831450765d5b896fad2a86ec5dd9e63bf0f8777b575d4ab7ae8d158c233364fad6d4437bc0767452 SHA512 2b8d730ef9d808a24a9708f2b33409510bd6b7350f515679ba0395a45fc2dea2125639cdeb867bec4ac9c8114e448fb9777a69f8859e172f6e694ecacbb07f56
+DIST lean-3.50.1.tar.gz 1918323 BLAKE2B 3a26a6481a8472941a928a7b33b24231239e553cd4a4af5671f6a05f1fa68a54657518c4775b641239aa55401100e44c2797d7ae572405225657f1f7da8e193c SHA512 df2e5915e8a7f7e278e2d3472afe6cc23fec5de808b0cc1b20365ad41cfd03b1efda80523059a96c6b3d9b8b0ccab311700ee6a5d6c9751454ebe3b2f168cf77

diff --git a/sci-mathematics/lean/lean-3.50.1.ebuild b/sci-mathematics/lean/lean-3.50.1.ebuild
new file mode 100644
index 000000000000..e008b81cf582
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.50.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
+}

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

[Maciej Barć]

commit:     ff43595f6fc27b3ffca106f140c5e677f7c38418
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Dec 15 08:31:04 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Dec 15 08:41:12 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ff43595f

sci-mathematics/lean: bump to 3.50.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.50.0.ebuild | 77 +++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index a6322520da8d..334759fa7784 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,2 +1,3 @@
 DIST lean-3.49.0.tar.gz 1918154 BLAKE2B 9f9973d00d2d5d5b7d26d50117c27754feb5132e88decd55859432a384dac2897184dcf8d841ad0034854657ac25e462dc69cdbe1cf2040787d108bb7e1370f4 SHA512 b4672843c2e923da8d56b91c14966fc2ec66c573564d68db9c52f9b40f2c97d82497f2ef6424b023c4ae50f6f0c11674e2d79053844ea669d226d0fe24077ade
 DIST lean-3.49.1.tar.gz 1918165 BLAKE2B bebb29023f7d8979dae19d7c5ef6503be03012366c8a4f21a69244a1daadf90c73e8a8754656d7b1a6eccb1123f0905f3dcaa15885b0307399979024d2c5a051 SHA512 6648ab84840099495df5bec9432c75c40fc0920ac2a18297b42c35de593ec4eaee8bcf807cb6e273c2715090e5d1ab6c59652f482016af68d758e7e6e55dd87f
+DIST lean-3.50.0.tar.gz 1918549 BLAKE2B 79827ffb9f825dff040e41e9bcbd8306e2f3a116b74fc6e0831450765d5b896fad2a86ec5dd9e63bf0f8777b575d4ab7ae8d158c233364fad6d4437bc0767452 SHA512 2b8d730ef9d808a24a9708f2b33409510bd6b7350f515679ba0395a45fc2dea2125639cdeb867bec4ac9c8114e448fb9777a69f8859e172f6e694ecacbb07f56

diff --git a/sci-mathematics/lean/lean-3.50.0.ebuild b/sci-mathematics/lean/lean-3.50.0.ebuild
new file mode 100644
index 000000000000..e008b81cf582
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.50.0.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
+}

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

[Maciej Barć]

commit:     ad73daf529a2e367c224390bf18f17e72fa3ccd3
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Dec 15 08:17:58 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Dec 15 08:41:12 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ad73daf5

sci-mathematics/lean: drop old 3.48.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.48.0.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 6cab555cb67f..a6322520da8d 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,2 @@
-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.48.0.ebuild b/sci-mathematics/lean/lean-3.48.0.ebuild
deleted file mode 100644
index e008b81cf582..000000000000
--- a/sci-mathematics/lean/lean-3.48.0.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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
-}

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

[Maciej Barć]

commit:     c07ecd3a781cdb9c02c6b9b3c212e46c528d6de5
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Dec 15 08:16:23 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Dec 15 08:41:12 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c07ecd3a

sci-mathematics/lean: drop old 3.47.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.47.0.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 0f3179c248a3..6cab555cb67f 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
-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.47.0.ebuild b/sci-mathematics/lean/lean-3.47.0.ebuild
deleted file mode 100644
index e008b81cf582..000000000000
--- a/sci-mathematics/lean/lean-3.47.0.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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
-}

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

[Maciej Barć]

commit:     9f378b9a170e462527b9d6580df1f653a7ab15e1
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Fri Nov 18 22:13:11 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Fri Nov 18 22:15:13 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=9f378b9a

sci-mathematics/lean: bump to 3.49.1

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.49.1.ebuild | 77 +++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)

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
+}

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

[Maciej Barć]

commit:     3a343e45ca66c1757266e59583465526adf1c056
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Nov 12 05:02:46 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Nov 12 05:02:55 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=3a343e45

sci-mathematics/lean: drop old 3.46.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.46.0.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 3d2824e4146a..bd291d742f31 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
-DIST lean-3.46.0.tar.gz 1913857 BLAKE2B de0a48ab3cff934d6a9583833a94a409a6351bd8433dbf47dbb510620a6c27aae26891472b4f1443e0f833b1c13de8653f0ea4edf61d14d43cfdb1aa25a555bf SHA512 d4487154cf6364b49ce19d1946a0bf0af6faeb1276ef08754a3dbed9bf071c2873eebdb1d6bcbe39ab2aaf5e93a97007ce954fd7c1ca4062fb2e6214e75e3b2b
 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

diff --git a/sci-mathematics/lean/lean-3.46.0.ebuild b/sci-mathematics/lean/lean-3.46.0.ebuild
deleted file mode 100644
index 6623228581a0..000000000000
--- a/sci-mathematics/lean/lean-3.46.0.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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="${WORKDIR}/lean-${PV}/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
-}

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

[Maciej Barć]

commit:     e8151b7873f72fce1435682a90e2a41fa464ae35
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Nov 12 04:33:22 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Nov 12 05:02:55 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e8151b78

sci-mathematics/lean: bump to 3.49.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.49.0.ebuild | 77 +++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 9ab1ec4d18f7..3d2824e4146a 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.46.0.tar.gz 1913857 BLAKE2B de0a48ab3cff934d6a9583833a94a409a6351bd8433dbf47dbb510620a6c27aae26891472b4f1443e0f833b1c13de8653f0ea4edf61d14d43cfdb1aa25a555bf SHA512 d4487154cf6364b49ce19d1946a0bf0af6faeb1276ef08754a3dbed9bf071c2873eebdb1d6bcbe39ab2aaf5e93a97007ce954fd7c1ca4062fb2e6214e75e3b2b
 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

diff --git a/sci-mathematics/lean/lean-3.49.0.ebuild b/sci-mathematics/lean/lean-3.49.0.ebuild
new file mode 100644
index 000000000000..e008b81cf582
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.49.0.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
+}

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

[Maciej Barć]

commit:     e0ab0acc6d5afb6a4ada31765fefad105c05a204
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Aug 30 14:35:20 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Aug 30 14:35:36 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e0ab0acc

sci-mathematics/lean: drop old 3.45.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.45.0.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 2713b7b8577a..9ab1ec4d18f7 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
-DIST lean-3.45.0.tar.gz 1913638 BLAKE2B f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f7241844ffff69400ec354a194cc345feca8f0dbcb06a673cc2d3d4 SHA512 c97c1dc6004823c73d8e40b5587ebbee7bd7a90b65ecdd3a976510d0d335b6df9a26916eedd5524f7137a32254a59dd5a6f15ce67f77d500926c9bc781aa5526
 DIST lean-3.46.0.tar.gz 1913857 BLAKE2B de0a48ab3cff934d6a9583833a94a409a6351bd8433dbf47dbb510620a6c27aae26891472b4f1443e0f833b1c13de8653f0ea4edf61d14d43cfdb1aa25a555bf SHA512 d4487154cf6364b49ce19d1946a0bf0af6faeb1276ef08754a3dbed9bf071c2873eebdb1d6bcbe39ab2aaf5e93a97007ce954fd7c1ca4062fb2e6214e75e3b2b
 DIST lean-3.47.0.tar.gz 1917990 BLAKE2B 1249654b3a71d1a3b601c79915232d5f53335cd4a5b3c41f97dd5cb39e86bc5ea3c4208b5ebca9fae43c01b7da64579cdf6bcec12b8861ca69339277efe7431d SHA512 11879e4bc324e036b917af0761d918eb393aa3226a36b305dbcd233988504178082290dab2d2e25bc3b7732cb5246a397e29fbd4c956efa9ea454cb46568d942
 DIST lean-3.48.0.tar.gz 1918012 BLAKE2B 4616af2e4d66c56866f321797d6bb05049925f62c2c62c72a3a5552d39cc83c48c1dc2e59b9d81a7341346ed6f3173ef6e69902b8e8a5a24c4af86dace76360b SHA512 9e017484f88fac40e35604643c972d5f316df70c18b00f90b107d994f5e58eeb0637033354c1e0159a9dfc8c72fe3ea9d3b70569b46fc37b22a94c3d7445cdac

diff --git a/sci-mathematics/lean/lean-3.45.0.ebuild b/sci-mathematics/lean/lean-3.45.0.ebuild
deleted file mode 100644
index 6623228581a0..000000000000
--- a/sci-mathematics/lean/lean-3.45.0.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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="${WORKDIR}/lean-${PV}/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
-}

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

[Maciej Barć]

commit:     4c42b4e422dded92c6d4964caf09f6d6ac9c5800
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Aug 30 13:42:47 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Aug 30 14:35:35 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=4c42b4e4

sci-mathematics/lean: bump to 3.48.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.48.0.ebuild | 77 +++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 46924bc36752..2713b7b8577a 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.45.0.tar.gz 1913638 BLAKE2B f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f7241844ffff69400ec354a194cc345feca8f0dbcb06a673cc2d3d4 SHA512 c97c1dc6004823c73d8e40b5587ebbee7bd7a90b65ecdd3a976510d0d335b6df9a26916eedd5524f7137a32254a59dd5a6f15ce67f77d500926c9bc781aa5526
 DIST lean-3.46.0.tar.gz 1913857 BLAKE2B de0a48ab3cff934d6a9583833a94a409a6351bd8433dbf47dbb510620a6c27aae26891472b4f1443e0f833b1c13de8653f0ea4edf61d14d43cfdb1aa25a555bf SHA512 d4487154cf6364b49ce19d1946a0bf0af6faeb1276ef08754a3dbed9bf071c2873eebdb1d6bcbe39ab2aaf5e93a97007ce954fd7c1ca4062fb2e6214e75e3b2b
 DIST lean-3.47.0.tar.gz 1917990 BLAKE2B 1249654b3a71d1a3b601c79915232d5f53335cd4a5b3c41f97dd5cb39e86bc5ea3c4208b5ebca9fae43c01b7da64579cdf6bcec12b8861ca69339277efe7431d SHA512 11879e4bc324e036b917af0761d918eb393aa3226a36b305dbcd233988504178082290dab2d2e25bc3b7732cb5246a397e29fbd4c956efa9ea454cb46568d942
+DIST lean-3.48.0.tar.gz 1918012 BLAKE2B 4616af2e4d66c56866f321797d6bb05049925f62c2c62c72a3a5552d39cc83c48c1dc2e59b9d81a7341346ed6f3173ef6e69902b8e8a5a24c4af86dace76360b SHA512 9e017484f88fac40e35604643c972d5f316df70c18b00f90b107d994f5e58eeb0637033354c1e0159a9dfc8c72fe3ea9d3b70569b46fc37b22a94c3d7445cdac

diff --git a/sci-mathematics/lean/lean-3.48.0.ebuild b/sci-mathematics/lean/lean-3.48.0.ebuild
new file mode 100644
index 000000000000..e008b81cf582
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.48.0.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
+}

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

[Maciej Barć]

commit:     83a2c3f160fefff958a12efb306e3ad54e3bd159
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Fri Aug 26 00:12:18 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Fri Aug 26 00:32:04 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=83a2c3f1

sci-mathematics/lean: fix live

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

 sci-mathematics/lean/lean-3.9999.ebuild | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/sci-mathematics/lean/lean-3.9999.ebuild b/sci-mathematics/lean/lean-3.9999.ebuild
index 6623228581a0..307c5b95bc1b 100644
--- a/sci-mathematics/lean/lean-3.9999.ebuild
+++ b/sci-mathematics/lean/lean-3.9999.ebuild
@@ -11,14 +11,14 @@ inherit flag-o-matic cmake readme.gentoo-r1
 DESCRIPTION="The Lean Theorem Prover"
 HOMEPAGE="https://leanprover-community.github.io/"
 
-if [[ "${PV}" == *9999* ]]; then
+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="${WORKDIR}/lean-${PV}/src"
+S="${S}/src"
 
 LICENSE="Apache-2.0"
 SLOT="0/${MAJOR}"
@@ -27,7 +27,7 @@ IUSE="debug +threads"
 RDEPEND="dev-libs/gmp:="
 DEPEND="${RDEPEND}"
 
-PATCHES=( "${FILESDIR}/${PN}-CMakeLists-fix_flags.patch" )
+PATCHES=( "${FILESDIR}"/${PN}-CMakeLists-fix_flags.patch )
 
 src_configure() {
 	local CMAKE_BUILD_TYPE

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

[Maciej Barć]

commit:     c872faa59cdf7824ca359cbd30682806fa636898
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Fri Aug 26 00:15:03 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Fri Aug 26 00:32:05 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c872faa5

sci-mathematics/lean: drop old 3.44.1

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.44.1.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 165b313788c8..46924bc36752 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
-DIST lean-3.44.1.tar.gz 1911708 BLAKE2B 33dc94fb1f1eac2684b7a37fda3545ad6d4f6d703e7914c44b9a05fb57e55d4b9bef484ff1f6608f9bb0fe453ca28b7fa5c74e6bce135df06fb25ad6d9d3a37b SHA512 69ffd1a8519b476dd1879bfe2f8f8f4268a5490f11b581ee1e583382e6f03f947d958e8b5ee8ceead562945a406ee2dc9b0ae2da6f29f03a38828eadab88a4f8
 DIST lean-3.45.0.tar.gz 1913638 BLAKE2B f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f7241844ffff69400ec354a194cc345feca8f0dbcb06a673cc2d3d4 SHA512 c97c1dc6004823c73d8e40b5587ebbee7bd7a90b65ecdd3a976510d0d335b6df9a26916eedd5524f7137a32254a59dd5a6f15ce67f77d500926c9bc781aa5526
 DIST lean-3.46.0.tar.gz 1913857 BLAKE2B de0a48ab3cff934d6a9583833a94a409a6351bd8433dbf47dbb510620a6c27aae26891472b4f1443e0f833b1c13de8653f0ea4edf61d14d43cfdb1aa25a555bf SHA512 d4487154cf6364b49ce19d1946a0bf0af6faeb1276ef08754a3dbed9bf071c2873eebdb1d6bcbe39ab2aaf5e93a97007ce954fd7c1ca4062fb2e6214e75e3b2b
 DIST lean-3.47.0.tar.gz 1917990 BLAKE2B 1249654b3a71d1a3b601c79915232d5f53335cd4a5b3c41f97dd5cb39e86bc5ea3c4208b5ebca9fae43c01b7da64579cdf6bcec12b8861ca69339277efe7431d SHA512 11879e4bc324e036b917af0761d918eb393aa3226a36b305dbcd233988504178082290dab2d2e25bc3b7732cb5246a397e29fbd4c956efa9ea454cb46568d942

diff --git a/sci-mathematics/lean/lean-3.44.1.ebuild b/sci-mathematics/lean/lean-3.44.1.ebuild
deleted file mode 100644
index 6623228581a0..000000000000
--- a/sci-mathematics/lean/lean-3.44.1.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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="${WORKDIR}/lean-${PV}/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
-}

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

[Maciej Barć]

commit:     48ab1124b5f76709034a86da56caa70933173cef
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Fri Aug 26 00:12:51 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Fri Aug 26 00:32:04 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=48ab1124

sci-mathematics/lean: bump to 3.47.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.47.0.ebuild | 77 +++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 346decdf5c6c..165b313788c8 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.44.1.tar.gz 1911708 BLAKE2B 33dc94fb1f1eac2684b7a37fda3545ad6d4f6d703e7914c44b9a05fb57e55d4b9bef484ff1f6608f9bb0fe453ca28b7fa5c74e6bce135df06fb25ad6d9d3a37b SHA512 69ffd1a8519b476dd1879bfe2f8f8f4268a5490f11b581ee1e583382e6f03f947d958e8b5ee8ceead562945a406ee2dc9b0ae2da6f29f03a38828eadab88a4f8
 DIST lean-3.45.0.tar.gz 1913638 BLAKE2B f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f7241844ffff69400ec354a194cc345feca8f0dbcb06a673cc2d3d4 SHA512 c97c1dc6004823c73d8e40b5587ebbee7bd7a90b65ecdd3a976510d0d335b6df9a26916eedd5524f7137a32254a59dd5a6f15ce67f77d500926c9bc781aa5526
 DIST lean-3.46.0.tar.gz 1913857 BLAKE2B de0a48ab3cff934d6a9583833a94a409a6351bd8433dbf47dbb510620a6c27aae26891472b4f1443e0f833b1c13de8653f0ea4edf61d14d43cfdb1aa25a555bf SHA512 d4487154cf6364b49ce19d1946a0bf0af6faeb1276ef08754a3dbed9bf071c2873eebdb1d6bcbe39ab2aaf5e93a97007ce954fd7c1ca4062fb2e6214e75e3b2b
+DIST lean-3.47.0.tar.gz 1917990 BLAKE2B 1249654b3a71d1a3b601c79915232d5f53335cd4a5b3c41f97dd5cb39e86bc5ea3c4208b5ebca9fae43c01b7da64579cdf6bcec12b8861ca69339277efe7431d SHA512 11879e4bc324e036b917af0761d918eb393aa3226a36b305dbcd233988504178082290dab2d2e25bc3b7732cb5246a397e29fbd4c956efa9ea454cb46568d942

diff --git a/sci-mathematics/lean/lean-3.47.0.ebuild b/sci-mathematics/lean/lean-3.47.0.ebuild
new file mode 100644
index 000000000000..e008b81cf582
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.47.0.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
+}

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

[Maciej Barć]

commit:     3b93a2c696da21d2f18531ea9ed81c730e73e69f
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Aug  9 00:02:09 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Aug  9 00:02:09 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=3b93a2c6

sci-mathematics/lean: drop old 3.43.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.43.0.ebuild | 77 ---------------------------------
 2 files changed, 78 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index d61351695e7e..346decdf5c6c 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
-DIST lean-3.43.0.tar.gz 1909158 BLAKE2B 587995afb123e6c74a730f9709a001bab6b2ac82471dcf8b1219dda782853fcdb9735d16038b95a7950f6530dd3cf1e0b13e4d1044d723d3662217951b809928 SHA512 25cbad94b869bb39edaf9ed2478ffc298b130f22cb4db7c116212546583d670079ddde1b524a33499d00ac43fc82b6928e6801c83d613597aae255db9c45d9f3
 DIST lean-3.44.1.tar.gz 1911708 BLAKE2B 33dc94fb1f1eac2684b7a37fda3545ad6d4f6d703e7914c44b9a05fb57e55d4b9bef484ff1f6608f9bb0fe453ca28b7fa5c74e6bce135df06fb25ad6d9d3a37b SHA512 69ffd1a8519b476dd1879bfe2f8f8f4268a5490f11b581ee1e583382e6f03f947d958e8b5ee8ceead562945a406ee2dc9b0ae2da6f29f03a38828eadab88a4f8
 DIST lean-3.45.0.tar.gz 1913638 BLAKE2B f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f7241844ffff69400ec354a194cc345feca8f0dbcb06a673cc2d3d4 SHA512 c97c1dc6004823c73d8e40b5587ebbee7bd7a90b65ecdd3a976510d0d335b6df9a26916eedd5524f7137a32254a59dd5a6f15ce67f77d500926c9bc781aa5526
 DIST lean-3.46.0.tar.gz 1913857 BLAKE2B de0a48ab3cff934d6a9583833a94a409a6351bd8433dbf47dbb510620a6c27aae26891472b4f1443e0f833b1c13de8653f0ea4edf61d14d43cfdb1aa25a555bf SHA512 d4487154cf6364b49ce19d1946a0bf0af6faeb1276ef08754a3dbed9bf071c2873eebdb1d6bcbe39ab2aaf5e93a97007ce954fd7c1ca4062fb2e6214e75e3b2b

diff --git a/sci-mathematics/lean/lean-3.43.0.ebuild b/sci-mathematics/lean/lean-3.43.0.ebuild
deleted file mode 100644
index 6623228581a0..000000000000
--- a/sci-mathematics/lean/lean-3.43.0.ebuild
+++ /dev/null
@@ -1,77 +0,0 @@
-# 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="${WORKDIR}/lean-${PV}/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
-}

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

[Maciej Barć]

commit:     b5dd196eb69a20afced12e16dfdb0235ed590f52
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Mon Aug  8 23:59:11 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Mon Aug  8 23:59:11 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=b5dd196e

sci-mathematics/lean: bump to 3.46.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.46.0.ebuild | 77 +++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index a86db5365be7..d61351695e7e 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.43.0.tar.gz 1909158 BLAKE2B 587995afb123e6c74a730f9709a001bab6b2ac82471dcf8b1219dda782853fcdb9735d16038b95a7950f6530dd3cf1e0b13e4d1044d723d3662217951b809928 SHA512 25cbad94b869bb39edaf9ed2478ffc298b130f22cb4db7c116212546583d670079ddde1b524a33499d00ac43fc82b6928e6801c83d613597aae255db9c45d9f3
 DIST lean-3.44.1.tar.gz 1911708 BLAKE2B 33dc94fb1f1eac2684b7a37fda3545ad6d4f6d703e7914c44b9a05fb57e55d4b9bef484ff1f6608f9bb0fe453ca28b7fa5c74e6bce135df06fb25ad6d9d3a37b SHA512 69ffd1a8519b476dd1879bfe2f8f8f4268a5490f11b581ee1e583382e6f03f947d958e8b5ee8ceead562945a406ee2dc9b0ae2da6f29f03a38828eadab88a4f8
 DIST lean-3.45.0.tar.gz 1913638 BLAKE2B f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f7241844ffff69400ec354a194cc345feca8f0dbcb06a673cc2d3d4 SHA512 c97c1dc6004823c73d8e40b5587ebbee7bd7a90b65ecdd3a976510d0d335b6df9a26916eedd5524f7137a32254a59dd5a6f15ce67f77d500926c9bc781aa5526
+DIST lean-3.46.0.tar.gz 1913857 BLAKE2B de0a48ab3cff934d6a9583833a94a409a6351bd8433dbf47dbb510620a6c27aae26891472b4f1443e0f833b1c13de8653f0ea4edf61d14d43cfdb1aa25a555bf SHA512 d4487154cf6364b49ce19d1946a0bf0af6faeb1276ef08754a3dbed9bf071c2873eebdb1d6bcbe39ab2aaf5e93a97007ce954fd7c1ca4062fb2e6214e75e3b2b

diff --git a/sci-mathematics/lean/lean-3.46.0.ebuild b/sci-mathematics/lean/lean-3.46.0.ebuild
new file mode 100644
index 000000000000..6623228581a0
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.46.0.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="${WORKDIR}/lean-${PV}/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
+}

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

[Maciej Barć]

commit:     56a7877fca5ed96053d93689e4e4a28786f3003f
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Aug  2 21:42:02 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Aug  2 21:42:18 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=56a7877f

sci-mathematics/lean: filter LTO (odr)

Closes: https://bugs.gentoo.org/863086
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 sci-mathematics/lean/lean-3.43.0.ebuild | 4 +++-
 sci-mathematics/lean/lean-3.44.1.ebuild | 4 +++-
 sci-mathematics/lean/lean-3.45.0.ebuild | 4 +++-
 sci-mathematics/lean/lean-3.9999.ebuild | 4 +++-
 4 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/sci-mathematics/lean/lean-3.43.0.ebuild b/sci-mathematics/lean/lean-3.43.0.ebuild
index 5d8ee8eecd4b..6623228581a0 100644
--- a/sci-mathematics/lean/lean-3.43.0.ebuild
+++ b/sci-mathematics/lean/lean-3.43.0.ebuild
@@ -6,7 +6,7 @@ EAPI=8
 MAJOR=$(ver_cut 1)
 CMAKE_IN_SOURCE_BUILD="ON"
 
-inherit cmake readme.gentoo-r1
+inherit flag-o-matic cmake readme.gentoo-r1
 
 DESCRIPTION="The Lean Theorem Prover"
 HOMEPAGE="https://leanprover-community.github.io/"
@@ -37,6 +37,8 @@ src_configure() {
 		CMAKE_BUILD_TYPE="Release"
 	fi
 
+	filter-lto
+
 	local mycmakeargs=(
 		-DALPHA=ON
 		-DAUTO_THREAD_FINALIZATION=ON

diff --git a/sci-mathematics/lean/lean-3.44.1.ebuild b/sci-mathematics/lean/lean-3.44.1.ebuild
index 5d8ee8eecd4b..6623228581a0 100644
--- a/sci-mathematics/lean/lean-3.44.1.ebuild
+++ b/sci-mathematics/lean/lean-3.44.1.ebuild
@@ -6,7 +6,7 @@ EAPI=8
 MAJOR=$(ver_cut 1)
 CMAKE_IN_SOURCE_BUILD="ON"
 
-inherit cmake readme.gentoo-r1
+inherit flag-o-matic cmake readme.gentoo-r1
 
 DESCRIPTION="The Lean Theorem Prover"
 HOMEPAGE="https://leanprover-community.github.io/"
@@ -37,6 +37,8 @@ src_configure() {
 		CMAKE_BUILD_TYPE="Release"
 	fi
 
+	filter-lto
+
 	local mycmakeargs=(
 		-DALPHA=ON
 		-DAUTO_THREAD_FINALIZATION=ON

diff --git a/sci-mathematics/lean/lean-3.45.0.ebuild b/sci-mathematics/lean/lean-3.45.0.ebuild
index 5d8ee8eecd4b..6623228581a0 100644
--- a/sci-mathematics/lean/lean-3.45.0.ebuild
+++ b/sci-mathematics/lean/lean-3.45.0.ebuild
@@ -6,7 +6,7 @@ EAPI=8
 MAJOR=$(ver_cut 1)
 CMAKE_IN_SOURCE_BUILD="ON"
 
-inherit cmake readme.gentoo-r1
+inherit flag-o-matic cmake readme.gentoo-r1
 
 DESCRIPTION="The Lean Theorem Prover"
 HOMEPAGE="https://leanprover-community.github.io/"
@@ -37,6 +37,8 @@ src_configure() {
 		CMAKE_BUILD_TYPE="Release"
 	fi
 
+	filter-lto
+
 	local mycmakeargs=(
 		-DALPHA=ON
 		-DAUTO_THREAD_FINALIZATION=ON

diff --git a/sci-mathematics/lean/lean-3.9999.ebuild b/sci-mathematics/lean/lean-3.9999.ebuild
index 5d8ee8eecd4b..6623228581a0 100644
--- a/sci-mathematics/lean/lean-3.9999.ebuild
+++ b/sci-mathematics/lean/lean-3.9999.ebuild
@@ -6,7 +6,7 @@ EAPI=8
 MAJOR=$(ver_cut 1)
 CMAKE_IN_SOURCE_BUILD="ON"
 
-inherit cmake readme.gentoo-r1
+inherit flag-o-matic cmake readme.gentoo-r1
 
 DESCRIPTION="The Lean Theorem Prover"
 HOMEPAGE="https://leanprover-community.github.io/"
@@ -37,6 +37,8 @@ src_configure() {
 		CMAKE_BUILD_TYPE="Release"
 	fi
 
+	filter-lto
+
 	local mycmakeargs=(
 		-DALPHA=ON
 		-DAUTO_THREAD_FINALIZATION=ON

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

[Maciej Barć]

commit:     a8bce87f953078b3eadf7659b15626c415ce13cd
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Jul 14 08:06:54 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Jul 14 10:05:26 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=a8bce87f

sci-mathematics/lean: bump to 3.45.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.45.0.ebuild | 75 +++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 9bef7ade59c6..c369f65e687e 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.42.1.tar.gz 1908398 BLAKE2B 7a83269deb3dc7ee60bf7a09b36df332355d9caf575b8435345956697121e95e1fb44cada1237e44bab04a56af4fb40c0d01e49f4cb3e4896e616f2bc58bf9ef SHA512 ab266e385e3026ce3219eef6ef171e243576e291fb26cef3d97ca4cc5190988e3bd6fe93c37a1192b8d2eec0ae7620131826ee1073a038f5a024e706953242d1
 DIST lean-3.43.0.tar.gz 1909158 BLAKE2B 587995afb123e6c74a730f9709a001bab6b2ac82471dcf8b1219dda782853fcdb9735d16038b95a7950f6530dd3cf1e0b13e4d1044d723d3662217951b809928 SHA512 25cbad94b869bb39edaf9ed2478ffc298b130f22cb4db7c116212546583d670079ddde1b524a33499d00ac43fc82b6928e6801c83d613597aae255db9c45d9f3
 DIST lean-3.44.1.tar.gz 1911708 BLAKE2B 33dc94fb1f1eac2684b7a37fda3545ad6d4f6d703e7914c44b9a05fb57e55d4b9bef484ff1f6608f9bb0fe453ca28b7fa5c74e6bce135df06fb25ad6d9d3a37b SHA512 69ffd1a8519b476dd1879bfe2f8f8f4268a5490f11b581ee1e583382e6f03f947d958e8b5ee8ceead562945a406ee2dc9b0ae2da6f29f03a38828eadab88a4f8
+DIST lean-3.45.0.tar.gz 1913638 BLAKE2B f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f7241844ffff69400ec354a194cc345feca8f0dbcb06a673cc2d3d4 SHA512 c97c1dc6004823c73d8e40b5587ebbee7bd7a90b65ecdd3a976510d0d335b6df9a26916eedd5524f7137a32254a59dd5a6f15ce67f77d500926c9bc781aa5526

diff --git a/sci-mathematics/lean/lean-3.45.0.ebuild b/sci-mathematics/lean/lean-3.45.0.ebuild
new file mode 100644
index 000000000000..5d8ee8eecd4b
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.45.0.ebuild
@@ -0,0 +1,75 @@
+# 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 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="${WORKDIR}/lean-${PV}/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
+
+	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
+}

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

[Maciej Barć]

commit:     57d436b81243c5cd193dadc99d83aaaf61513017
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Jul 14 09:38:26 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Jul 14 10:05:27 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=57d436b8

sci-mathematics/lean: drop old 3.42.1

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.42.1.ebuild | 75 ---------------------------------
 2 files changed, 76 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index c369f65e687e..a86db5365be7 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
-DIST lean-3.42.1.tar.gz 1908398 BLAKE2B 7a83269deb3dc7ee60bf7a09b36df332355d9caf575b8435345956697121e95e1fb44cada1237e44bab04a56af4fb40c0d01e49f4cb3e4896e616f2bc58bf9ef SHA512 ab266e385e3026ce3219eef6ef171e243576e291fb26cef3d97ca4cc5190988e3bd6fe93c37a1192b8d2eec0ae7620131826ee1073a038f5a024e706953242d1
 DIST lean-3.43.0.tar.gz 1909158 BLAKE2B 587995afb123e6c74a730f9709a001bab6b2ac82471dcf8b1219dda782853fcdb9735d16038b95a7950f6530dd3cf1e0b13e4d1044d723d3662217951b809928 SHA512 25cbad94b869bb39edaf9ed2478ffc298b130f22cb4db7c116212546583d670079ddde1b524a33499d00ac43fc82b6928e6801c83d613597aae255db9c45d9f3
 DIST lean-3.44.1.tar.gz 1911708 BLAKE2B 33dc94fb1f1eac2684b7a37fda3545ad6d4f6d703e7914c44b9a05fb57e55d4b9bef484ff1f6608f9bb0fe453ca28b7fa5c74e6bce135df06fb25ad6d9d3a37b SHA512 69ffd1a8519b476dd1879bfe2f8f8f4268a5490f11b581ee1e583382e6f03f947d958e8b5ee8ceead562945a406ee2dc9b0ae2da6f29f03a38828eadab88a4f8
 DIST lean-3.45.0.tar.gz 1913638 BLAKE2B f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f7241844ffff69400ec354a194cc345feca8f0dbcb06a673cc2d3d4 SHA512 c97c1dc6004823c73d8e40b5587ebbee7bd7a90b65ecdd3a976510d0d335b6df9a26916eedd5524f7137a32254a59dd5a6f15ce67f77d500926c9bc781aa5526

diff --git a/sci-mathematics/lean/lean-3.42.1.ebuild b/sci-mathematics/lean/lean-3.42.1.ebuild
deleted file mode 100644
index 5d8ee8eecd4b..000000000000
--- a/sci-mathematics/lean/lean-3.42.1.ebuild
+++ /dev/null
@@ -1,75 +0,0 @@
-# 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 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="${WORKDIR}/lean-${PV}/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
-
-	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
-}

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

[Maciej Barć]

commit:     657666c6a8b6cbfc7a0acdb14d343300c056f54a
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Mon Jun 27 14:41:16 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Mon Jun 27 14:50:17 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=657666c6

sci-mathematics/lean: bump to 3.44.1

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.44.1.ebuild | 75 +++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 8727c64f6035..88926772a008 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -2,3 +2,4 @@ DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0e
 DIST lean-3.42.0.tar.gz 1908134 BLAKE2B 7b6403786cc1a3a2b974f8df4c2bf2921e4e374ead4290a0e263c8464a9c009fd2f62e7cf5bdbc5087d0c9bb4c57f798b9d1a4b8ee2d66152714ec2af649e196 SHA512 2f1fc1bf3aff7fa806e1cd4647380d6896d98a9191f2035d5a37cc35938de42b243188984aa2fced37bdbee3b2c3c6ef25d27bf2428bf9a0307cc3237c80560f
 DIST lean-3.42.1.tar.gz 1908398 BLAKE2B 7a83269deb3dc7ee60bf7a09b36df332355d9caf575b8435345956697121e95e1fb44cada1237e44bab04a56af4fb40c0d01e49f4cb3e4896e616f2bc58bf9ef SHA512 ab266e385e3026ce3219eef6ef171e243576e291fb26cef3d97ca4cc5190988e3bd6fe93c37a1192b8d2eec0ae7620131826ee1073a038f5a024e706953242d1
 DIST lean-3.43.0.tar.gz 1909158 BLAKE2B 587995afb123e6c74a730f9709a001bab6b2ac82471dcf8b1219dda782853fcdb9735d16038b95a7950f6530dd3cf1e0b13e4d1044d723d3662217951b809928 SHA512 25cbad94b869bb39edaf9ed2478ffc298b130f22cb4db7c116212546583d670079ddde1b524a33499d00ac43fc82b6928e6801c83d613597aae255db9c45d9f3
+DIST lean-3.44.1.tar.gz 1911708 BLAKE2B 33dc94fb1f1eac2684b7a37fda3545ad6d4f6d703e7914c44b9a05fb57e55d4b9bef484ff1f6608f9bb0fe453ca28b7fa5c74e6bce135df06fb25ad6d9d3a37b SHA512 69ffd1a8519b476dd1879bfe2f8f8f4268a5490f11b581ee1e583382e6f03f947d958e8b5ee8ceead562945a406ee2dc9b0ae2da6f29f03a38828eadab88a4f8

diff --git a/sci-mathematics/lean/lean-3.44.1.ebuild b/sci-mathematics/lean/lean-3.44.1.ebuild
new file mode 100644
index 000000000000..5d8ee8eecd4b
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.44.1.ebuild
@@ -0,0 +1,75 @@
+# 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 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="${WORKDIR}/lean-${PV}/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
+
+	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
+}

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

[Maciej Barć]

commit:     b276a47dda6fd8ab8a9a8aa332776bcea2e35ee0
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Mon Jun 27 14:42:04 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Mon Jun 27 14:50:17 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=b276a47d

sci-mathematics/lean: drop old 3.39.1 & 3.42.0

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

 sci-mathematics/lean/Manifest           |  2 -
 sci-mathematics/lean/lean-3.39.1.ebuild | 75 ---------------------------------
 sci-mathematics/lean/lean-3.42.0.ebuild | 75 ---------------------------------
 3 files changed, 152 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 88926772a008..9bef7ade59c6 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,5 +1,3 @@
-DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd
-DIST lean-3.42.0.tar.gz 1908134 BLAKE2B 7b6403786cc1a3a2b974f8df4c2bf2921e4e374ead4290a0e263c8464a9c009fd2f62e7cf5bdbc5087d0c9bb4c57f798b9d1a4b8ee2d66152714ec2af649e196 SHA512 2f1fc1bf3aff7fa806e1cd4647380d6896d98a9191f2035d5a37cc35938de42b243188984aa2fced37bdbee3b2c3c6ef25d27bf2428bf9a0307cc3237c80560f
 DIST lean-3.42.1.tar.gz 1908398 BLAKE2B 7a83269deb3dc7ee60bf7a09b36df332355d9caf575b8435345956697121e95e1fb44cada1237e44bab04a56af4fb40c0d01e49f4cb3e4896e616f2bc58bf9ef SHA512 ab266e385e3026ce3219eef6ef171e243576e291fb26cef3d97ca4cc5190988e3bd6fe93c37a1192b8d2eec0ae7620131826ee1073a038f5a024e706953242d1
 DIST lean-3.43.0.tar.gz 1909158 BLAKE2B 587995afb123e6c74a730f9709a001bab6b2ac82471dcf8b1219dda782853fcdb9735d16038b95a7950f6530dd3cf1e0b13e4d1044d723d3662217951b809928 SHA512 25cbad94b869bb39edaf9ed2478ffc298b130f22cb4db7c116212546583d670079ddde1b524a33499d00ac43fc82b6928e6801c83d613597aae255db9c45d9f3
 DIST lean-3.44.1.tar.gz 1911708 BLAKE2B 33dc94fb1f1eac2684b7a37fda3545ad6d4f6d703e7914c44b9a05fb57e55d4b9bef484ff1f6608f9bb0fe453ca28b7fa5c74e6bce135df06fb25ad6d9d3a37b SHA512 69ffd1a8519b476dd1879bfe2f8f8f4268a5490f11b581ee1e583382e6f03f947d958e8b5ee8ceead562945a406ee2dc9b0ae2da6f29f03a38828eadab88a4f8

diff --git a/sci-mathematics/lean/lean-3.39.1.ebuild b/sci-mathematics/lean/lean-3.39.1.ebuild
deleted file mode 100644
index d8b241bcd34b..000000000000
--- a/sci-mathematics/lean/lean-3.39.1.ebuild
+++ /dev/null
@@ -1,75 +0,0 @@
-# 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 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="${WORKDIR}/lean-${PV}/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
-
-	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
-}

diff --git a/sci-mathematics/lean/lean-3.42.0.ebuild b/sci-mathematics/lean/lean-3.42.0.ebuild
deleted file mode 100644
index 5d8ee8eecd4b..000000000000
--- a/sci-mathematics/lean/lean-3.42.0.ebuild
+++ /dev/null
@@ -1,75 +0,0 @@
-# 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 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="${WORKDIR}/lean-${PV}/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
-
-	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
-}

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

[Maciej Barć]

commit:     36d52f5fb108e6cc0663a6cbfdce443127a6577f
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Wed May 18 19:14:16 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Wed May 18 19:29:56 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=36d52f5f

sci-mathematics/lean: drop old 3.41.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.41.0.ebuild | 75 ---------------------------------
 2 files changed, 76 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 8821361f03b5..8727c64f6035 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,5 +1,4 @@
 DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd
-DIST lean-3.41.0.tar.gz 1905966 BLAKE2B 1921ba4a975ed8fc6001695151bb366341e0895989a570bb7fbef1e719685945d0b7c51ed0716ff29daaf81af24ce2e289cab41b251c686a286cd94a0cf708f8 SHA512 855a56812ba5dc7cf431490957570d0fcbc4760faa1602095e708ddcc4e5a3c6aeac42133c210375d4538d97c8ae90df3ab3c7e7840e8896b8d0db439e925fbf
 DIST lean-3.42.0.tar.gz 1908134 BLAKE2B 7b6403786cc1a3a2b974f8df4c2bf2921e4e374ead4290a0e263c8464a9c009fd2f62e7cf5bdbc5087d0c9bb4c57f798b9d1a4b8ee2d66152714ec2af649e196 SHA512 2f1fc1bf3aff7fa806e1cd4647380d6896d98a9191f2035d5a37cc35938de42b243188984aa2fced37bdbee3b2c3c6ef25d27bf2428bf9a0307cc3237c80560f
 DIST lean-3.42.1.tar.gz 1908398 BLAKE2B 7a83269deb3dc7ee60bf7a09b36df332355d9caf575b8435345956697121e95e1fb44cada1237e44bab04a56af4fb40c0d01e49f4cb3e4896e616f2bc58bf9ef SHA512 ab266e385e3026ce3219eef6ef171e243576e291fb26cef3d97ca4cc5190988e3bd6fe93c37a1192b8d2eec0ae7620131826ee1073a038f5a024e706953242d1
 DIST lean-3.43.0.tar.gz 1909158 BLAKE2B 587995afb123e6c74a730f9709a001bab6b2ac82471dcf8b1219dda782853fcdb9735d16038b95a7950f6530dd3cf1e0b13e4d1044d723d3662217951b809928 SHA512 25cbad94b869bb39edaf9ed2478ffc298b130f22cb4db7c116212546583d670079ddde1b524a33499d00ac43fc82b6928e6801c83d613597aae255db9c45d9f3

diff --git a/sci-mathematics/lean/lean-3.41.0.ebuild b/sci-mathematics/lean/lean-3.41.0.ebuild
deleted file mode 100644
index 5d8ee8eecd4b..000000000000
--- a/sci-mathematics/lean/lean-3.41.0.ebuild
+++ /dev/null
@@ -1,75 +0,0 @@
-# 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 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="${WORKDIR}/lean-${PV}/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
-
-	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
-}

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

[Maciej Barć]

commit:     e124cd89e3a8e36edbccc14fd5b791b8c11b9857
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sun Mar 27 00:56:32 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sun Mar 27 01:46:25 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e124cd89

sci-mathematics/lean: bump to 3.42.1

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.42.1.ebuild | 75 +++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index ad0e723b1b3c..910ec2d2d32c 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -2,3 +2,4 @@ DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0e
 DIST lean-3.40.0.tar.gz 1878547 BLAKE2B 762c12b9fee9ac405730fb4a748326e7c9603c50f44512166f94df51e8cde0096803f11d0201980e1a1c0121a2b278075bf238452254d83e2d8b7b5566355416 SHA512 4daa32b60195a9776019c3c13c3765a1f5a817d78f189c3f92859298118815af4cb47359816ebbb977f35453be358956f3680b06b5930d5cf3a4245599602873
 DIST lean-3.41.0.tar.gz 1905966 BLAKE2B 1921ba4a975ed8fc6001695151bb366341e0895989a570bb7fbef1e719685945d0b7c51ed0716ff29daaf81af24ce2e289cab41b251c686a286cd94a0cf708f8 SHA512 855a56812ba5dc7cf431490957570d0fcbc4760faa1602095e708ddcc4e5a3c6aeac42133c210375d4538d97c8ae90df3ab3c7e7840e8896b8d0db439e925fbf
 DIST lean-3.42.0.tar.gz 1908134 BLAKE2B 7b6403786cc1a3a2b974f8df4c2bf2921e4e374ead4290a0e263c8464a9c009fd2f62e7cf5bdbc5087d0c9bb4c57f798b9d1a4b8ee2d66152714ec2af649e196 SHA512 2f1fc1bf3aff7fa806e1cd4647380d6896d98a9191f2035d5a37cc35938de42b243188984aa2fced37bdbee3b2c3c6ef25d27bf2428bf9a0307cc3237c80560f
+DIST lean-3.42.1.tar.gz 1908398 BLAKE2B 7a83269deb3dc7ee60bf7a09b36df332355d9caf575b8435345956697121e95e1fb44cada1237e44bab04a56af4fb40c0d01e49f4cb3e4896e616f2bc58bf9ef SHA512 ab266e385e3026ce3219eef6ef171e243576e291fb26cef3d97ca4cc5190988e3bd6fe93c37a1192b8d2eec0ae7620131826ee1073a038f5a024e706953242d1

diff --git a/sci-mathematics/lean/lean-3.42.1.ebuild b/sci-mathematics/lean/lean-3.42.1.ebuild
new file mode 100644
index 000000000000..5d8ee8eecd4b
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.42.1.ebuild
@@ -0,0 +1,75 @@
+# 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 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="${WORKDIR}/lean-${PV}/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
+
+	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
+}

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

[Maciej Barć]

commit:     7640503c4f08775eef6ccf16d7a5ccb93ac5d25d
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sun Mar 27 00:57:39 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sun Mar 27 01:46:25 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=7640503c

sci-mathematics/lean: drop old 3.40.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.40.0.ebuild | 75 ---------------------------------
 2 files changed, 76 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 910ec2d2d32c..41cd0f0901a9 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,5 +1,4 @@
 DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd
-DIST lean-3.40.0.tar.gz 1878547 BLAKE2B 762c12b9fee9ac405730fb4a748326e7c9603c50f44512166f94df51e8cde0096803f11d0201980e1a1c0121a2b278075bf238452254d83e2d8b7b5566355416 SHA512 4daa32b60195a9776019c3c13c3765a1f5a817d78f189c3f92859298118815af4cb47359816ebbb977f35453be358956f3680b06b5930d5cf3a4245599602873
 DIST lean-3.41.0.tar.gz 1905966 BLAKE2B 1921ba4a975ed8fc6001695151bb366341e0895989a570bb7fbef1e719685945d0b7c51ed0716ff29daaf81af24ce2e289cab41b251c686a286cd94a0cf708f8 SHA512 855a56812ba5dc7cf431490957570d0fcbc4760faa1602095e708ddcc4e5a3c6aeac42133c210375d4538d97c8ae90df3ab3c7e7840e8896b8d0db439e925fbf
 DIST lean-3.42.0.tar.gz 1908134 BLAKE2B 7b6403786cc1a3a2b974f8df4c2bf2921e4e374ead4290a0e263c8464a9c009fd2f62e7cf5bdbc5087d0c9bb4c57f798b9d1a4b8ee2d66152714ec2af649e196 SHA512 2f1fc1bf3aff7fa806e1cd4647380d6896d98a9191f2035d5a37cc35938de42b243188984aa2fced37bdbee3b2c3c6ef25d27bf2428bf9a0307cc3237c80560f
 DIST lean-3.42.1.tar.gz 1908398 BLAKE2B 7a83269deb3dc7ee60bf7a09b36df332355d9caf575b8435345956697121e95e1fb44cada1237e44bab04a56af4fb40c0d01e49f4cb3e4896e616f2bc58bf9ef SHA512 ab266e385e3026ce3219eef6ef171e243576e291fb26cef3d97ca4cc5190988e3bd6fe93c37a1192b8d2eec0ae7620131826ee1073a038f5a024e706953242d1

diff --git a/sci-mathematics/lean/lean-3.40.0.ebuild b/sci-mathematics/lean/lean-3.40.0.ebuild
deleted file mode 100644
index 5d8ee8eecd4b..000000000000
--- a/sci-mathematics/lean/lean-3.40.0.ebuild
+++ /dev/null
@@ -1,75 +0,0 @@
-# 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 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="${WORKDIR}/lean-${PV}/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
-
-	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
-}

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

[Agostino Sarubbo]

commit:     6f0f88b35d832c70ae0fe4817a70623718d86bf4
Author:     Agostino Sarubbo <ago <AT> gentoo <DOT> org>
AuthorDate: Sat Mar 26 19:46:58 2022 +0000
Commit:     Agostino Sarubbo <ago <AT> gentoo <DOT> org>
CommitDate: Sat Mar 26 19:46:58 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=6f0f88b3

sci-mathematics/lean: amd64 stable wrt bug #835981

Package-Manager: Portage-3.0.30, Repoman-3.0.3
RepoMan-Options: --include-arches="amd64"
Signed-off-by: Agostino Sarubbo <ago <AT> gentoo.org>

 sci-mathematics/lean/lean-3.39.1.ebuild | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sci-mathematics/lean/lean-3.39.1.ebuild b/sci-mathematics/lean/lean-3.39.1.ebuild
index 5d8ee8eecd4b..d8b241bcd34b 100644
--- a/sci-mathematics/lean/lean-3.39.1.ebuild
+++ b/sci-mathematics/lean/lean-3.39.1.ebuild
@@ -16,7 +16,7 @@ if [[ "${PV}" == *9999* ]]; then
 	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"
+	KEYWORDS="amd64 ~x86"
 fi
 S="${WORKDIR}/lean-${PV}/src"
 

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

[Maciej Barć]

commit:     61bd2fdc46fc2e895d15dabd68a31c19322ad37f
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Fri Mar 18 18:29:39 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Fri Mar 18 19:37:48 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=61bd2fdc

sci-mathematics/lean: bump to 3.42.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.42.0.ebuild | 75 +++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 3ef12ca10328..ad0e723b1b3c 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd
 DIST lean-3.40.0.tar.gz 1878547 BLAKE2B 762c12b9fee9ac405730fb4a748326e7c9603c50f44512166f94df51e8cde0096803f11d0201980e1a1c0121a2b278075bf238452254d83e2d8b7b5566355416 SHA512 4daa32b60195a9776019c3c13c3765a1f5a817d78f189c3f92859298118815af4cb47359816ebbb977f35453be358956f3680b06b5930d5cf3a4245599602873
 DIST lean-3.41.0.tar.gz 1905966 BLAKE2B 1921ba4a975ed8fc6001695151bb366341e0895989a570bb7fbef1e719685945d0b7c51ed0716ff29daaf81af24ce2e289cab41b251c686a286cd94a0cf708f8 SHA512 855a56812ba5dc7cf431490957570d0fcbc4760faa1602095e708ddcc4e5a3c6aeac42133c210375d4538d97c8ae90df3ab3c7e7840e8896b8d0db439e925fbf
+DIST lean-3.42.0.tar.gz 1908134 BLAKE2B 7b6403786cc1a3a2b974f8df4c2bf2921e4e374ead4290a0e263c8464a9c009fd2f62e7cf5bdbc5087d0c9bb4c57f798b9d1a4b8ee2d66152714ec2af649e196 SHA512 2f1fc1bf3aff7fa806e1cd4647380d6896d98a9191f2035d5a37cc35938de42b243188984aa2fced37bdbee3b2c3c6ef25d27bf2428bf9a0307cc3237c80560f

diff --git a/sci-mathematics/lean/lean-3.42.0.ebuild b/sci-mathematics/lean/lean-3.42.0.ebuild
new file mode 100644
index 000000000000..5d8ee8eecd4b
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.42.0.ebuild
@@ -0,0 +1,75 @@
+# 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 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="${WORKDIR}/lean-${PV}/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
+
+	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
+}

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

[Maciej Barć]

commit:     3f0b44230b3002df360b247e3906e3c23d701f5a
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Mar 12 10:14:36 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Mar 12 10:15:11 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=3f0b4423

sci-mathematics/lean: drop old 3.38.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.38.0.ebuild | 75 ---------------------------------
 2 files changed, 76 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index d6c9758bdc2e..3ef12ca10328 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
-DIST lean-3.38.0.tar.gz 1877265 BLAKE2B 30d4364ee9d788ed128b63c42b5f7d55b91721ca74a6bc847e33f0d7be800cd2d3d90b4964e398f9116375afe6447a3f10f25ab716445aa9b7a5458d534bbf09 SHA512 441889f561a1fd369d2a4bc305e936834bb6c11ef85cfb4b69a5649226b405340fa787eb2ff73e44d2da6bb25a7819af70cf465abdf323777601c9f619c58508
 DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd
 DIST lean-3.40.0.tar.gz 1878547 BLAKE2B 762c12b9fee9ac405730fb4a748326e7c9603c50f44512166f94df51e8cde0096803f11d0201980e1a1c0121a2b278075bf238452254d83e2d8b7b5566355416 SHA512 4daa32b60195a9776019c3c13c3765a1f5a817d78f189c3f92859298118815af4cb47359816ebbb977f35453be358956f3680b06b5930d5cf3a4245599602873
 DIST lean-3.41.0.tar.gz 1905966 BLAKE2B 1921ba4a975ed8fc6001695151bb366341e0895989a570bb7fbef1e719685945d0b7c51ed0716ff29daaf81af24ce2e289cab41b251c686a286cd94a0cf708f8 SHA512 855a56812ba5dc7cf431490957570d0fcbc4760faa1602095e708ddcc4e5a3c6aeac42133c210375d4538d97c8ae90df3ab3c7e7840e8896b8d0db439e925fbf

diff --git a/sci-mathematics/lean/lean-3.38.0.ebuild b/sci-mathematics/lean/lean-3.38.0.ebuild
deleted file mode 100644
index 5d8ee8eecd4b..000000000000
--- a/sci-mathematics/lean/lean-3.38.0.ebuild
+++ /dev/null
@@ -1,75 +0,0 @@
-# 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 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="${WORKDIR}/lean-${PV}/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
-
-	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
-}

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

[Maciej Barć]

commit:     7746d09bf48110a2fb6d76732811beb2565171d6
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Mar 12 09:59:38 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Mar 12 10:11:51 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=7746d09b

sci-mathematics/lean: bump to 3.41.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.41.0.ebuild | 75 +++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index e447ce7628d4..d6c9758bdc2e 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.38.0.tar.gz 1877265 BLAKE2B 30d4364ee9d788ed128b63c42b5f7d55b91721ca74a6bc847e33f0d7be800cd2d3d90b4964e398f9116375afe6447a3f10f25ab716445aa9b7a5458d534bbf09 SHA512 441889f561a1fd369d2a4bc305e936834bb6c11ef85cfb4b69a5649226b405340fa787eb2ff73e44d2da6bb25a7819af70cf465abdf323777601c9f619c58508
 DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd
 DIST lean-3.40.0.tar.gz 1878547 BLAKE2B 762c12b9fee9ac405730fb4a748326e7c9603c50f44512166f94df51e8cde0096803f11d0201980e1a1c0121a2b278075bf238452254d83e2d8b7b5566355416 SHA512 4daa32b60195a9776019c3c13c3765a1f5a817d78f189c3f92859298118815af4cb47359816ebbb977f35453be358956f3680b06b5930d5cf3a4245599602873
+DIST lean-3.41.0.tar.gz 1905966 BLAKE2B 1921ba4a975ed8fc6001695151bb366341e0895989a570bb7fbef1e719685945d0b7c51ed0716ff29daaf81af24ce2e289cab41b251c686a286cd94a0cf708f8 SHA512 855a56812ba5dc7cf431490957570d0fcbc4760faa1602095e708ddcc4e5a3c6aeac42133c210375d4538d97c8ae90df3ab3c7e7840e8896b8d0db439e925fbf

diff --git a/sci-mathematics/lean/lean-3.41.0.ebuild b/sci-mathematics/lean/lean-3.41.0.ebuild
new file mode 100644
index 000000000000..5d8ee8eecd4b
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.41.0.ebuild
@@ -0,0 +1,75 @@
+# 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 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="${WORKDIR}/lean-${PV}/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
+
+	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
+}

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

[Maciej Barć]

commit:     3d11f6436d29d336eed1d2917507135ba0759e6d
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Feb 22 17:43:06 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Feb 22 18:34:04 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=3d11f643

sci-mathematics/lean: bump to 3.40.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.40.0.ebuild | 75 +++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 326d8bf80df0..940c3766d694 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.37.0.tar.gz 1875569 BLAKE2B 26d2513da35f0fa7efa6a9bb7706884b95666079e1c0d4349f2745a5908417c0b3d01027901425bf6bc4affdb314a79235c52bac9395bd9e54d53930e6b0dbe0 SHA512 c28139cfff7b40785ab51a9591964adc473f28d7a9877d891a132737c165ce6649924e6c75905442632452b9447c095aae830df347492bae058215d3392a7c09
 DIST lean-3.38.0.tar.gz 1877265 BLAKE2B 30d4364ee9d788ed128b63c42b5f7d55b91721ca74a6bc847e33f0d7be800cd2d3d90b4964e398f9116375afe6447a3f10f25ab716445aa9b7a5458d534bbf09 SHA512 441889f561a1fd369d2a4bc305e936834bb6c11ef85cfb4b69a5649226b405340fa787eb2ff73e44d2da6bb25a7819af70cf465abdf323777601c9f619c58508
 DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd
+DIST lean-3.40.0.tar.gz 1878547 BLAKE2B 762c12b9fee9ac405730fb4a748326e7c9603c50f44512166f94df51e8cde0096803f11d0201980e1a1c0121a2b278075bf238452254d83e2d8b7b5566355416 SHA512 4daa32b60195a9776019c3c13c3765a1f5a817d78f189c3f92859298118815af4cb47359816ebbb977f35453be358956f3680b06b5930d5cf3a4245599602873

diff --git a/sci-mathematics/lean/lean-3.40.0.ebuild b/sci-mathematics/lean/lean-3.40.0.ebuild
new file mode 100644
index 000000000000..e47a48054580
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.40.0.ebuild
@@ -0,0 +1,75 @@
+# 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 cmake optfeature 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="${WORKDIR}/lean-${PV}/src"
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug +json +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
+
+	local mycmakeargs=(
+		-DALPHA=ON
+		-DAUTO_THREAD_FINALIZATION=ON
+		-DJSON=$(usex json)
+		-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
+}

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

[Maciej Barć]

commit:     6e3bf14e2fb5e305a6bd887e804499bb2521f380
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Feb 22 17:43:36 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Feb 22 18:34:04 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=6e3bf14e

sci-mathematics/lean: drop old 3.37.0

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

 sci-mathematics/lean/Manifest           |  1 -
 sci-mathematics/lean/lean-3.37.0.ebuild | 75 ---------------------------------
 2 files changed, 76 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 940c3766d694..e447ce7628d4 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
-DIST lean-3.37.0.tar.gz 1875569 BLAKE2B 26d2513da35f0fa7efa6a9bb7706884b95666079e1c0d4349f2745a5908417c0b3d01027901425bf6bc4affdb314a79235c52bac9395bd9e54d53930e6b0dbe0 SHA512 c28139cfff7b40785ab51a9591964adc473f28d7a9877d891a132737c165ce6649924e6c75905442632452b9447c095aae830df347492bae058215d3392a7c09
 DIST lean-3.38.0.tar.gz 1877265 BLAKE2B 30d4364ee9d788ed128b63c42b5f7d55b91721ca74a6bc847e33f0d7be800cd2d3d90b4964e398f9116375afe6447a3f10f25ab716445aa9b7a5458d534bbf09 SHA512 441889f561a1fd369d2a4bc305e936834bb6c11ef85cfb4b69a5649226b405340fa787eb2ff73e44d2da6bb25a7819af70cf465abdf323777601c9f619c58508
 DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd
 DIST lean-3.40.0.tar.gz 1878547 BLAKE2B 762c12b9fee9ac405730fb4a748326e7c9603c50f44512166f94df51e8cde0096803f11d0201980e1a1c0121a2b278075bf238452254d83e2d8b7b5566355416 SHA512 4daa32b60195a9776019c3c13c3765a1f5a817d78f189c3f92859298118815af4cb47359816ebbb977f35453be358956f3680b06b5930d5cf3a4245599602873

diff --git a/sci-mathematics/lean/lean-3.37.0.ebuild b/sci-mathematics/lean/lean-3.37.0.ebuild
deleted file mode 100644
index e47a48054580..000000000000
--- a/sci-mathematics/lean/lean-3.37.0.ebuild
+++ /dev/null
@@ -1,75 +0,0 @@
-# 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 cmake optfeature 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="${WORKDIR}/lean-${PV}/src"
-
-LICENSE="Apache-2.0"
-SLOT="0/${MAJOR}"
-IUSE="debug +json +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
-
-	local mycmakeargs=(
-		-DALPHA=ON
-		-DAUTO_THREAD_FINALIZATION=ON
-		-DJSON=$(usex json)
-		-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
-}

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

[Maciej Barć]

commit:     024840070aea8eb50149f8f9d97df53a3f1fb940
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Feb 22 18:32:10 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Feb 22 18:34:04 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=02484007

sci-mathematics/lean: remove USE=json and inherit of optfeature

Closes: https://bugs.gentoo.org/833900
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 sci-mathematics/lean/lean-3.38.0.ebuild | 6 +++---
 sci-mathematics/lean/lean-3.39.1.ebuild | 6 +++---
 sci-mathematics/lean/lean-3.40.0.ebuild | 6 +++---
 sci-mathematics/lean/lean-3.9999.ebuild | 8 ++++----
 sci-mathematics/lean/metadata.xml       | 3 ---
 5 files changed, 13 insertions(+), 16 deletions(-)

diff --git a/sci-mathematics/lean/lean-3.38.0.ebuild b/sci-mathematics/lean/lean-3.38.0.ebuild
index e47a48054580..5d8ee8eecd4b 100644
--- a/sci-mathematics/lean/lean-3.38.0.ebuild
+++ b/sci-mathematics/lean/lean-3.38.0.ebuild
@@ -6,7 +6,7 @@ EAPI=8
 MAJOR=$(ver_cut 1)
 CMAKE_IN_SOURCE_BUILD="ON"
 
-inherit cmake optfeature readme.gentoo-r1
+inherit cmake readme.gentoo-r1
 
 DESCRIPTION="The Lean Theorem Prover"
 HOMEPAGE="https://leanprover-community.github.io/"
@@ -22,7 +22,7 @@ S="${WORKDIR}/lean-${PV}/src"
 
 LICENSE="Apache-2.0"
 SLOT="0/${MAJOR}"
-IUSE="debug +json +threads"
+IUSE="debug +threads"
 
 RDEPEND="dev-libs/gmp:="
 DEPEND="${RDEPEND}"
@@ -40,7 +40,7 @@ src_configure() {
 	local mycmakeargs=(
 		-DALPHA=ON
 		-DAUTO_THREAD_FINALIZATION=ON
-		-DJSON=$(usex json)
+		-DJSON=ON  # bug 833900
 		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
 		-DMULTI_THREAD=$(usex threads)
 		-DUSE_GITHASH=OFF

diff --git a/sci-mathematics/lean/lean-3.39.1.ebuild b/sci-mathematics/lean/lean-3.39.1.ebuild
index e47a48054580..5d8ee8eecd4b 100644
--- a/sci-mathematics/lean/lean-3.39.1.ebuild
+++ b/sci-mathematics/lean/lean-3.39.1.ebuild
@@ -6,7 +6,7 @@ EAPI=8
 MAJOR=$(ver_cut 1)
 CMAKE_IN_SOURCE_BUILD="ON"
 
-inherit cmake optfeature readme.gentoo-r1
+inherit cmake readme.gentoo-r1
 
 DESCRIPTION="The Lean Theorem Prover"
 HOMEPAGE="https://leanprover-community.github.io/"
@@ -22,7 +22,7 @@ S="${WORKDIR}/lean-${PV}/src"
 
 LICENSE="Apache-2.0"
 SLOT="0/${MAJOR}"
-IUSE="debug +json +threads"
+IUSE="debug +threads"
 
 RDEPEND="dev-libs/gmp:="
 DEPEND="${RDEPEND}"
@@ -40,7 +40,7 @@ src_configure() {
 	local mycmakeargs=(
 		-DALPHA=ON
 		-DAUTO_THREAD_FINALIZATION=ON
-		-DJSON=$(usex json)
+		-DJSON=ON  # bug 833900
 		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
 		-DMULTI_THREAD=$(usex threads)
 		-DUSE_GITHASH=OFF

diff --git a/sci-mathematics/lean/lean-3.40.0.ebuild b/sci-mathematics/lean/lean-3.40.0.ebuild
index e47a48054580..5d8ee8eecd4b 100644
--- a/sci-mathematics/lean/lean-3.40.0.ebuild
+++ b/sci-mathematics/lean/lean-3.40.0.ebuild
@@ -6,7 +6,7 @@ EAPI=8
 MAJOR=$(ver_cut 1)
 CMAKE_IN_SOURCE_BUILD="ON"
 
-inherit cmake optfeature readme.gentoo-r1
+inherit cmake readme.gentoo-r1
 
 DESCRIPTION="The Lean Theorem Prover"
 HOMEPAGE="https://leanprover-community.github.io/"
@@ -22,7 +22,7 @@ S="${WORKDIR}/lean-${PV}/src"
 
 LICENSE="Apache-2.0"
 SLOT="0/${MAJOR}"
-IUSE="debug +json +threads"
+IUSE="debug +threads"
 
 RDEPEND="dev-libs/gmp:="
 DEPEND="${RDEPEND}"
@@ -40,7 +40,7 @@ src_configure() {
 	local mycmakeargs=(
 		-DALPHA=ON
 		-DAUTO_THREAD_FINALIZATION=ON
-		-DJSON=$(usex json)
+		-DJSON=ON  # bug 833900
 		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
 		-DMULTI_THREAD=$(usex threads)
 		-DUSE_GITHASH=OFF

diff --git a/sci-mathematics/lean/lean-3.9999.ebuild b/sci-mathematics/lean/lean-3.9999.ebuild
index a15591b790f5..5d8ee8eecd4b 100644
--- a/sci-mathematics/lean/lean-3.9999.ebuild
+++ b/sci-mathematics/lean/lean-3.9999.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=8
@@ -6,7 +6,7 @@ EAPI=8
 MAJOR=$(ver_cut 1)
 CMAKE_IN_SOURCE_BUILD="ON"
 
-inherit cmake optfeature readme.gentoo-r1
+inherit cmake readme.gentoo-r1
 
 DESCRIPTION="The Lean Theorem Prover"
 HOMEPAGE="https://leanprover-community.github.io/"
@@ -22,7 +22,7 @@ S="${WORKDIR}/lean-${PV}/src"
 
 LICENSE="Apache-2.0"
 SLOT="0/${MAJOR}"
-IUSE="debug +json +threads"
+IUSE="debug +threads"
 
 RDEPEND="dev-libs/gmp:="
 DEPEND="${RDEPEND}"
@@ -40,7 +40,7 @@ src_configure() {
 	local mycmakeargs=(
 		-DALPHA=ON
 		-DAUTO_THREAD_FINALIZATION=ON
-		-DJSON=$(usex json)
+		-DJSON=ON  # bug 833900
 		-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
 		-DMULTI_THREAD=$(usex threads)
 		-DUSE_GITHASH=OFF

diff --git a/sci-mathematics/lean/metadata.xml b/sci-mathematics/lean/metadata.xml
index f06c80c2d7be..ddb0be8a571c 100644
--- a/sci-mathematics/lean/metadata.xml
+++ b/sci-mathematics/lean/metadata.xml
@@ -14,7 +14,4 @@
     <bugs-to>https://github.com/leanprover-community/lean/issues</bugs-to>
     <remote-id type="github">leanprover-community/lean</remote-id>
   </upstream>
-  <use>
-    <flag name="json"> Enable JSON support</flag>
-  </use>
 </pkgmetadata>

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

[Maciej Barć]

commit:     34df81ac434b83d7e7c4bfffb68959f67719a82c
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Feb  8 17:09:22 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Feb  8 17:21:23 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=34df81ac

sci-mathematics/lean: bump to 3.39.1

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.39.1.ebuild | 75 +++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index 225830067d1e..ccc3a53a1f35 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,3 +1,4 @@
 DIST lean-3.35.1.tar.gz 1872461 BLAKE2B 44635b05a7e8ea89522dfb44b8f097ec530419ab79a5413648292ca34019ca744ae3e327cf3a7c627cb7a7a682cfcb2ffc5e6802f2c5ad67e0a7abc303624a3c SHA512 24238cd9e920042f5bf7ba0a121da860e7e9c804d169c888bfabbc5e79e55f556a8920fab0c1a7e72b13501798c5f3fcb068f1705a0cf230f2b89abe1b3045ab
 DIST lean-3.37.0.tar.gz 1875569 BLAKE2B 26d2513da35f0fa7efa6a9bb7706884b95666079e1c0d4349f2745a5908417c0b3d01027901425bf6bc4affdb314a79235c52bac9395bd9e54d53930e6b0dbe0 SHA512 c28139cfff7b40785ab51a9591964adc473f28d7a9877d891a132737c165ce6649924e6c75905442632452b9447c095aae830df347492bae058215d3392a7c09
 DIST lean-3.38.0.tar.gz 1877265 BLAKE2B 30d4364ee9d788ed128b63c42b5f7d55b91721ca74a6bc847e33f0d7be800cd2d3d90b4964e398f9116375afe6447a3f10f25ab716445aa9b7a5458d534bbf09 SHA512 441889f561a1fd369d2a4bc305e936834bb6c11ef85cfb4b69a5649226b405340fa787eb2ff73e44d2da6bb25a7819af70cf465abdf323777601c9f619c58508
+DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd

diff --git a/sci-mathematics/lean/lean-3.39.1.ebuild b/sci-mathematics/lean/lean-3.39.1.ebuild
new file mode 100644
index 000000000000..e47a48054580
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.39.1.ebuild
@@ -0,0 +1,75 @@
+# 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 cmake optfeature 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="${WORKDIR}/lean-${PV}/src"
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug +json +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
+
+	local mycmakeargs=(
+		-DALPHA=ON
+		-DAUTO_THREAD_FINALIZATION=ON
+		-DJSON=$(usex json)
+		-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
+}

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

[Maciej Barć]

commit:     4db633aab7e4f7334eb29434098fd7a18f428b9e
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Feb  8 17:11:41 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Feb  8 17:21:23 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=4db633aa

sci-mathematics/lean: drop old 3.35.1-r2

Closes: https://bugs.gentoo.org/828088
Package-Manager: Portage-3.0.30, Repoman-3.0.3
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 sci-mathematics/lean/Manifest              |  1 -
 sci-mathematics/lean/lean-3.35.1-r2.ebuild | 75 ------------------------------
 2 files changed, 76 deletions(-)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index ccc3a53a1f35..326d8bf80df0 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,4 +1,3 @@
-DIST lean-3.35.1.tar.gz 1872461 BLAKE2B 44635b05a7e8ea89522dfb44b8f097ec530419ab79a5413648292ca34019ca744ae3e327cf3a7c627cb7a7a682cfcb2ffc5e6802f2c5ad67e0a7abc303624a3c SHA512 24238cd9e920042f5bf7ba0a121da860e7e9c804d169c888bfabbc5e79e55f556a8920fab0c1a7e72b13501798c5f3fcb068f1705a0cf230f2b89abe1b3045ab
 DIST lean-3.37.0.tar.gz 1875569 BLAKE2B 26d2513da35f0fa7efa6a9bb7706884b95666079e1c0d4349f2745a5908417c0b3d01027901425bf6bc4affdb314a79235c52bac9395bd9e54d53930e6b0dbe0 SHA512 c28139cfff7b40785ab51a9591964adc473f28d7a9877d891a132737c165ce6649924e6c75905442632452b9447c095aae830df347492bae058215d3392a7c09
 DIST lean-3.38.0.tar.gz 1877265 BLAKE2B 30d4364ee9d788ed128b63c42b5f7d55b91721ca74a6bc847e33f0d7be800cd2d3d90b4964e398f9116375afe6447a3f10f25ab716445aa9b7a5458d534bbf09 SHA512 441889f561a1fd369d2a4bc305e936834bb6c11ef85cfb4b69a5649226b405340fa787eb2ff73e44d2da6bb25a7819af70cf465abdf323777601c9f619c58508
 DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd

diff --git a/sci-mathematics/lean/lean-3.35.1-r2.ebuild b/sci-mathematics/lean/lean-3.35.1-r2.ebuild
deleted file mode 100644
index a15591b790f5..000000000000
--- a/sci-mathematics/lean/lean-3.35.1-r2.ebuild
+++ /dev/null
@@ -1,75 +0,0 @@
-# Copyright 1999-2021 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 cmake optfeature 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="${WORKDIR}/lean-${PV}/src"
-
-LICENSE="Apache-2.0"
-SLOT="0/${MAJOR}"
-IUSE="debug +json +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
-
-	local mycmakeargs=(
-		-DALPHA=ON
-		-DAUTO_THREAD_FINALIZATION=ON
-		-DJSON=$(usex json)
-		-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
-}

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

[Maciej Barć]

commit:     f45b887a09c256445f76e9764e27501424636a83
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sun Jan 30 19:21:08 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sun Jan 30 19:21:28 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=f45b887a

sci-mathematics/lean: bump to 3.38.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.38.0.ebuild | 75 +++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index f0d02b545bdd..225830067d1e 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,2 +1,3 @@
 DIST lean-3.35.1.tar.gz 1872461 BLAKE2B 44635b05a7e8ea89522dfb44b8f097ec530419ab79a5413648292ca34019ca744ae3e327cf3a7c627cb7a7a682cfcb2ffc5e6802f2c5ad67e0a7abc303624a3c SHA512 24238cd9e920042f5bf7ba0a121da860e7e9c804d169c888bfabbc5e79e55f556a8920fab0c1a7e72b13501798c5f3fcb068f1705a0cf230f2b89abe1b3045ab
 DIST lean-3.37.0.tar.gz 1875569 BLAKE2B 26d2513da35f0fa7efa6a9bb7706884b95666079e1c0d4349f2745a5908417c0b3d01027901425bf6bc4affdb314a79235c52bac9395bd9e54d53930e6b0dbe0 SHA512 c28139cfff7b40785ab51a9591964adc473f28d7a9877d891a132737c165ce6649924e6c75905442632452b9447c095aae830df347492bae058215d3392a7c09
+DIST lean-3.38.0.tar.gz 1877265 BLAKE2B 30d4364ee9d788ed128b63c42b5f7d55b91721ca74a6bc847e33f0d7be800cd2d3d90b4964e398f9116375afe6447a3f10f25ab716445aa9b7a5458d534bbf09 SHA512 441889f561a1fd369d2a4bc305e936834bb6c11ef85cfb4b69a5649226b405340fa787eb2ff73e44d2da6bb25a7819af70cf465abdf323777601c9f619c58508

diff --git a/sci-mathematics/lean/lean-3.38.0.ebuild b/sci-mathematics/lean/lean-3.38.0.ebuild
new file mode 100644
index 000000000000..e47a48054580
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.38.0.ebuild
@@ -0,0 +1,75 @@
+# 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 cmake optfeature 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="${WORKDIR}/lean-${PV}/src"
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug +json +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
+
+	local mycmakeargs=(
+		-DALPHA=ON
+		-DAUTO_THREAD_FINALIZATION=ON
+		-DJSON=$(usex json)
+		-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
+}

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

[Maciej Barć]

commit:     6e592397386181641bc0ca1cd8c40417a460e5cd
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Jan  8 03:01:49 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Jan  8 03:02:06 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=6e592397

sci-mathematics/lean: bump to 3.37.0

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

 sci-mathematics/lean/Manifest           |  1 +
 sci-mathematics/lean/lean-3.37.0.ebuild | 75 +++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index cad21881763c..f0d02b545bdd 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1 +1,2 @@
 DIST lean-3.35.1.tar.gz 1872461 BLAKE2B 44635b05a7e8ea89522dfb44b8f097ec530419ab79a5413648292ca34019ca744ae3e327cf3a7c627cb7a7a682cfcb2ffc5e6802f2c5ad67e0a7abc303624a3c SHA512 24238cd9e920042f5bf7ba0a121da860e7e9c804d169c888bfabbc5e79e55f556a8920fab0c1a7e72b13501798c5f3fcb068f1705a0cf230f2b89abe1b3045ab
+DIST lean-3.37.0.tar.gz 1875569 BLAKE2B 26d2513da35f0fa7efa6a9bb7706884b95666079e1c0d4349f2745a5908417c0b3d01027901425bf6bc4affdb314a79235c52bac9395bd9e54d53930e6b0dbe0 SHA512 c28139cfff7b40785ab51a9591964adc473f28d7a9877d891a132737c165ce6649924e6c75905442632452b9447c095aae830df347492bae058215d3392a7c09

diff --git a/sci-mathematics/lean/lean-3.37.0.ebuild b/sci-mathematics/lean/lean-3.37.0.ebuild
new file mode 100644
index 000000000000..e47a48054580
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.37.0.ebuild
@@ -0,0 +1,75 @@
+# 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 cmake optfeature 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="${WORKDIR}/lean-${PV}/src"
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug +json +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
+
+	local mycmakeargs=(
+		-DALPHA=ON
+		-DAUTO_THREAD_FINALIZATION=ON
+		-DJSON=$(usex json)
+		-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
+}

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

[Maciej Barć]

commit:     3c03d7044dd45cd23b5a4cb8bef5f0d9c0e121eb
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Dec 25 20:41:29 2021 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Dec 25 20:41:29 2021 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=3c03d704

sci-mathematics/lean: change maintainer to Gentoo Mathematics Project

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

 sci-mathematics/lean/metadata.xml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/sci-mathematics/lean/metadata.xml b/sci-mathematics/lean/metadata.xml
index 278e5b1a42a2..efbd9f15e639 100644
--- a/sci-mathematics/lean/metadata.xml
+++ b/sci-mathematics/lean/metadata.xml
@@ -2,11 +2,11 @@
 <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
 
 <pkgmetadata>
-  <maintainer type="person">
-    <email>xgqt@gentoo.org</email>
-    <name>Maciej Barć</name>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
   </maintainer>
-  <longdescription lang="en">
+  <longdescription>
     The Lean theorem prover is a proof assistant developed principally
     by Leonardo de Moura at Microsoft Research.
   </longdescription>

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

[Maciej Barć]

commit:     0539348664c95ea43e2156585ecedcc306ce7513
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Dec  4 02:29:23 2021 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Dec  4 02:36:10 2021 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=05393486

sci-mathematics/lean: gmp slot

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

 sci-mathematics/lean/{lean-3.35.1-r1.ebuild => lean-3.35.1-r2.ebuild} | 2 +-
 sci-mathematics/lean/lean-3.9999.ebuild                               | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/sci-mathematics/lean/lean-3.35.1-r1.ebuild b/sci-mathematics/lean/lean-3.35.1-r2.ebuild
similarity index 98%
rename from sci-mathematics/lean/lean-3.35.1-r1.ebuild
rename to sci-mathematics/lean/lean-3.35.1-r2.ebuild
index cc208dc27850..a15591b790f5 100644
--- a/sci-mathematics/lean/lean-3.35.1-r1.ebuild
+++ b/sci-mathematics/lean/lean-3.35.1-r2.ebuild
@@ -24,7 +24,7 @@ LICENSE="Apache-2.0"
 SLOT="0/${MAJOR}"
 IUSE="debug +json +threads"
 
-RDEPEND="dev-libs/gmp"
+RDEPEND="dev-libs/gmp:="
 DEPEND="${RDEPEND}"
 
 PATCHES=( "${FILESDIR}/${PN}-CMakeLists-fix_flags.patch" )

diff --git a/sci-mathematics/lean/lean-3.9999.ebuild b/sci-mathematics/lean/lean-3.9999.ebuild
index cc208dc27850..a15591b790f5 100644
--- a/sci-mathematics/lean/lean-3.9999.ebuild
+++ b/sci-mathematics/lean/lean-3.9999.ebuild
@@ -24,7 +24,7 @@ LICENSE="Apache-2.0"
 SLOT="0/${MAJOR}"
 IUSE="debug +json +threads"
 
-RDEPEND="dev-libs/gmp"
+RDEPEND="dev-libs/gmp:="
 DEPEND="${RDEPEND}"
 
 PATCHES=( "${FILESDIR}/${PN}-CMakeLists-fix_flags.patch" )

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

[Maciej Barć]

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

sci-mathematics/lean: add live

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

 sci-mathematics/lean/lean-3.9999.ebuild | 75 +++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)

diff --git a/sci-mathematics/lean/lean-3.9999.ebuild b/sci-mathematics/lean/lean-3.9999.ebuild
new file mode 100644
index 000000000000..cc208dc27850
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.9999.ebuild
@@ -0,0 +1,75 @@
+# Copyright 1999-2021 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 cmake optfeature 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="${WORKDIR}/lean-${PV}/src"
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug +json +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
+
+	local mycmakeargs=(
+		-DALPHA=ON
+		-DAUTO_THREAD_FINALIZATION=ON
+		-DJSON=$(usex json)
+		-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
+}

[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
 }