From cfc49e8b4f716904f89b273e92c57abf0f1a3bd4 Mon Sep 17 00:00:00 2001 From: Stephan Bauroth Date: Thu, 9 Apr 2026 13:01:56 +0200 Subject: [PATCH 1/3] lean: allow older CMake versions to configure --- build-bench-env.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build-bench-env.sh b/build-bench-env.sh index 26e8c42..49c96ca 100755 --- a/build-bench-env.sh +++ b/build-bench-env.sh @@ -793,7 +793,7 @@ if test "$setup_lean" = "1"; then checkout lean $version_lean https://github.com/leanprover-community/lean mkdir -p out/release cd out/release - env CC=gcc CXX="g++" cmake ../../src -DCUSTOM_ALLOCATORS=OFF -DLEAN_EXTRA_CXX_FLAGS="-w" + env CC=gcc CXX="g++" cmake ../../src -DCUSTOM_ALLOCATORS=OFF -DLEAN_EXTRA_CXX_FLAGS="-w" -DCMAKE_POLICY_VERSION_MINIMUM=3.5 echo "make -j$procs" make -j $procs rm -rf ./tests/ # we don't need tests From 8eb43eaa5ea8330d68b3ce39ddee8e7ab69cba1e Mon Sep 17 00:00:00 2001 From: Stephan Bauroth Date: Thu, 9 Apr 2026 13:38:41 +0200 Subject: [PATCH 2/3] lean: apply patch to let lean compile the deleted operator seems to be unused across the codebase --- build-bench-env.sh | 3 +++ patches/lean.patch | 31 +++++++++++++++++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 patches/lean.patch diff --git a/build-bench-env.sh b/build-bench-env.sh index 49c96ca..5cd32b2 100755 --- a/build-bench-env.sh +++ b/build-bench-env.sh @@ -791,6 +791,9 @@ fi if test "$setup_lean" = "1"; then phase "build lean $version_lean" checkout lean $version_lean https://github.com/leanprover-community/lean + set +e + patch -p1 -N -r- < ../../patches/lean.patch + set -e mkdir -p out/release cd out/release env CC=gcc CXX="g++" cmake ../../src -DCUSTOM_ALLOCATORS=OFF -DLEAN_EXTRA_CXX_FLAGS="-w" -DCMAKE_POLICY_VERSION_MINIMUM=3.5 diff --git a/patches/lean.patch b/patches/lean.patch new file mode 100644 index 0000000..93a5e32 --- /dev/null +++ b/patches/lean.patch @@ -0,0 +1,31 @@ +diff --git a/src/library/parray.h b/src/library/parray.h +index e84ac3bf7..8f2cffeb3 100644 +--- a/src/library/parray.h ++++ b/src/library/parray.h +@@ -586,14 +586,6 @@ public: + return *this; + } + +- parray & operator=(parray && s) { +- if (m_cell) +- dec_ref(m_cell); +- m_cell = s.m_ptr; +- s.m_ptr = nullptr; +- return *this; +- } +- + size_t size() const { + return size(m_cell); + } +diff --git a/src/util/hash.cpp b/src/util/hash.cpp +index b4529df92..f58d3c618 100644 +--- a/src/util/hash.cpp ++++ b/src/util/hash.cpp +@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. + Author: Leonardo de Moura + */ + #include "util/hash.h" ++#include + #include + + namespace lean { From 32d9c6f8a3a635a1fa7964180551b0ac526e89f1 Mon Sep 17 00:00:00 2001 From: Stephan Bauroth Date: Thu, 9 Apr 2026 13:40:37 +0200 Subject: [PATCH 3/3] CI: reactivate fedora, lean should build there, now --- .github/workflows/all.yml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/.github/workflows/all.yml b/.github/workflows/all.yml index 930eee1..099f375 100644 --- a/.github/workflows/all.yml +++ b/.github/workflows/all.yml @@ -17,11 +17,8 @@ jobs: strategy: matrix: platform: [ubuntu, alpine, fedora] - exclude: - # Fedora is not currently building lean. - - platform: fedora fail-fast: false uses: ./.github/workflows/platform.yml name: ${{ matrix.platform }} with: - platform: ${{ matrix.platform }} \ No newline at end of file + platform: ${{ matrix.platform }}