Race condition in lean4 stage2+ builds

Stream: lean4

[Nicolas Rouquette]

I'm preparing a PR for lean4 for this discussion: #mathlib4 > Where should List.mem_eraseDup and List.mem_eraseDups live?

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'

I tracked down a subtle race condition to src/CMakeLists.txt:

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 had leancpp as a dependent. This creates a race condition in which Init_shared may attempt to build before the runtime library has been copied.

The solution is fairly simple: add additional dependencies:

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(leanrt_initial-exec copy-leancpp)  # new
  add_dependencies(leanrt copy-leancpp)               # new
  add_dependencies(leancpp_1 copy-leancpp)            # new
  add_dependencies(leancpp copy-leancpp)

Is this appropriate as an issue/pr for lean4?

[Henrik Böving]

Certainly do open an issue and maybe a draft PR!

[Nicolas Rouquette]

ok, will do.

[Nicolas Rouquette]

Here's the issue: https://github.com/leanprover/lean4/issues/11808
and PR: https://github.com/leanprover/lean4/pull/11809

I'm having problems w/ the PR title & body compliance checker.

https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md

I don't understand what's the problem.

[Nicolas Rouquette]

ah I figured it out... a maintainer needs to add a label.

[Thomas Murrills]

Note: i believe you should be able to add the label yourself by commenting the name of the label on the PR (you can also comment "awaiting-review"! :) ), but I'm not sure changelog-fix is an option. You can see the available changelog labels here.