summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaciej Barć <xgqt@gentoo.org>2023-04-18 15:52:42 +0200
committerMaciej Barć <xgqt@gentoo.org>2023-04-18 15:55:10 +0200
commit93eca38ef76c1a9c568155659b891db542f22939 (patch)
tree8029093b78ae620675043b610394fea8bc3243df
parentsci-mathematics/lean: drop old 3.50.2 (diff)
downloadgentoo-93eca38ef76c1a9c568155659b891db542f22939.tar.gz
gentoo-93eca38ef76c1a9c568155659b891db542f22939.tar.bz2
gentoo-93eca38ef76c1a9c568155659b891db542f22939.zip
sci-mathematics/lean: fix build with GCC 13
Closes: https://bugs.gentoo.org/895202 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
-rw-r--r--sci-mathematics/lean/files/lean-3.50.3-gcc-13.patch10
-rw-r--r--sci-mathematics/lean/lean-3.50.3.ebuild11
-rw-r--r--sci-mathematics/lean/lean-3.9999.ebuild13
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