diff --git a/.github/workflows/all.yml b/.github/workflows/all.yml index 930eee13..099f3756 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 }} diff --git a/build-bench-env.sh b/build-bench-env.sh index 26e8c421..5cd32b25 100755 --- a/build-bench-env.sh +++ b/build-bench-env.sh @@ -791,9 +791,12 @@ 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" + 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 diff --git a/patches/lean.patch b/patches/lean.patch new file mode 100644 index 00000000..93a5e327 --- /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 {