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

fix(bin/leanc.in): use C compiler only when not linking

Browse source
This commit is contained in:
Sebastian Ullrich 2019-09-04 17:53:53 +02:00
parent 2110da4784
commit e23eded178
1 changed files with 27 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
bin/leanc.in
View file

@ -11,26 +11,36 @@
set -e
bindir=$(dirname $0)
# Check C compiler
for cc in $LEAN_CC @CMAKE_C_COMPILER@ /usr/bin/gcc; do
if [ -f $cc ] || command -v $cc; then
export LEAN_CC=$cc && break
fi
# As an optimization, we use a C compiler for compiling object files without linking.
# C files produced by Lean are also valid C++ files, but C compilers tend to be faster.
# Final linking still has to be done by a C++ compiler because we need to link against the
# Lean runtime written in C++ (https://isocpp.org/wiki/faq/mixing-c-and-cpp#overview-mixing-langs).
use_c=maybe
for arg in "$@"; do
[[ $use_c == maybe && $arg == "-c" ]] && use_c=yes
[[ $arg == "*.cpp" ]] && use_c=no
done
[ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!"
# Check C++ compiler
for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/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!"
if [[ $use_c == yes ]]; then
# Check C compiler
for cc in $LEAN_CC @CMAKE_C_COMPILER@ /usr/bin/gcc; do
if [ -f $cc ] || command -v $cc; then
export LEAN_CC=$cc && break
fi
done
[ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!"
# NOTE: leanstatic and leanstdlib are cyclically dependent
$LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
else
# Check C++ compiler
for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/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!"
# Use C++ compiler if input contains substring ".cpp"
if [[ "$@" == *".cpp"* ]]; then
# NOTE: leanstatic and leanstdlib are cyclically dependent
$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
else
$LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
fi