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

chore: remove lakefile copy in root and tests/ (#8054)

Browse source 
As we use a different Lean in these directories, using those copies
always results in a full rebuild
This commit is contained in:
Sebastian Ullrich 2025-04-22 18:03:12 +02:00 • committed by GitHub
parent 5d82927d10
commit ad3ac150bc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/CMakeLists.txt
View file

@ -843,6 +843,4 @@ endif()
if(USE_LAKE AND STAGE EQUAL 1)
configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../tests/lakefile.toml)
configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../lakefile.toml)
endif()

2
src/stdlib.make.in
View file

@ -41,7 +41,7 @@ ifeq "${USE_LAKE} ${STAGE}" "ON 1"
# build in parallel
Init:
${PREV_STAGE}/bin/lake build Init Std Lean Lake LakeMain
${PREV_STAGE}/bin/lake build Init Std Lean Lake LakeMain $(LAKE_EXTRA_ARGS)
Std Lean Lake: Init