diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0d37b08f9c..c14696c253 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -82,6 +82,7 @@ option(USE_MIMALLOC "use mimalloc" ON) # development-specific options option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF) option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON) +option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF) set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make") set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`") @@ -826,10 +827,13 @@ if(LEAN_INSTALL_PREFIX) set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}") endif() -if (STAGE GREATER 1) + +if (USE_LAKE_CACHE AND STAGE EQUAL 1) + set(LAKE_ARTIFACT_CACHE_TOML "true") +else() # The build of stage2+ may depend on local changes made to src/ that are not reflected by the # commit hash in stage1/bin/lean, so we make sure to disable the global cache - string(APPEND LEAN_EXTRA_LAKEFILE_TOML "\n\nenableArtifactCache = false") + set(LAKE_ARTIFACT_CACHE_TOML "false") endif() # Escape for `make`. Yes, twice. diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in index 75e3205dd8..758b397f03 100644 --- a/src/lakefile.toml.in +++ b/src/lakefile.toml.in @@ -16,6 +16,10 @@ buildType = "${CMAKE_BUILD_TYPE_TOML}" # The root of all the compiler output directories buildDir = "${CMAKE_BINARY_DIR}" +# Enables the Lake artifact cache if configured via CMake +# (i.e., for stage 1 when the CMake `USE_LAKE_CACHE` option is set). +enableArtifactCache = ${LAKE_ARTIFACT_CACHE_TOML} + # Ensure build artifacts end up in the build directory even when the Lake # local artifact cache is enabled. This is necessary because subsequent stages # will expect the previous stage's artifacts to be in the build directory.