[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/
commit: 15dff3a1f5bd74ef84c1f6679be0a464418c60ff
Author: Sam James gentoo org>
AuthorDate: Thu Jan 18 17:23:39 2024 +
Commit: Sam James gentoo org>
CommitDate: Thu Jan 18 17:23:39 2024 +
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 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/
commit: c424b1a0464033e5499ea963860773dbf0fea6a0
Author: Maciej Barć gentoo org>
AuthorDate: Mon Jan 15 20:10:03 2024 +
Commit: Maciej Barć gentoo org>
CommitDate: Mon Jan 15 21:20:41 2024 +
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ć 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..
--- 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}" == ** ]] ; 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/
commit: b6d29d865fb76d54ffbae7eefa32b2ac04a5cff1
Author: Maciej Barć gentoo org>
AuthorDate: Thu Nov 30 09:46:49 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu Nov 30 16:52:25 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=b6d29d86
sci-mathematics/lean: bump to 4.2.0
Signed-off-by: Maciej Barć 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 ..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}" == ** ]] ; 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/
commit: 2ebcc7f39c3ec50ee080478c0651a13b753b0e90
Author: Maciej Barć gentoo org>
AuthorDate: Thu Oct 26 10:06:36 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu Oct 26 13:11:35 2023 +
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ć 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 ..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}" == ** ]] ; 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/
commit: 0a9f17ccefbfe98fa6b5d3698f412e4def72048b
Author: Maciej Barć gentoo org>
AuthorDate: Wed Oct 25 20:03:32 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu Oct 26 13:11:35 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0a9f17cc
sci-mathematics/lean: drop old 3.
Signed-off-by: Maciej Barć gentoo.org>
sci-mathematics/lean/lean-3..ebuild | 80 -
1 file changed, 80 deletions(-)
diff --git a/sci-mathematics/lean/lean-3..ebuild
b/sci-mathematics/lean/lean-3..ebuild
deleted file mode 100644
index 72a23985077c..
--- a/sci-mathematics/lean/lean-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} == ** ]] ; 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/
commit: a34aff2a52124ee5a1ff2c7d8e01aadbc9a55254
Author: Maciej Barć gentoo org>
AuthorDate: Sat Oct 7 14:53:12 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Oct 7 14:57:43 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=a34aff2a
sci-mathematics/lean: drop old 3.49.0
Signed-off-by: Maciej Barć 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..
--- 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} == ** ]] ; 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/
commit: fa16ba57a6b933ac4c43fb6cffa5c3299fafa616
Author: Maciej Barć gentoo org>
AuthorDate: Sat Oct 7 14:53:08 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Oct 7 14:57:43 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=fa16ba57
sci-mathematics/lean: drop old 3.50.3
Signed-off-by: Maciej Barć 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..
--- 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} == ** ]] ; 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/
commit: 479d6e498b77704daeaa13b6643c00bb1915aea5
Author: Maciej Barć gentoo org>
AuthorDate: Sat Oct 7 14:53:03 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Oct 7 14:57:42 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=479d6e49
sci-mathematics/lean: drop old 3.51.0
Signed-off-by: Maciej Barć 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..
--- 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} == ** ]] ; 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/
commit: ae428f64fdaf392bc0ed57cef1ec5915fdd4d5c2
Author: Arthur Zamarin gentoo org>
AuthorDate: Tue Aug 15 15:45:33 2023 +
Commit: Arthur Zamarin gentoo org>
CommitDate: Tue Aug 15 15:45:33 2023 +
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 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} == ** ]] ; 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/
commit: 0a01120cbca04b48ee8e276775bca1d68184ad51
Author: Sam James gentoo org>
AuthorDate: Fri May 26 07:14:40 2023 +
Commit: Sam James gentoo org>
CommitDate: Fri May 26 07:14:47 2023 +
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 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} == ** ]] ; 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/
commit: fe3cf754c1e7031e14cfbe8491fc00e6de38ab81
Author: Maciej Barć gentoo org>
AuthorDate: Wed May 24 23:15:06 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Wed May 24 23:15:06 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=fe3cf754
sci-mathematics/lean: bump to 3.51.1
Signed-off-by: Maciej Barć 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 ..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} == ** ]] ; 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/
commit: 2700367b2e05b7d45e0400d13a6d1256206a2300
Author: Maciej Barć gentoo org>
AuthorDate: Wed May 17 20:21:02 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Wed May 17 20:45:10 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2700367b
sci-mathematics/lean: bump to 3.51.0
Signed-off-by: Maciej Barć 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 ..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} == ** ]] ; 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/
commit: 0821d9165c3618576c8658be0545906e3b85d9a5
Author: Maciej Barć gentoo org>
AuthorDate: Tue Apr 18 13:08:13 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Apr 18 13:55:10 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0821d916
sci-mathematics/lean: drop old 3.50.1
Signed-off-by: Maciej Barć 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..
--- 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} == ** ]] ; 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/
commit: 794b21a627436b9189d5ac0caede74e2936c5de8
Author: Maciej Barć gentoo org>
AuthorDate: Tue Apr 18 13:08:18 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Apr 18 13:55:10 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=794b21a6
sci-mathematics/lean: drop old 3.50.2
Signed-off-by: Maciej Barć 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..
--- 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} == ** ]] ; 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/, sci-mathematics/lean/files/
commit: 93eca38ef76c1a9c568155659b891db542f22939
Author: Maciej Barć gentoo org>
AuthorDate: Tue Apr 18 13:52:42 2023 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Apr 18 13:55:10 2023 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=93eca38e
sci-mathematics/lean: fix build with GCC 13
Closes: https://bugs.gentoo.org/895202
Signed-off-by: Maciej Barć gentoo.org>
sci-mathematics/lean/files/lean-3.50.3-gcc-13.patch | 10 ++
sci-mathematics/lean/lean-3.50.3.ebuild | 11 +++
sci-mathematics/lean/lean-3..ebuild | 13 -
3 files changed, 25 insertions(+), 9 deletions(-)
diff --git a/sci-mathematics/lean/files/lean-3.50.3-gcc-13.patch
b/sci-mathematics/lean/files/lean-3.50.3-gcc-13.patch
new file mode 100644
index ..273dd5161080
--- /dev/null
+++ b/sci-mathematics/lean/files/lean-3.50.3-gcc-13.patch
@@ -0,0 +1,10 @@
+--- a/shell/lean_js_main.cpp
b/shell/lean_js_main.cpp
+@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file
LICENSE.
+
+ Author: Leonardo de Moura
+ */
++#include
+ #include
+ #include
+ #include "shell/lean_js.h"
diff --git a/sci-mathematics/lean/lean-3.50.3.ebuild
b/sci-mathematics/lean/lean-3.50.3.ebuild
index e008b81cf582..72a23985077c 100644
--- a/sci-mathematics/lean/lean-3.50.3.ebuild
+++ b/sci-mathematics/lean/lean-3.50.3.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
@@ -27,7 +27,10 @@ IUSE="debug +threads"
RDEPEND="dev-libs/gmp:="
DEPEND="${RDEPEND}"
-PATCHES=( "${FILESDIR}"/${PN}-CMakeLists-fix_flags.patch )
+PATCHES=(
+ "${FILESDIR}"/${PN}-3.50.3-gcc-13.patch
+ "${FILESDIR}"/${PN}-CMakeLists-fix_flags.patch
+)
src_configure() {
local CMAKE_BUILD_TYPE
@@ -39,7 +42,7 @@ src_configure() {
filter-lto
- local mycmakeargs=(
+ local -a mycmakeargs=(
-DALPHA=ON
-DAUTO_THREAD_FINALIZATION=ON
-DJSON=ON # bug 833900
@@ -51,7 +54,7 @@ src_configure() {
}
src_test() {
- local myctestargs=(
+ local -a myctestargs=(
# Disable problematic "style_check" cpplint test,
# this also removes the python test dependency
--exclude-regex style_check
diff --git a/sci-mathematics/lean/lean-3..ebuild
b/sci-mathematics/lean/lean-3..ebuild
index 307c5b95bc1b..72a23985077c 100644
--- a/sci-mathematics/lean/lean-3..ebuild
+++ b/sci-mathematics/lean/lean-3..ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
@@ -11,7 +11,7 @@ inherit flag-o-matic cmake readme.gentoo-r1
DESCRIPTION="The Lean Theorem Prover"
HOMEPAGE="https://leanprover-community.github.io/;
-if [[ ${PV} == ** ]]; then
+if [[ ${PV} == ** ]] ; then
inherit git-r3
EGIT_REPO_URI="https://github.com/leanprover-community/lean.git;
else
@@ -27,7 +27,10 @@ IUSE="debug +threads"
RDEPEND="dev-libs/gmp:="
DEPEND="${RDEPEND}"
-PATCHES=( "${FILESDIR}"/${PN}-CMakeLists-fix_flags.patch )
+PATCHES=(
+ "${FILESDIR}"/${PN}-3.50.3-gcc-13.patch
+ "${FILESDIR}"/${PN}-CMakeLists-fix_flags.patch
+)
src_configure() {
local CMAKE_BUILD_TYPE
@@ -39,7 +42,7 @@ src_configure() {
filter-lto
- local mycmakeargs=(
+ local -a mycmakeargs=(
-DALPHA=ON
-DAUTO_THREAD_FINALIZATION=ON
-DJSON=ON # bug 833900
@@ -51,7 +54,7 @@ src_configure() {
}
src_test() {
- local myctestargs=(
+ local -a myctestargs=(
# Disable problematic "style_check" cpplint test,
# this also removes the python test dependency
--exclude-regex style_check
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/
commit: 6ae7758296c1aeb975019f0d0b72ce3aac209512
Author: Maciej Barć gentoo org>
AuthorDate: Tue Dec 27 02:01:24 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Dec 27 02:01:24 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=6ae77582
sci-mathematics/lean: drop old 3.50.0
Signed-off-by: Maciej Barć 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..
--- 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} == ** ]] ; 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/
commit: ca603043a7b48df6477fe7addee7dddadfad2664
Author: Maciej Barć gentoo org>
AuthorDate: Tue Dec 27 02:14:07 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Dec 27 02:14:07 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ca603043
sci-mathematics/lean: bump to 3.50.3
Signed-off-by: Maciej Barć 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 ..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} == ** ]] ; 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/
commit: fb75aa659ac9fd8c44cb96b3c45441cca6ff58a0
Author: Maciej Barć gentoo org>
AuthorDate: Sat Dec 24 02:45:46 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Dec 24 02:47:21 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=fb75aa65
sci-mathematics/lean: bump to 3.50.2
Signed-off-by: Maciej Barć 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 ..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} == ** ]] ; 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/
commit: 9c2a388c47e62f982dd56125265afec2ceac9de7
Author: Maciej Barć gentoo org>
AuthorDate: Sat Dec 24 02:35:51 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Dec 24 02:47:21 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=9c2a388c
sci-mathematics/lean: drop old 3.49.1
Signed-off-by: Maciej Barć 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..
--- 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} == ** ]] ; 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/
commit: b9d8d9bfb9a22e7736057a5aa9d7a83876caa5d9
Author: Sam James gentoo org>
AuthorDate: Wed Dec 21 23:51:55 2022 +
Commit: Sam James gentoo org>
CommitDate: Wed Dec 21 23:52:01 2022 +
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 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} == ** ]] ; 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/
commit: 9d57ecf9103a6e6d1a83e9c066531624660345ca
Author: Maciej Barć gentoo org>
AuthorDate: Wed Dec 21 23:32:02 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Wed Dec 21 23:49:28 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=9d57ecf9
sci-mathematics/lean: bump to 3.50.1
Signed-off-by: Maciej Barć 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 ..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} == ** ]] ; 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/
commit: ff43595f6fc27b3ffca106f140c5e677f7c38418
Author: Maciej Barć gentoo org>
AuthorDate: Thu Dec 15 08:31:04 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu Dec 15 08:41:12 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ff43595f
sci-mathematics/lean: bump to 3.50.0
Signed-off-by: Maciej Barć 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 ..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} == ** ]] ; 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/
commit: ad73daf529a2e367c224390bf18f17e72fa3ccd3
Author: Maciej Barć gentoo org>
AuthorDate: Thu Dec 15 08:17:58 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu Dec 15 08:41:12 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=ad73daf5
sci-mathematics/lean: drop old 3.48.0
Signed-off-by: Maciej Barć 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..
--- 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} == ** ]] ; 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/
commit: c07ecd3a781cdb9c02c6b9b3c212e46c528d6de5
Author: Maciej Barć gentoo org>
AuthorDate: Thu Dec 15 08:16:23 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu Dec 15 08:41:12 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c07ecd3a
sci-mathematics/lean: drop old 3.47.0
Signed-off-by: Maciej Barć 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..
--- 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} == ** ]] ; 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/
commit: 9f378b9a170e462527b9d6580df1f653a7ab15e1
Author: Maciej Barć gentoo org>
AuthorDate: Fri Nov 18 22:13:11 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Fri Nov 18 22:15:13 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=9f378b9a
sci-mathematics/lean: bump to 3.49.1
Signed-off-by: Maciej Barć 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 ..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} == ** ]] ; 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/
commit: e8151b7873f72fce1435682a90e2a41fa464ae35
Author: Maciej Barć gentoo org>
AuthorDate: Sat Nov 12 04:33:22 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Nov 12 05:02:55 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e8151b78
sci-mathematics/lean: bump to 3.49.0
Signed-off-by: Maciej Barć 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 ..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} == ** ]] ; 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/
commit: 3a343e45ca66c1757266e59583465526adf1c056
Author: Maciej Barć gentoo org>
AuthorDate: Sat Nov 12 05:02:46 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Nov 12 05:02:55 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=3a343e45
sci-mathematics/lean: drop old 3.46.0
Signed-off-by: Maciej Barć 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..
--- 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}" == ** ]]; 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/
commit: e0ab0acc6d5afb6a4ada31765fefad105c05a204
Author: Maciej Barć gentoo org>
AuthorDate: Tue Aug 30 14:35:20 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Aug 30 14:35:36 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e0ab0acc
sci-mathematics/lean: drop old 3.45.0
Signed-off-by: Maciej Barć 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
f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f724184469400ec354a194cc345feca8f0dbcb06a673cc2d3d4
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..
--- 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}" == ** ]]; 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/
commit: 4c42b4e422dded92c6d4964caf09f6d6ac9c5800
Author: Maciej Barć gentoo org>
AuthorDate: Tue Aug 30 13:42:47 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Aug 30 14:35:35 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=4c42b4e4
sci-mathematics/lean: bump to 3.48.0
Signed-off-by: Maciej Barć 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
f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f724184469400ec354a194cc345feca8f0dbcb06a673cc2d3d4
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 ..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} == ** ]] ; 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/
commit: 48ab1124b5f76709034a86da56caa70933173cef
Author: Maciej Barć gentoo org>
AuthorDate: Fri Aug 26 00:12:51 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Fri Aug 26 00:32:04 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=48ab1124
sci-mathematics/lean: bump to 3.47.0
Signed-off-by: Maciej Barć 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
f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f724184469400ec354a194cc345feca8f0dbcb06a673cc2d3d4
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 ..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} == ** ]] ; 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/
commit: c872faa59cdf7824ca359cbd30682806fa636898
Author: Maciej Barć gentoo org>
AuthorDate: Fri Aug 26 00:15:03 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Fri Aug 26 00:32:05 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c872faa5
sci-mathematics/lean: drop old 3.44.1
Signed-off-by: Maciej Barć 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
f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f724184469400ec354a194cc345feca8f0dbcb06a673cc2d3d4
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..
--- 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}" == ** ]]; 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/
commit: 83a2c3f160fefff958a12efb306e3ad54e3bd159
Author: Maciej Barć gentoo org>
AuthorDate: Fri Aug 26 00:12:18 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Fri Aug 26 00:32:04 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=83a2c3f1
sci-mathematics/lean: fix live
Signed-off-by: Maciej Barć gentoo.org>
sci-mathematics/lean/lean-3..ebuild | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/sci-mathematics/lean/lean-3..ebuild
b/sci-mathematics/lean/lean-3..ebuild
index 6623228581a0..307c5b95bc1b 100644
--- a/sci-mathematics/lean/lean-3..ebuild
+++ b/sci-mathematics/lean/lean-3..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}" == ** ]]; then
+if [[ ${PV} == ** ]]; 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/
commit: 3b93a2c696da21d2f18531ea9ed81c730e73e69f
Author: Maciej Barć gentoo org>
AuthorDate: Tue Aug 9 00:02:09 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Aug 9 00:02:09 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=3b93a2c6
sci-mathematics/lean: drop old 3.43.0
Signed-off-by: Maciej Barć 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
f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f724184469400ec354a194cc345feca8f0dbcb06a673cc2d3d4
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..
--- 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}" == ** ]]; 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/
commit: b5dd196eb69a20afced12e16dfdb0235ed590f52
Author: Maciej Barć gentoo org>
AuthorDate: Mon Aug 8 23:59:11 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Mon Aug 8 23:59:11 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=b5dd196e
sci-mathematics/lean: bump to 3.46.0
Signed-off-by: Maciej Barć 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
f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f724184469400ec354a194cc345feca8f0dbcb06a673cc2d3d4
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 ..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}" == ** ]]; 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/
commit: 56a7877fca5ed96053d93689e4e4a28786f3003f
Author: Maciej Barć gentoo org>
AuthorDate: Tue Aug 2 21:42:02 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Aug 2 21:42:18 2022 +
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ć 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..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..ebuild
b/sci-mathematics/lean/lean-3..ebuild
index 5d8ee8eecd4b..6623228581a0 100644
--- a/sci-mathematics/lean/lean-3..ebuild
+++ b/sci-mathematics/lean/lean-3..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/
commit: 57d436b81243c5cd193dadc99d83aaaf61513017
Author: Maciej Barć gentoo org>
AuthorDate: Thu Jul 14 09:38:26 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu Jul 14 10:05:27 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=57d436b8
sci-mathematics/lean: drop old 3.42.1
Signed-off-by: Maciej Barć 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
f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f724184469400ec354a194cc345feca8f0dbcb06a673cc2d3d4
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..
--- 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}" == ** ]]; 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/
commit: a8bce87f953078b3eadf7659b15626c415ce13cd
Author: Maciej Barć gentoo org>
AuthorDate: Thu Jul 14 08:06:54 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Thu Jul 14 10:05:26 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=a8bce87f
sci-mathematics/lean: bump to 3.45.0
Signed-off-by: Maciej Barć 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
f36548be556407cbf7b30a7988bb2454542543cafcd2d0f2af90f75f886d4b711c6955503f724184469400ec354a194cc345feca8f0dbcb06a673cc2d3d4
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 ..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}" == ** ]]; 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/
commit: b276a47dda6fd8ab8a9a8aa332776bcea2e35ee0
Author: Maciej Barć gentoo org>
AuthorDate: Mon Jun 27 14:42:04 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Mon Jun 27 14:50:17 2022 +
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ć 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
b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af
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..
--- 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}" == ** ]]; 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..
--- a/sci-mathematics/lean/lean-3.42.0.ebuild
+++ /dev/null
@@ -1,75 +0,0 @@
-# Copyright 1999-2022
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/
commit: 657666c6a8b6cbfc7a0acdb14d343300c056f54a
Author: Maciej Barć gentoo org>
AuthorDate: Mon Jun 27 14:41:16 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Mon Jun 27 14:50:17 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=657666c6
sci-mathematics/lean: bump to 3.44.1
Signed-off-by: Maciej Barć 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 ..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}" == ** ]]; 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/
commit: 2d71d221298ddf5a54541872cfdb99799e1246d6
Author: Maciej Barć gentoo org>
AuthorDate: Wed May 18 19:13:55 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Wed May 18 19:29:55 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2d71d221
sci-mathematics/lean: bump to 3.43.0
Signed-off-by: Maciej Barć 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 ..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}" == ** ]]; 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/
commit: 36d52f5fb108e6cc0663a6cbfdce443127a6577f
Author: Maciej Barć gentoo org>
AuthorDate: Wed May 18 19:14:16 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Wed May 18 19:29:56 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=36d52f5f
sci-mathematics/lean: drop old 3.41.0
Signed-off-by: Maciej Barć 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
b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af
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..
--- 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}" == ** ]]; 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/
commit: 7640503c4f08775eef6ccf16d7a5ccb93ac5d25d
Author: Maciej Barć gentoo org>
AuthorDate: Sun Mar 27 00:57:39 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Sun Mar 27 01:46:25 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=7640503c
sci-mathematics/lean: drop old 3.40.0
Signed-off-by: Maciej Barć 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
b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af
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..
--- 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}" == ** ]]; 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/
commit: e124cd89e3a8e36edbccc14fd5b791b8c11b9857
Author: Maciej Barć gentoo org>
AuthorDate: Sun Mar 27 00:56:32 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Sun Mar 27 01:46:25 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=e124cd89
sci-mathematics/lean: bump to 3.42.1
Signed-off-by: Maciej Barć 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 ..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}" == ** ]]; 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/
commit: 6f0f88b35d832c70ae0fe4817a70623718d86bf4
Author: Agostino Sarubbo gentoo org>
AuthorDate: Sat Mar 26 19:46:58 2022 +
Commit: Agostino Sarubbo gentoo org>
CommitDate: Sat Mar 26 19:46:58 2022 +
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 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}" == ** ]]; 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/
commit: 61bd2fdc46fc2e895d15dabd68a31c19322ad37f
Author: Maciej Barć gentoo org>
AuthorDate: Fri Mar 18 18:29:39 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Fri Mar 18 19:37:48 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=61bd2fdc
sci-mathematics/lean: bump to 3.42.0
Signed-off-by: Maciej Barć 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
b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af
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 ..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}" == ** ]]; 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/
commit: 3f0b44230b3002df360b247e3906e3c23d701f5a
Author: Maciej Barć gentoo org>
AuthorDate: Sat Mar 12 10:14:36 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Mar 12 10:15:11 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=3f0b4423
sci-mathematics/lean: drop old 3.38.0
Signed-off-by: Maciej Barć 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
b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af
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..
--- 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}" == ** ]]; 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/
commit: 7746d09bf48110a2fb6d76732811beb2565171d6
Author: Maciej Barć gentoo org>
AuthorDate: Sat Mar 12 09:59:38 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Mar 12 10:11:51 2022 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=7746d09b
sci-mathematics/lean: bump to 3.41.0
Signed-off-by: Maciej Barć 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
b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af
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 ..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}" == ** ]]; 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/
commit: 3d11f6436d29d336eed1d2917507135ba0759e6d
Author: Maciej Barć gentoo org>
AuthorDate: Tue Feb 22 17:43:06 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Feb 22 18:34:04 2022 +
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ć 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
b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af
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 ..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}" == ** ]]; 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/
commit: 024840070aea8eb50149f8f9d97df53a3f1fb940
Author: Maciej Barć gentoo org>
AuthorDate: Tue Feb 22 18:32:10 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Feb 22 18:34:04 2022 +
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ć 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..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..ebuild
b/sci-mathematics/lean/lean-3..ebuild
index a15591b790f5..5d8ee8eecd4b 100644
--- a/sci-mathematics/lean/lean-3..ebuild
+++ b/sci-mathematics/lean/lean-3..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
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/
commit: 6e3bf14e2fb5e305a6bd887e804499bb2521f380
Author: Maciej Barć gentoo org>
AuthorDate: Tue Feb 22 17:43:36 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Feb 22 18:34:04 2022 +
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ć 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
b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af
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..
--- 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}" == ** ]]; 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/
commit: 4db633aab7e4f7334eb29434098fd7a18f428b9e
Author: Maciej Barć gentoo org>
AuthorDate: Tue Feb 8 17:11:41 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Feb 8 17:21:23 2022 +
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ć 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
b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af
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..
--- 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}" == ** ]]; 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/
commit: 34df81ac434b83d7e7c4bfffb68959f67719a82c
Author: Maciej Barć gentoo org>
AuthorDate: Tue Feb 8 17:09:22 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Tue Feb 8 17:21:23 2022 +
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ć 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
b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af
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 ..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}" == ** ]]; 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/
commit: f45b887a09c256445f76e9764e27501424636a83
Author: Maciej Barć gentoo org>
AuthorDate: Sun Jan 30 19:21:08 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Sun Jan 30 19:21:28 2022 +
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ć 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 ..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}" == ** ]]; 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/
commit: 6e592397386181641bc0ca1cd8c40417a460e5cd
Author: Maciej Barć gentoo org>
AuthorDate: Sat Jan 8 03:01:49 2022 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Jan 8 03:02:06 2022 +
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ć 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 ..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}" == ** ]]; 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/
commit: 3c03d7044dd45cd23b5a4cb8bef5f0d9c0e121eb Author: Maciej Barć gentoo org> AuthorDate: Sat Dec 25 20:41:29 2021 + Commit: Maciej Barć gentoo org> CommitDate: Sat Dec 25 20:41:29 2021 + 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ć 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 @@ http://www.gentoo.org/dtd/metadata.dtd;> - -x...@gentoo.org -Maciej Barć + +sci-mathemat...@gentoo.org +Gentoo Mathematics Project - + The Lean theorem prover is a proof assistant developed principally by Leonardo de Moura at Microsoft Research.
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/
commit: 0539348664c95ea43e2156585ecedcc306ce7513
Author: Maciej Barć gentoo org>
AuthorDate: Sat Dec 4 02:29:23 2021 +
Commit: Maciej Barć gentoo org>
CommitDate: Sat Dec 4 02:36:10 2021 +
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ć gentoo.org>
sci-mathematics/lean/{lean-3.35.1-r1.ebuild => lean-3.35.1-r2.ebuild} | 2 +-
sci-mathematics/lean/lean-3..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..ebuild
b/sci-mathematics/lean/lean-3..ebuild
index cc208dc27850..a15591b790f5 100644
--- a/sci-mathematics/lean/lean-3..ebuild
+++ b/sci-mathematics/lean/lean-3..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/
commit: 0ceb76e690bd355afa6d84a9d2f2ebcaec422baa
Author: Maciej Barć gentoo org>
AuthorDate: Fri Nov 26 14:04:04 2021 +
Commit: Maciej Barć gentoo org>
CommitDate: Fri Nov 26 14:16:41 2021 +
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ć 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}" == ** ]]; 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
}
[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/
commit: 34386f101654e6e97603cd2b2ff7c9ab64e0dcfb
Author: Maciej Barć gentoo org>
AuthorDate: Fri Nov 26 14:16:04 2021 +
Commit: Maciej Barć gentoo org>
CommitDate: Fri Nov 26 14:16:42 2021 +
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ć gentoo.org>
sci-mathematics/lean/lean-3..ebuild | 75 +
1 file changed, 75 insertions(+)
diff --git a/sci-mathematics/lean/lean-3..ebuild
b/sci-mathematics/lean/lean-3..ebuild
new file mode 100644
index ..cc208dc27850
--- /dev/null
+++ b/sci-mathematics/lean/lean-3..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}" == ** ]]; 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/, sci-mathematics/lean/files/
commit: 7d5b1c7ba22597740387ad17314b58d88e941474
Author: Maciej Barć gentoo org>
AuthorDate: Fri Nov 26 12:06:35 2021 +
Commit: Maciej Barć gentoo org>
CommitDate: Fri Nov 26 13:08:07 2021 +
URL:https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=7d5b1c7b
sci-mathematics/lean: new package; add version 3.35.1
Package-Manager: Portage-3.0.28, Repoman-3.0.3
Signed-off-by: Maciej Barć gentoo.org>
sci-mathematics/lean/Manifest | 1 +
.../lean/files/lean-CMakeLists-fix_flags.patch | 23
sci-mathematics/lean/lean-3.35.1.ebuild| 68 ++
sci-mathematics/lean/metadata.xml | 20 +++
4 files changed, 112 insertions(+)
diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
new file mode 100644
index ..cad21881763c
--- /dev/null
+++ b/sci-mathematics/lean/Manifest
@@ -0,0 +1 @@
+DIST lean-3.35.1.tar.gz 1872461 BLAKE2B
44635b05a7e8ea89522dfb44b8f097ec530419ab79a5413648292ca34019ca744ae3e327cf3a7c627cb7a7a682cfcb2ffc5e6802f2c5ad67e0a7abc303624a3c
SHA512
24238cd9e920042f5bf7ba0a121da860e7e9c804d169c888bfabbc5e79e55f556a8920fab0c1a7e72b13501798c5f3fcb068f1705a0cf230f2b89abe1b3045ab
diff --git a/sci-mathematics/lean/files/lean-CMakeLists-fix_flags.patch
b/sci-mathematics/lean/files/lean-CMakeLists-fix_flags.patch
new file mode 100644
index ..1fd788fd79be
--- /dev/null
+++ b/sci-mathematics/lean/files/lean-CMakeLists-fix_flags.patch
@@ -0,0 +1,23 @@
+index f0efdf425..4cd461986 100644
+--- a/CMakeLists.txt
b/CMakeLists.txt
+@@ -194,7 +194,7 @@ set(CMAKE_CXX_FLAGS_DEBUG "-DLEAN_DEBUG
-DLEAN_TRACE")
+ set(CMAKE_CXX_FLAGS_MINSIZEREL "-DNDEBUG")
+ set(CMAKE_CXX_FLAGS_RELEASE"-DNDEBUG")
+ set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-DLEAN_DEBUG")
+-set(CMAKE_CXX_FLAGS_GPROF "-O2 -g -pg")
++set(CMAKE_CXX_FLAGS_GPROF "-g -pg")
+
+ # OSX .dmg generation (this is working in progress)
+ set(CPACK_DMG_BACKGROUND_IMAGE "${LEAN_SOURCE_DIR}/../images/lean.png")
+@@ -264,8 +264,8 @@ if (NOT MSVC)
+ set(CMAKE_CXX_FLAGS"-Wall -Wextra -std=c++11
${CMAKE_CXX_FLAGS}")
+ set(CMAKE_CXX_FLAGS_DEBUG "-g3 ${CMAKE_CXX_FLAGS_DEBUG}")
+ set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os ${CMAKE_CXX_FLAGS_MINSIZEREL}")
+-set(CMAKE_CXX_FLAGS_RELEASE"-O3 ${CMAKE_CXX_FLAGS_RELEASE}")
+-set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g3
${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
++set(CMAKE_CXX_FLAGS_RELEASE"${CMAKE_CXX_FLAGS_RELEASE}")
++set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-g3
${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
+ elseif (MULTI_THREAD)
+ set(CMAKE_CXX_FLAGS_DEBUG "/MTd ${CMAKE_CXX_FLAGS_DEBUG}")
+ set(CMAKE_CXX_FLAGS_MINSIZEREL "/MT ${CMAKE_CXX_FLAGS_MINSIZEREL}")
diff --git a/sci-mathematics/lean/lean-3.35.1.ebuild
b/sci-mathematics/lean/lean-3.35.1.ebuild
new file mode 100644
index ..71e0662ac80e
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.35.1.ebuild
@@ -0,0 +1,68 @@
+# Copyright 1999-2021 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+CMAKE_IN_SOURCE_BUILD="ON"
+
+inherit cmake optfeature
+
+DESCRIPTION="The Lean Theorem Prover"
+HOMEPAGE="https://leanprover-community.github.io/;
+
+if [[ "${PV}" == ** ]]; 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
+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
+}
+
+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
