summaryrefslogtreecommitdiff
path: root/sci-mathematics/lean
diff options
context:
space:
mode:
authorV3n3RiX <venerix@koprulu.sector>2022-03-20 00:40:44 +0000
committerV3n3RiX <venerix@koprulu.sector>2022-03-20 00:40:44 +0000
commit4cbcc855382a06088e2f016f62cafdbcb7e40665 (patch)
tree356496503d52354aa6d9f2d36126302fed5f3a73 /sci-mathematics/lean
parentfcc5224904648a8e6eb528d7603154160a20022f (diff)
gentoo resync : 20.03.2022
Diffstat (limited to 'sci-mathematics/lean')
-rw-r--r--sci-mathematics/lean/Manifest18
-rw-r--r--sci-mathematics/lean/lean-3.39.1.ebuild (renamed from sci-mathematics/lean/lean-3.37.0.ebuild)6
-rw-r--r--sci-mathematics/lean/lean-3.40.0.ebuild (renamed from sci-mathematics/lean/lean-3.38.0.ebuild)6
-rw-r--r--sci-mathematics/lean/lean-3.41.0.ebuild (renamed from sci-mathematics/lean/lean-3.35.1-r2.ebuild)8
-rw-r--r--sci-mathematics/lean/lean-3.42.0.ebuild75
-rw-r--r--sci-mathematics/lean/lean-3.9999.ebuild8
-rw-r--r--sci-mathematics/lean/metadata.xml3
7 files changed, 99 insertions, 25 deletions
diff --git a/sci-mathematics/lean/Manifest b/sci-mathematics/lean/Manifest
index c22074c5a4c7..18b25a5655e3 100644
--- a/sci-mathematics/lean/Manifest
+++ b/sci-mathematics/lean/Manifest
@@ -1,9 +1,11 @@
AUX lean-CMakeLists-fix_flags.patch 1285 BLAKE2B 0507e553c1acf2a53c5267932127117d5ae5ba9015a08c88748b3d82c041f8d904d15cd033dd7934ac55c474fa75a5d4a46f680cc887fee37c05c3f5f3832839 SHA512 11a5918847e45aac7bf79e48d8f881ef5cd3e6b09dbb0979f3f0b88fd36458be21ebeb530158da801399a0cdc8fe382444ff338cd793cd9f1bfced90c5d5a71b
-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
-EBUILD lean-3.35.1-r2.ebuild 1773 BLAKE2B 15392079ec1e4d9eec5dfd9ee13fee05eca98fb2d7fe204a05b793b06588848c339dbb3b01c8c84f30fc45acc2ce8bb74be5841b9aa216a3d5f2d42d3158b7a6 SHA512 89f983bdb770e0fdbbcbd4db2a1bc8de25df33050ed936748788695e4926588471e8963289ef5bd397748abc41aae656f5614f3317b05b70f54dcd43189464d1
-EBUILD lean-3.37.0.ebuild 1773 BLAKE2B 6a332c70ff4fe6731391d180909c732976385466dc28add08014be98e84dd0c7a36a56349516099f6b16966bf70e03d3bf1b19633d9e54c054d2adbb4b9d12e8 SHA512 7601871b46ee585037c8c7600ebf3f4166004314cae3062b3a70838920f0199f5ba4570daa8f1b051a1aa7390e9a9986a0e553088e0a39b1ac45e884bc1ed18a
-EBUILD lean-3.38.0.ebuild 1773 BLAKE2B 6a332c70ff4fe6731391d180909c732976385466dc28add08014be98e84dd0c7a36a56349516099f6b16966bf70e03d3bf1b19633d9e54c054d2adbb4b9d12e8 SHA512 7601871b46ee585037c8c7600ebf3f4166004314cae3062b3a70838920f0199f5ba4570daa8f1b051a1aa7390e9a9986a0e553088e0a39b1ac45e884bc1ed18a
-EBUILD lean-3.9999.ebuild 1773 BLAKE2B 15392079ec1e4d9eec5dfd9ee13fee05eca98fb2d7fe204a05b793b06588848c339dbb3b01c8c84f30fc45acc2ce8bb74be5841b9aa216a3d5f2d42d3158b7a6 SHA512 89f983bdb770e0fdbbcbd4db2a1bc8de25df33050ed936748788695e4926588471e8963289ef5bd397748abc41aae656f5614f3317b05b70f54dcd43189464d1
-MISC metadata.xml 673 BLAKE2B a0450429934f5c161e73df65461ef4142663b704766424aa13abd06a83bf27744a1505d06b615bde4fa0b4fe65500d7d4ac904753a107bf830722af92a3ab1ef SHA512 bad144f7071ec66f4eb0b167c83c3a32614d6d57a03cab3d981a42d174a853a118f3f9a938c41de21db9933b0bdf2290f52c33795be9df12c195572ab1b4d8b9
+DIST lean-3.39.1.tar.gz 1878481 BLAKE2B b3d1760594751418d6ebb7754d733e8fdebc5e0eba25e8d4993280325ec9d40e9083af155d388d52b5edfff2e9dffbeff91caa68ccb76500dcd88ebac2af4444 SHA512 5839eb7b5f7cd2d93ab603f1a5121e0a6b55850686677f103c16ec2157dc19479f1909ea056b54e41331c28fd59a4a825741384fa431473924381b72640a04dd
+DIST lean-3.40.0.tar.gz 1878547 BLAKE2B 762c12b9fee9ac405730fb4a748326e7c9603c50f44512166f94df51e8cde0096803f11d0201980e1a1c0121a2b278075bf238452254d83e2d8b7b5566355416 SHA512 4daa32b60195a9776019c3c13c3765a1f5a817d78f189c3f92859298118815af4cb47359816ebbb977f35453be358956f3680b06b5930d5cf3a4245599602873
+DIST lean-3.41.0.tar.gz 1905966 BLAKE2B 1921ba4a975ed8fc6001695151bb366341e0895989a570bb7fbef1e719685945d0b7c51ed0716ff29daaf81af24ce2e289cab41b251c686a286cd94a0cf708f8 SHA512 855a56812ba5dc7cf431490957570d0fcbc4760faa1602095e708ddcc4e5a3c6aeac42133c210375d4538d97c8ae90df3ab3c7e7840e8896b8d0db439e925fbf
+DIST lean-3.42.0.tar.gz 1908134 BLAKE2B 7b6403786cc1a3a2b974f8df4c2bf2921e4e374ead4290a0e263c8464a9c009fd2f62e7cf5bdbc5087d0c9bb4c57f798b9d1a4b8ee2d66152714ec2af649e196 SHA512 2f1fc1bf3aff7fa806e1cd4647380d6896d98a9191f2035d5a37cc35938de42b243188984aa2fced37bdbee3b2c3c6ef25d27bf2428bf9a0307cc3237c80560f
+EBUILD lean-3.39.1.ebuild 1760 BLAKE2B 21543910ba7f9eee7186e4db4ba439ce4e23cf72e49c936beb47fd0717cbcb276c41b03a651efc46a9855d1d9f2b0bd9904e34f52b3c6569eff0f757c6719c6a SHA512 bfb7062d09fff733cb5779b0f1f49c1ec7b1d90e48f12b2c524dc4c5189439e2de2773ac25f3621359a39cae5c2c6d338d2e6f0a1c892ebf1f5e4ad742ce9f2c
+EBUILD lean-3.40.0.ebuild 1760 BLAKE2B 21543910ba7f9eee7186e4db4ba439ce4e23cf72e49c936beb47fd0717cbcb276c41b03a651efc46a9855d1d9f2b0bd9904e34f52b3c6569eff0f757c6719c6a SHA512 bfb7062d09fff733cb5779b0f1f49c1ec7b1d90e48f12b2c524dc4c5189439e2de2773ac25f3621359a39cae5c2c6d338d2e6f0a1c892ebf1f5e4ad742ce9f2c
+EBUILD lean-3.41.0.ebuild 1760 BLAKE2B 21543910ba7f9eee7186e4db4ba439ce4e23cf72e49c936beb47fd0717cbcb276c41b03a651efc46a9855d1d9f2b0bd9904e34f52b3c6569eff0f757c6719c6a SHA512 bfb7062d09fff733cb5779b0f1f49c1ec7b1d90e48f12b2c524dc4c5189439e2de2773ac25f3621359a39cae5c2c6d338d2e6f0a1c892ebf1f5e4ad742ce9f2c
+EBUILD lean-3.42.0.ebuild 1760 BLAKE2B 21543910ba7f9eee7186e4db4ba439ce4e23cf72e49c936beb47fd0717cbcb276c41b03a651efc46a9855d1d9f2b0bd9904e34f52b3c6569eff0f757c6719c6a SHA512 bfb7062d09fff733cb5779b0f1f49c1ec7b1d90e48f12b2c524dc4c5189439e2de2773ac25f3621359a39cae5c2c6d338d2e6f0a1c892ebf1f5e4ad742ce9f2c
+EBUILD lean-3.9999.ebuild 1760 BLAKE2B 21543910ba7f9eee7186e4db4ba439ce4e23cf72e49c936beb47fd0717cbcb276c41b03a651efc46a9855d1d9f2b0bd9904e34f52b3c6569eff0f757c6719c6a SHA512 bfb7062d09fff733cb5779b0f1f49c1ec7b1d90e48f12b2c524dc4c5189439e2de2773ac25f3621359a39cae5c2c6d338d2e6f0a1c892ebf1f5e4ad742ce9f2c
+MISC metadata.xml 606 BLAKE2B 6478d84a762a59082fdea0a11a95b27c093782228c48dba58dc490ea9ac2cecef54cc3101dc98e385f3a29f85d84af21b7d2ae1a9f089ee0313158ecb44eb0e7 SHA512 02d2ac07b155c7a04c857d397d476a39864d02b10dd81c5830db5e21eb86c6dcff26da552a04717f5f587b326ddf8e2e8d27f1a138f88b391f0199d8004d8cb7
diff --git a/sci-mathematics/lean/lean-3.37.0.ebuild b/sci-mathematics/lean/lean-3.39.1.ebuild
index e47a48054580..5d8ee8eecd4b 100644
--- a/sci-mathematics/lean/lean-3.37.0.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.38.0.ebuild b/sci-mathematics/lean/lean-3.40.0.ebuild
index e47a48054580..5d8ee8eecd4b 100644
--- a/sci-mathematics/lean/lean-3.38.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.35.1-r2.ebuild b/sci-mathematics/lean/lean-3.41.0.ebuild
index a15591b790f5..5d8ee8eecd4b 100644
--- a/sci-mathematics/lean/lean-3.35.1-r2.ebuild
+++ b/sci-mathematics/lean/lean-3.41.0.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
@@ -6,7 +6,7 @@ EAPI=8
MAJOR=$(ver_cut 1)
CMAKE_IN_SOURCE_BUILD="ON"
-inherit cmake optfeature readme.gentoo-r1
+inherit cmake readme.gentoo-r1
DESCRIPTION="The Lean Theorem Prover"
HOMEPAGE="https://leanprover-community.github.io/"
@@ -22,7 +22,7 @@ S="${WORKDIR}/lean-${PV}/src"
LICENSE="Apache-2.0"
SLOT="0/${MAJOR}"
-IUSE="debug +json +threads"
+IUSE="debug +threads"
RDEPEND="dev-libs/gmp:="
DEPEND="${RDEPEND}"
@@ -40,7 +40,7 @@ src_configure() {
local mycmakeargs=(
-DALPHA=ON
-DAUTO_THREAD_FINALIZATION=ON
- -DJSON=$(usex json)
+ -DJSON=ON # bug 833900
-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
-DMULTI_THREAD=$(usex threads)
-DUSE_GITHASH=OFF
diff --git a/sci-mathematics/lean/lean-3.42.0.ebuild b/sci-mathematics/lean/lean-3.42.0.ebuild
new file mode 100644
index 000000000000..5d8ee8eecd4b
--- /dev/null
+++ b/sci-mathematics/lean/lean-3.42.0.ebuild
@@ -0,0 +1,75 @@
+# Copyright 1999-2022 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+MAJOR=$(ver_cut 1)
+CMAKE_IN_SOURCE_BUILD="ON"
+
+inherit cmake readme.gentoo-r1
+
+DESCRIPTION="The Lean Theorem Prover"
+HOMEPAGE="https://leanprover-community.github.io/"
+
+if [[ "${PV}" == *9999* ]]; then
+ inherit git-r3
+ EGIT_REPO_URI="https://github.com/leanprover-community/lean.git"
+else
+ SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz"
+ KEYWORDS="~amd64 ~x86"
+fi
+S="${WORKDIR}/lean-${PV}/src"
+
+LICENSE="Apache-2.0"
+SLOT="0/${MAJOR}"
+IUSE="debug +threads"
+
+RDEPEND="dev-libs/gmp:="
+DEPEND="${RDEPEND}"
+
+PATCHES=( "${FILESDIR}/${PN}-CMakeLists-fix_flags.patch" )
+
+src_configure() {
+ local CMAKE_BUILD_TYPE
+ if use debug; then
+ CMAKE_BUILD_TYPE="Debug"
+ else
+ CMAKE_BUILD_TYPE="Release"
+ fi
+
+ local mycmakeargs=(
+ -DALPHA=ON
+ -DAUTO_THREAD_FINALIZATION=ON
+ -DJSON=ON # bug 833900
+ -DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
+ -DMULTI_THREAD=$(usex threads)
+ -DUSE_GITHASH=OFF
+ )
+ cmake_src_configure
+}
+
+src_test() {
+ local myctestargs=(
+ # Disable problematic "style_check" cpplint test,
+ # this also removes the python test dependency
+ --exclude-regex style_check
+ )
+ cmake_src_test
+}
+
+src_install() {
+ cmake_src_install
+
+ local DISABLE_AUTOFORMATTING="yes"
+ local DOC_CONTENTS="You probably want to use lean with mathlib, you can either:
+ - Do not install mathlib globally and use local versions
+ - Use leanproject from sci-mathematics/mathlib-tools
+ $ leanproject global-install
+ - Use leanpkg and compile mathlib (which will take some time)
+ $ leanpkg install https://github.com/leanprover-community/mathlib"
+ readme.gentoo_create_doc
+}
+
+pkg_postinst() {
+ readme.gentoo_print_elog
+}
diff --git a/sci-mathematics/lean/lean-3.9999.ebuild b/sci-mathematics/lean/lean-3.9999.ebuild
index a15591b790f5..5d8ee8eecd4b 100644
--- a/sci-mathematics/lean/lean-3.9999.ebuild
+++ b/sci-mathematics/lean/lean-3.9999.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2021 Gentoo Authors
+# Copyright 1999-2022 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
@@ -6,7 +6,7 @@ EAPI=8
MAJOR=$(ver_cut 1)
CMAKE_IN_SOURCE_BUILD="ON"
-inherit cmake optfeature readme.gentoo-r1
+inherit cmake readme.gentoo-r1
DESCRIPTION="The Lean Theorem Prover"
HOMEPAGE="https://leanprover-community.github.io/"
@@ -22,7 +22,7 @@ S="${WORKDIR}/lean-${PV}/src"
LICENSE="Apache-2.0"
SLOT="0/${MAJOR}"
-IUSE="debug +json +threads"
+IUSE="debug +threads"
RDEPEND="dev-libs/gmp:="
DEPEND="${RDEPEND}"
@@ -40,7 +40,7 @@ src_configure() {
local mycmakeargs=(
-DALPHA=ON
-DAUTO_THREAD_FINALIZATION=ON
- -DJSON=$(usex json)
+ -DJSON=ON # bug 833900
-DLEAN_EXTRA_CXX_FLAGS="${CXXFLAGS}"
-DMULTI_THREAD=$(usex threads)
-DUSE_GITHASH=OFF
diff --git a/sci-mathematics/lean/metadata.xml b/sci-mathematics/lean/metadata.xml
index f06c80c2d7be..ddb0be8a571c 100644
--- a/sci-mathematics/lean/metadata.xml
+++ b/sci-mathematics/lean/metadata.xml
@@ -14,7 +14,4 @@
<bugs-to>https://github.com/leanprover-community/lean/issues</bugs-to>
<remote-id type="github">leanprover-community/lean</remote-id>
</upstream>
- <use>
- <flag name="json"> Enable JSON support</flag>
- </use>
</pkgmetadata>
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-06 10:03:55 +0000