diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix index ff69994ef0..7647056241 100644 --- a/nix/buildLeanPackage.nix +++ b/nix/buildLeanPackage.nix @@ -87,7 +87,7 @@ with builtins; let }; compileMod = mod: drv: mkDerivation { name = "${mod}-cc"; - buildInputs = [ leanc ]; + buildInputs = [ leanc stdenv.cc ]; hardeningDisable = [ "all" ]; oPath = drv.relpath + ".o"; inherit leancFlags; diff --git a/src/bin/leanc.in b/src/bin/leanc.in index def749ac5f..446c65addd 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -24,13 +24,7 @@ for arg in "$@"; do [[ $arg == "-print-ldflags" ]] && echo "${ldflags_ext[@]} ${ldflags[@]}" && exit done -# Check C++ compiler -for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ g++; do - if [ -f $cxx ] || command -v $cxx; then - export LEAN_CXX=$cxx && break - fi -done -[ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!" +[ -n "$LEAN_CXX" ] || LEAN_CXX=c++ # Note the `-x c` for treating all input as C code -@CMAKE_CXX_COMPILER_LAUNCHER@ $LEAN_CXX -D LEAN_MULTI_THREAD "${cflags[@]}" -x c "$@" -x none "${ldflags_ext[@]}" "${ldflags[@]}" -Wno-unused-command-line-argument +$LEAN_CXX -D LEAN_MULTI_THREAD "${cflags[@]}" -x c "$@" -x none "${ldflags_ext[@]}" "${ldflags[@]}" -Wno-unused-command-line-argument diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 1e41c5f291..e6f96cbe94 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -10,6 +10,7 @@ LEANMAKE_OPTS=\ BIN_OUT="${CMAKE_BINARY_DIR}/bin"\ LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\ LEANC_OPTS+="${LEANC_OPTS}"\ + LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}" MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\ CMAKE_LIKE_OUTPUT=1