diff --git a/CMakeLists.txt b/CMakeLists.txt index 2af38729071b..6aa7bf15479d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -52,7 +52,8 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten") # Use same platform flags as for Lean executables, in particular from `prepare-llvm-linux.sh`, # but not Lean-specific `LEAN_EXTRA_CXX_FLAGS` such as fsanitize. set(CADICAL_CXXFLAGS "${CMAKE_CXX_FLAGS}") - set(CADICAL_LDFLAGS "-Wl,-rpath=\\$$ORIGIN/../lib") + string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}/stage1" CADICAL_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}") + set(CADICAL_LDFLAGS "${CADICAL_INTERNAL_LINKER_FLAGS} -Wl,-rpath=\\$$ORIGIN/../lib") endif() find_program(CCACHE ccache) if(CCACHE) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 372be2b36bc0..b764dc260eaa 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1075,6 +1075,7 @@ string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERN string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}") toml_escape("${LEAN_EXTRA_OPTS}" LEAN_EXTRA_OPTS_TOML) +toml_escape("${LEANC_INTERNAL_FLAGS} ${LEANC_INTERNAL_LINKER_FLAGS}" LEAN_MORE_LEANC_ARGS_TOML) if(CMAKE_BUILD_TYPE MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel") set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}") diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in index c0faf4fa46d2..21e59a9e4a14 100644 --- a/src/lakefile.toml.in +++ b/src/lakefile.toml.in @@ -46,6 +46,8 @@ moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}] # Uncomment to limit number of reported errors further in case of overwhelming cmdline output #weakLeanArgs = ["-DmaxErrors=1"] +moreLeancArgs = [${LEAN_MORE_LEANC_ARGS_TOML}] + ${LEAN_EXTRA_LAKEFILE_TOML} [[lean_lib]] diff --git a/tests/bench_build.sh b/tests/bench_build.sh index c91fb109acd8..749cc9682ceb 100755 --- a/tests/bench_build.sh +++ b/tests/bench_build.sh @@ -1,10 +1,28 @@ -#!/usr/bin/env bash +#!/usr/bin/env nix +#! nix develop ..#oldGlibc --command /usr/bin/env bash # This script must be called from the repo root. # The radar environment variables must be provided. # See also the https://github.com/leanprover/radar readme. -cmake --preset release -DWFAIL=OFF +LLVM_RELEASE=19.1.2 +LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst" + +if [ ! -f "$LLVM_TARBALL" ]; then + mkdir -p "$RADAR_CACHE/llvm" + curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst" +fi + +mkdir -p build/release +cd build/release +eval cmake ../.. \ + --preset release $(../../script/prepare-llvm-linux.sh $LLVM_TARBALL) \ + -DWFAIL=OFF +rm -rf stage2 +cp -r stage1 stage2 +rm -rf stage3 +cp -r stage1 stage3 +cd ../.. make -C build/release -j"$(nproc)" bench-part1 mv tests/part1.measurements.jsonl "$RADAR_OUT" diff --git a/tests/bench_other.sh b/tests/bench_other.sh index 18d23d0019a2..98bae3ff685a 100755 --- a/tests/bench_other.sh +++ b/tests/bench_other.sh @@ -1,9 +1,27 @@ -#!/usr/bin/env bash +#!/usr/bin/env nix +#! nix develop ..#oldGlibc --command /usr/bin/env bash # This script must be called from the repo root. # The radar environment variables must be provided. # See also the https://github.com/leanprover/radar readme. -cmake --preset release -DWFAIL=OFF +LLVM_RELEASE=19.1.2 +LLVM_TARBALL="$RADAR_CACHE/llvm/$LLVM_RELEASE.tar.zst" + +if [ ! -f "$LLVM_TARBALL" ]; then + mkdir -p "$RADAR_CACHE/llvm" + curl --location -o "$LLVM_TARBALL" "https://github.com/leanprover/lean-llvm/releases/download/$LLVM_RELEASE/lean-llvm-x86_64-linux-gnu.tar.zst" +fi + +mkdir -p build/release +cd build/release +eval cmake ../.. \ + --preset release $(../../script/prepare-llvm-linux.sh $LLVM_TARBALL) \ + -DWFAIL=OFF +rm -rf stage2 +cp -r stage1 stage2 +rm -rf stage3 +cp -r stage1 stage3 +cd ../.. make -C build/release -j"$(nproc)" bench-part2 mv tests/part2.measurements.jsonl "$RADAR_OUT"