chore: benchmark using USE_LAKE (#9361)

.github/workflows/build-template.yml

@@ -226,8 +226,9 @@ jobs:
         if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |
-          # clean rebuild in case of Makefile changes
-          make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC
+          # clean rebuild in case of Makefile changes/Lake does not detect uncommited stage 0
+          # changes yet
+          make -C build update-stage0 && make -C build/stage1 clean-stdlib && make -C build -j$NPROC
         if: matrix.check-rebootstrap
       - name: CCache stats
         if: always()

script/bench.sh

@@ -1,9 +1,16 @@
 #!/usr/bin/env bash
 set -euo pipefail
 
+cmake --preset release -DUSE_LAKE=ON 1>&2
+
 # We benchmark against stage 2 to test new optimizations.
-timeout -s KILL 1h time bash -c 'mkdir -p build/release; cd build/release; cmake ../.. && make -j$(nproc) stage2' 1>&2
+timeout -s KILL 1h time make -C build/release -j$(nproc) stage2 1>&2
 export PATH=$PWD/build/release/stage2/bin:$PATH
+
+# The extra opts used to be passed to the Makefile during benchmarking only but with Lake it is
+# easier to configure them statically.
+cmake -B build/release/stage2 -S src -DLEAN_EXTRA_LAKEFILE_TOML='weakLeanArgs=["-Dprofiler=true", "-Dprofiler.threshold=9999999", "--stats"]' 1>&2
+
 cd tests/bench
 timeout -s KILL 1h time temci exec --config speedcenter.yaml --in speedcenter.exec.velcom.yaml 1>&2
 temci report run_output.yaml --reporter codespeed2

src/CMakeLists.txt

@@ -533,12 +533,21 @@ else()
         OUTPUT_VARIABLE GIT_SHA1
         OUTPUT_STRIP_TRAILING_WHITESPACE)
     message(STATUS "stage0 sha1: ${GIT_SHA1}")
+    # Now that we've prepared the information for the next stage, we can forget that we will use
+    # Lake in the future as we won't use it in this stage
+    set(USE_LAKE OFF)
   else()
     set(GIT_SHA1 "")
   endif()
 endif()
 configure_file("${LEAN_SOURCE_DIR}/githash.h.in" "${LEAN_BINARY_DIR}/githash.h")
 
+if(USE_LAKE AND ${STAGE} EQUAL 0)
+  # Now that we've prepared the information for the next stage, we can forget that we will use
+  # Lake in the future as we won't use it in this stage
+  set(USE_LAKE OFF)
+endif()
+
 # Windows uses ";" as a path separator. We use `LEAN_PATH_SEPARATOR` on scripts such as lean.mk.in
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   set(LEAN_PATH_SEPARATOR ";")
@@ -838,6 +847,10 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   set(LAKE_LIB_PREFIX "lib")
 endif()
 
-if(USE_LAKE AND STAGE EQUAL 1)
-  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
+if(USE_LAKE)
+  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${CMAKE_BINARY_DIR}/lakefile.toml)
+  # copy for editing
+  if(STAGE EQUAL 1)
+    configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
+  endif()
 endif()

src/lakefile.toml.in

@@ -31,6 +31,8 @@ leanOptions = { experimental.module = true }
 # For example, CI will set `-DwarningAsError=true` through this
 moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}]
 
+${LEAN_EXTRA_LAKEFILE_TOML}
+
 [[lean_lib]]
 name = "Init"
 libName = "${LAKE_LIB_PREFIX}Init"

src/stdlib.make.in

@@ -6,7 +6,7 @@ SHELL := $(LEAN_BASH) -eo pipefail
 
 # any absolute path to the stdlib breaks the Makefile
 export LEAN_PATH=
-ifeq "${USE_LAKE} ${STAGE}" "ON 1"
+ifeq "${USE_LAKE}" "ON"
   export LEAN_CC=${CMAKE_C_COMPILER}
 else
   export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER}
@@ -36,12 +36,11 @@ endif
 # These can be phony since the inner Makefile/Lake will have the correct dependencies and avoid rebuilds
 .PHONY: Init Std Lean leanshared Lake libLake_shared lake lean
 
-# As the build directory is part of the lakefile.toml, only use it for stage 1 for now
-ifeq "${USE_LAKE} ${STAGE}" "ON 1"
+ifeq "${USE_LAKE}" "ON"
 
 # build in parallel
 Init:
-	${PREV_STAGE}/bin/lake build $(LAKE_EXTRA_ARGS)
+	${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml $(LAKE_EXTRA_ARGS)
 
 Std Lean Lake Leanc: Init
 

tests/bench/speedcenter.exec.velcom.yaml

@@ -18,7 +18,9 @@
   run_config:
     <<: *time
     cmd: |
-      bash -c 'set -eo pipefail; touch ../../src/Init/Prelude.lean; make LEAN_OPTS="-Dprofiler=true -Dprofiler.threshold=99999 --stats" -C ${BUILD:-../../build/release}/stage2 --output-sync -j$(nproc) 2>&1 | ./accumulate_profile.py'
+      # build only up to make-stdlib so Lake doesn't repeat its output, then finish the build to get
+      # the executables for further benchmarks, ignore output
+      bash -c 'set -eo pipefail; find ${BUILD:-../../build/release}/stage2 -name "*.olean" -delete; make LEAN_OPTS="-Dprofiler=true -Dprofiler.threshold=9999999 --stats" -C ${BUILD:-../../build/release}/stage2 --output-sync -j$(nproc) make_stdlib 2>&1 | ./accumulate_profile.py; make -C ${BUILD:-../../build/release}/stage2 -j$(nproc) 1>&2'
     max_runs: 2
     parse_output: true
   # initialize stage2 cmake + warmup