Fix lean build

.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 }}
+      platform: ${{ matrix.platform }}

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

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 <cstdint>
+ #include <string>
+
+ namespace lean {