From db2613ceadbd35c4e4442c0bcf15dd8a34b7cd03 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 9 Jan 2021 15:04:21 +0100
Subject: [PATCH] fix: leanc should not depend on ccache or cmake g++

use e.g. `LEAN_CXX=ccache clang++` to re-enable
---
 nix/buildLeanPackage.nix |  2 +-
 src/bin/leanc.in         | 10 ++--------
 src/stdlib.make.in       |  1 +
 3 files changed, 4 insertions(+), 9 deletions(-)

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