commit: 0687ff75b4800c03e0b715538105576eb41422cf
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Fri Nov 26 11:50:35 2021 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Fri Nov 26 13:08:39 2021 +0000
URL: https://gitweb.gentoo.org/repo/proj/guru.git/commit/?id=0687ff75
dev-lang: move lean to ::gentoo (as sci-mathematics/lean)
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
dev-lang/lean/Manifest | 3 --
dev-lang/lean/files/fix_flags.patch | 23 ------------
dev-lang/lean/lean-3.33.0.ebuild | 70 -------------------------------------
dev-lang/lean/lean-3.34.0.ebuild | 70 -------------------------------------
dev-lang/lean/lean-3.35.0.ebuild | 70 -------------------------------------
dev-lang/lean/metadata.xml | 20 -----------
6 files changed, 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>[email protected]</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>
