Skip to content

Commit 121ac93

Browse files
committed
Alternative fix for lean mathlib.
1 parent 0be2c4f commit 121ac93

1 file changed

Lines changed: 3 additions & 2 deletions

File tree

build-bench-env.sh

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,7 @@ readonly version_yal=main
6868
# benchmark versions
6969
readonly version_redis=6.2.7
7070
readonly version_lean=21d264a66d53b0a910178ae7d9529cb5886a39b6 # build fix for recent compilers
71+
readonly version_mathlib=release_812
7172
readonly version_rocksdb=8.1.1
7273
readonly version_lua=v5.4.7
7374
readonly version_linux=6.5.1
@@ -787,8 +788,8 @@ if test "$setup_lean" = "1"; then
787788
echo "make -j$procs"
788789
make -j $procs
789790
rm -rf ./tests/ # we don't need tests
790-
mkdir -p "$devdir/mathlib"
791-
cp -u "$devdir/lean/leanpkg/leanpkg.toml" "$devdir/mathlib"
791+
popd
792+
checkout mathlib $version_mathlib https://github.com/leanprover-community/mathlib3
792793
popd
793794
fi
794795

0 commit comments

Comments
 (0)