commit: 7d5b1c7ba22597740387ad17314b58d88e941474
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Fri Nov 26 12:06:35 2021 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Fri Nov 26 13:08:07 2021 +0000
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ć <xgqt <AT> 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 000000000000..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 000000000000..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 000000000000..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}" == *9999* ]]; then
+ MAJOR=3 # sync this periodically for the live version
+ inherit git-r3
+ EGIT_REPO_URI="https://github.com/leanprover-community/lean.git";
+else
+ MAJOR=$(ver_cut 1)
+
SRC_URI="https://github.com/leanprover-community/lean/archive/refs/tags/v${PV}.tar.gz
-> ${P}.tar.gz"
+ KEYWORDS="~amd64 ~x86"
+fi
+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 compile mathlib (which will take some time)"
+ elog " $ leanpkg install
https://github.com/leanprover-community/mathlib";
+}
diff --git a/sci-mathematics/lean/metadata.xml
b/sci-mathematics/lean/metadata.xml
new file mode 100644
index 000000000000..278e5b1a42a2
--- /dev/null
+++ b/sci-mathematics/lean/metadata.xml
@@ -0,0 +1,20 @@
+<?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>
