[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/, sci-mathematics/lean/files/

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/, sci-mathematics/lean/files/

[Maciej Barć]

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>xgqt@gentoo.org</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>

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/lean/, sci-mathematics/lean/files/

[Maciej Barć]

commit:     93eca38ef76c1a9c568155659b891db542f22939
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Apr 18 13:52:42 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Apr 18 13:55:10 2023 +0000
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ć <xgqt <AT> 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.9999.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 000000000000..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 <cstdint>
+ #include <iostream>
+ #include <string>
+ #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.9999.ebuild b/sci-mathematics/lean/lean-3.9999.ebuild
index 307c5b95bc1b..72a23985077c 100644
--- a/sci-mathematics/lean/lean-3.9999.ebuild
+++ b/sci-mathematics/lean/lean-3.9999.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} == *9999* ]]; then
+if [[ ${PV} == *9999* ]] ; 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