max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: leanc should not depend on ccache or cmake g++

Browse source 
use e.g. `LEAN_CXX=ccache clang++` to re-enable
This commit is contained in:
Sebastian Ullrich 2021-01-09 15:04:21 +01:00
parent 3407202436
commit db2613cead
3 changed files with 4 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
nix/buildLeanPackage.nix
View file

@ -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;

10
src/bin/leanc.in
View file

@ -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

1
src/stdlib.make.in
View file

@ -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