sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: fix shlib rebuild detection under LAKE_USE_CACHE (#12879)

Browse Source
This commit is contained in:
Sebastian Ullrich
2026-03-11 09:35:53 +01:00
committed by GitHub
parent 9fac847f5f
commit 4450ff8995
1 changed files with 10 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
src/stdlib.make.in
View File

@@ -93,6 +93,16 @@ ${LIB}/temp/empty.c:
# the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt
# Lake archive timestamps may be stale due to caching; use .trace files for rebuild decisions
ifeq "${USE_LAKE}" "ON"
$(OUTLIB)/libInit_shared$(SO): ${LIB}/lean/libInit.a.export.trace ${LIB}/lean/libStd.a.export.trace
$(OUTLIB)/libleanshared$(SO): ${LIB}/lean/libLean.a.export.trace
$(OUTLIB)/libLake_shared$(SO): ${LIB}/lean/libLean.a.export.trace ${LIB}/lean/libLake.a.export.trace
$(OUTBIN)/lake$(EXE): ${LIB}/temp/LakeMain.c.o.export.trace
$(OUTBIN)/leanc$(EXE): $(OUTARC)/libLeanc.a.trace
$(OUTBIN)/leanchecker$(EXE): $(OUTARC)/libLeanChecker.a.trace
endif
# we specify the precise file names here to avoid rebuilds
$(OUTLIB)/libInit_shared$(SO): ${LIB}/lean/libInit.a.export ${LIB}/lean/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c
$(link-preamble)