dev-lang: move lean to ::gentoo (as sci-mathematics/lean)

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

6 files changed, 0 insertions, 256 deletions

diff --git a/dev-lang/lean/Manifest b/dev-lang/lean/Manifest
deleted file mode 100644
index c9c3a7261..000000000
--- a/dev-lang/lean/Manifest
+++ /dev/null
@@ -1,3 +0,0 @@
-DIST lean-3.33.0.tar.gz 1890511 BLAKE2B 93fed81409a5d2fc31fd0963e00262ffbf7ce177954501e01d988666bf55bd4e0243488139f34eb4322055a5512565c6770749f793a8b7a8c7eb6e3045c5c2e7 SHA512 813f21f57913c15ca52b3a40bb0493d156b714ea26c5dcf4d159ee7aedf05dd6259ff57c05aa278bc72a3bfb9a531835387fc8cfbaca7d8341e0f2fbe9535bf3
-DIST lean-3.34.0.tar.gz 1891710 BLAKE2B 53c25b93c2e720187bfa5980a6bf3c9790aebb757b732704f6f5ad250b333c192417a938bc1cd6274a45f5b5f49f8e275da1f5c5597ffd7bc2da7bbe8b0371f7 SHA512 bc3f81ffbfa3291675d3c09c28c3eacccc2d44d021fb7e9923c7116091046b57f388589074e984f257842757c77972ef3b354d8690cccbebf6d3e2aae1f811a5
-DIST lean-3.35.0.tar.gz 1872221 BLAKE2B 8cdcaa65eb49ad6ed8b6961912d162a5832d45d5f8855ea62334010a1af647cd2aa4906d83317ee16c95cdb44522c1f7cb8f62ece6abda12354e18534e560e6e SHA512 b48a8134bdc39dc098a49303549ed4b96a2ca9e69043b9dca12c4789f60462b94374a184aee6fa33abd5a8f1acce9553b8144e935e539833c853e2384c41c2e7
diff --git a/dev-lang/lean/files/fix_flags.patch b/dev-lang/lean/files/fix_flags.patch
deleted file mode 100644
index 1fd788fd7..000000000
--- a/dev-lang/lean/files/fix_flags.patch
+++ /dev/null
@@ -1,23 +0,0 @@
-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/dev-lang/lean/lean-3.33.0.ebuild b/dev-lang/lean/lean-3.33.0.ebuild
deleted file mode 100644
index 3ab4b15f4..000000000
--- a/dev-lang/lean/lean-3.33.0.ebuild
+++ /dev/null
@@ -1,70 +0,0 @@
-# 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}" == *9999* ]]; then
-	MAJOR=3  # sync this periodically for the live version
-	inherit git-r3
-	EGIT_REPO_URI="https://github.com/leanprover-community/lean.git"
-else
-	MAJOR=$(ver_cut 1)
-	SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz"
-	KEYWORDS="~amd64"
-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}/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 python test dependency
-		--exclude-regex style_check
-	)
-	cmake_src_test
-}
-
-pkg_postinst() {
-	elog "You probably want to use lean with mathlib, to install it 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 long time)"
-	elog "   $ leanpkg install https://github.com/leanprover-community/mathlib"
-
-	optfeature "project management with leanproject" sci-mathematics/mathlib-tools
-}
diff --git a/dev-lang/lean/lean-3.34.0.ebuild b/dev-lang/lean/lean-3.34.0.ebuild
deleted file mode 100644
index 3ab4b15f4..000000000
--- a/dev-lang/lean/lean-3.34.0.ebuild
+++ /dev/null
@@ -1,70 +0,0 @@
-# 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}" == *9999* ]]; then
-	MAJOR=3  # sync this periodically for the live version
-	inherit git-r3
-	EGIT_REPO_URI="https://github.com/leanprover-community/lean.git"
-else
-	MAJOR=$(ver_cut 1)
-	SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz"
-	KEYWORDS="~amd64"
-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}/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 python test dependency
-		--exclude-regex style_check
-	)
-	cmake_src_test
-}
-
-pkg_postinst() {
-	elog "You probably want to use lean with mathlib, to install it 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 long time)"
-	elog "   $ leanpkg install https://github.com/leanprover-community/mathlib"
-
-	optfeature "project management with leanproject" sci-mathematics/mathlib-tools
-}
diff --git a/dev-lang/lean/lean-3.35.0.ebuild b/dev-lang/lean/lean-3.35.0.ebuild
deleted file mode 100644
index 3ab4b15f4..000000000
--- a/dev-lang/lean/lean-3.35.0.ebuild
+++ /dev/null
@@ -1,70 +0,0 @@
-# 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}" == *9999* ]]; then
-	MAJOR=3  # sync this periodically for the live version
-	inherit git-r3
-	EGIT_REPO_URI="https://github.com/leanprover-community/lean.git"
-else
-	MAJOR=$(ver_cut 1)
-	SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz -> ${P}.tar.gz"
-	KEYWORDS="~amd64"
-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}/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 python test dependency
-		--exclude-regex style_check
-	)
-	cmake_src_test
-}
-
-pkg_postinst() {
-	elog "You probably want to use lean with mathlib, to install it 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 long time)"
-	elog "   $ leanpkg install https://github.com/leanprover-community/mathlib"
-
-	optfeature "project management with leanproject" sci-mathematics/mathlib-tools
-}
diff --git a/dev-lang/lean/metadata.xml b/dev-lang/lean/metadata.xml
deleted file mode 100644
index 9e03d53ad..000000000
--- a/dev-lang/lean/metadata.xml
+++ /dev/null
@@ -1,20 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
-
-<pkgmetadata>
-  <maintainer type="person">
-    <email>xgqt@riseup.net</email>
-    <name>Maciej Barć</name>
-  </maintainer>
-  <longdescription lang="en">
-    The Lean theorem prover is a proof assistant developed principally
-    by Leonardo de Moura at Microsoft Research.
-  </longdescription>
-  <upstream>
-    <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>