max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: restoreAllArtifacts = true for core (#10582)

Browse source 
This PR sets `restoreAllArtifacts = true` in the core build Lake
configuration file.
This commit is contained in:
Mac Malone 2025-09-26 23:30:21 -04:00 • committed by GitHub
parent 0bf7741a3e
commit 05300f7b51
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/lakefile.toml.in
View file

@ -13,6 +13,11 @@ defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain", "Leanc"]
# The root of all the compiler output directories
buildDir = "${CMAKE_BINARY_DIR}"
# 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.
restoreAllArtifacts = true
# The directory of Lean source files (i.e., `src`)
srcDir = "${LEAN_SOURCE_DIR}"