Race condition in lean4 stage2+ builds #11808
Description
Prerequisites
- Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues - Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries. - Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
[Clear and concise description of the issue]
The src/CMakeLists.txt file is missing dependencies on the copy-leancpp target that other targets depend on.
Context
[Broader context that the issue occurred in. If there was any prior discussion on the Lean Zulip, link it here as well.]
See this discussion: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Race.20condition.20in.20lean4.20stage2.2B.20builds/with/565479591
The src/CMakeLists.txt file has:
if(${STAGE} GREATER 1)
# reuse C++ parts, which don't change
...
add_custom_target(copy-leancpp
COMMAND cmake -E copy_if_different "${PREV_STAGE}/runtime/libleanrt_initial-exec.a" "${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleanrt.a" "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleancpp.a" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/temp/libleancpp_1.a" "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a")
add_dependencies(leancpp copy-leancpp)
...
endif()
When building stage 2 (or higher), `Init_shared` depends on the imported library `leanrt_initial-exec`, which references `${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a`. However, this file is only copied from the previous stage by the `copy-leancpp` custom target, which only has `leancpp` as a dependent. This creates a race condition in which `Init_shared` may attempt to build before the runtime library has been copied.
### Steps to Reproduce
1. My system runs RHEL9.6 and has `nproc=56` that triggers the race condition.
2.
3.
**Expected behavior:** [Clear and concise description of what you expect to happen]
Even with `nproc=56`, `stage2` and `stage3` should build without errors.
**Actual behavior:** [Clear and concise description of what actually happens]
My system (RHEL9.6 with nproc=56) ran into an error during `make -C build/release stage2`:
make[7]: Entering directory '/home/nfr/projects/tlr/integration/lean/lean4/src'
Build completed successfully (4183 jobs).
make[7]: Leaving directory '/home/nfr/projects/tlr/integration/lean/lean4/src'
make[6]: Leaving directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release/stage2'
[ 50%] Built target make_stdlib
make[6]: Entering directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release/stage2'
make[6]: Leaving directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release/stage2'
make[6]: Entering directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release/stage2'
make[6]: *** No rule to make target 'runtime/libleanrt_initial-exec.a', needed by 'CMakeFiles/Init_shared'. Stop.
make[6]: Leaving directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release/stage2'
make[5]: *** [CMakeFiles/Makefile2:1027: CMakeFiles/Init_shared.dir/all] Error 2
make[5]: Leaving directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release/stage2'
make[4]: *** [Makefile:146: all] Error 2
make[4]: Leaving directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release/stage2'
make[3]: *** [CMakeFiles/stage2.dir/build.make:86: stage2-prefix/src/stage2-stamp/stage2-build] Error 2
make[3]: Leaving directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release'
make[2]: *** [CMakeFiles/Makefile2:202: CMakeFiles/stage2.dir/all] Error 2
make[2]: Leaving directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release'
make[1]: *** [CMakeFiles/Makefile2:209: CMakeFiles/stage2.dir/rule] Error 2
make[1]: Leaving directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release'
make: *** [Makefile:221: stage2] Error 2
make: Leaving directory '/home/nfr/projects/tlr/integration/lean/lean4/build/release'
### Versions
[Output of `#version` or `#eval Lean.versionString`]
git master, commit f483c6c10f
[OS version, if not using live.lean-lang.org.]
### Additional Information
[Additional information, configuration or data that might be necessary to reproduce the issue]
### Impact
Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others are impacted by this issue, please ask them to add :+1: to it.