lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

fix: pass CMAKE_C/CXX_COMPILER to all stages

Open Vtec234 opened this issue 1 year ago • 2 comments

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

Vtec234 avatar Dec 16 '23 16:12 Vtec234

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.

Vtec234 avatar Dec 16 '23 16:12 Vtec234

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.

Kha avatar Dec 18 '23 08:12 Kha