lean4
lean4 copied to clipboard
fix: pass CMAKE_C/CXX_COMPILER to all stages
Summary
This PR fixes #2863, making a guess as to how that should be done. We replace the if/else/else
with if/else;if
so that CMAKE_C/CXX_COMPILER
is stored both in PLATFORM_ARGS
and CL_ARGS
and consequently passed to all stages. I am not sure what the original intent of the logic was, but the comment below makes it sound like this was indeed a bug.
# Use standard release build (discarding LEAN_CXX_EXTRA_FLAGS etc.) for stage0 by default since it is assumed to be "good", but still pass through CMake platform arguments (compiler, toolchain file, ..).
Link to RFC
or bug
issue: #2863
Hm, it looks like the CI build actually sets CMAKE_C_COMPILER
to a custom LLVM under stage1/bin
. Before this PR, the stage0 build was still using the system compiler instead of that. Perhaps this PR is the wrong approach and people should just use STAGE0_CMAKE_C_COMPILER
explicitly.
We can switch to STAGE0_CMAKE_C_COMPILER=cc
in CI, though I'm actually not sure why that's necessary - we shouldn't be forwarding -nostdinc
in this case.