From 872d5fc7ba58e9edbcd717c074e0c3eb2c8c863d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 30 Apr 2020 17:09:23 +0200 Subject: [PATCH] feat: stop compiling Lean code as C++, remove `--cpp` option Since we don't use static initializers, really the only difference between using `clang` and `clang++` is the default inclusion of the C++ standard library. --- bin/leanc.in | 44 ++++++++++++--------------------------- src/shell/lean.cpp | 12 +++-------- tests/bench/.gitignore | 2 +- tests/bench/Makefile | 10 ++++----- tests/common.sh | 4 ++-- tests/compiler/.gitignore | 2 +- tests/plugin/.gitignore | 2 +- 7 files changed, 26 insertions(+), 50 deletions(-) diff --git a/bin/leanc.in b/bin/leanc.in index 8d18b74cd4..47549f5714 100644 --- a/bin/leanc.in +++ b/bin/leanc.in @@ -1,9 +1,10 @@ #!/usr/bin/env bash # Lean compiler # -# A simple wrapper around C and C++ compilers. Defaults to the compiler Lean was built with, -# which can be overridden with the environment variables `LEAN_CC` and `LEAN_CXX`. All parameters are passed -# as-is to the wrapped compiler. +# A simple wrapper around a C++ compiler. Defaults to the compiler Lean was built with, +# which can be overridden with the environment variable `LEAN_CXX`. All parameters are passed +# as-is to the wrapped compiler. Note that we use a C++ compiler purely for linking against +# the C++ standard library Lean depends on, all input files are treated as C code. # # Interesting options: # * `-U LEAN_MULTI_THREAD` can be used to optimize programs not making use of multi-threading @@ -11,38 +12,19 @@ set -e bindir=$(dirname $0) -# 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 # NOTE: leanstatic and leanstdlib are cyclically dependent linker_flags="-lleanstatic -lleanstdlib -lleanstatic -lleanstdlib" for arg in "$@"; do - [[ $use_c == maybe && $arg == "-c" ]] && use_c=yes - [[ $arg == *.c ]] && use_c=yes - [[ $arg == *.cpp ]] && use_c=no [[ $arg == "-shared" ]] && linker_flags="@LEANC_SHARED_LINKER_FLAGS@" done -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!" +# 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!" - @CMAKE_C_COMPILER_LAUNCHER@ $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -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!" - - @CMAKE_CXX_COMPILER_LAUNCHER@ $LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument -fi +# Note the `-x c` for treating all input as C code +@CMAKE_CXX_COMPILER_LAUNCHER@ $LEAN_CXX -x c -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" $linker_flags -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index caff44a53b..c5b763b012 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -194,8 +194,7 @@ static void display_help(std::ostream & out) { std::cout << " --githash display the git commit hash number used to build this binary\n"; std::cout << " --run executes the 'main' definition\n"; std::cout << " --make create olean file\n"; - std::cout << " --cpp=fname -c name of the C++ output file\n"; // TODO(Leo): delete - std::cout << " --c=fname -C name of the C output file\n"; + std::cout << " --c=fname -c name of the C output file\n"; std::cout << " --stdin take input from stdin\n"; std::cout << " --trust=num -t trust level (default: max) 0 means do not trust any macro,\n" << " and type check all imported modules\n"; @@ -239,8 +238,7 @@ static struct option g_long_options[] = { {"quiet", no_argument, 0, 'q'}, {"deps", no_argument, 0, 'd'}, {"timeout", optional_argument, 0, 'T'}, - {"cpp", optional_argument, 0, 'c'}, - {"c", optional_argument, 0, 'C'}, + {"c", optional_argument, 0, 'c'}, {"exitOnPanic", no_argument, 0, 'e'}, #if defined(LEAN_JSON) {"json", no_argument, 0, 'J'}, @@ -474,10 +472,6 @@ int main(int argc, char ** argv) { check_optarg("c"); c_output = optarg; break; - case 'C': - check_optarg("C"); - c_output = optarg; - break; case 's': lean::lthread::set_thread_stack_size( static_cast((atoi(optarg) / 4) * 4) * static_cast(1024)); @@ -602,7 +596,7 @@ int main(int argc, char ** argv) { } mod_fn = argv[optind++]; contents = read_file(mod_fn); - main_module_name = module_name_of_file(mod_fn, /* optional */ !olean_fn && !c_output); + main_module_name = module_name_of_file(mod_fn, /* optional */ !c_output); } bool ok = true; diff --git a/tests/bench/.gitignore b/tests/bench/.gitignore index e0d0bf25c3..eaa9e792f9 100644 --- a/tests/bench/.gitignore +++ b/tests/bench/.gitignore @@ -1,5 +1,5 @@ *.out -*.lean.cpp +*.lean.c *.cmi *.cmx *.o \ No newline at end of file diff --git a/tests/bench/Makefile b/tests/bench/Makefile index 31475377c2..f20bb38fe7 100644 --- a/tests/bench/Makefile +++ b/tests/bench/Makefile @@ -42,9 +42,9 @@ all: report_lean.tex report_cross.tex report %.lean: %.out: % -%.lean.cpp: %.lean - LEAN_PATH=Test=. $(LEAN_BIN)/lean --cpp=$@ $(LEAN_FLAGS) $< -%.lean.out: %.lean.cpp +%.lean.c: %.lean + LEAN_PATH=Test=. $(LEAN_BIN)/lean --c=$@ $(LEAN_FLAGS) $< +%.lean.out: %.lean.c $(LEAN_BIN)/leanc $(LEANC_FLAGS) -o $@ $< # Binaries x.lean.out and x.gcc.lean.out etc. are produced by the # same rules and x.lean source file by copying the latter to @@ -52,10 +52,10 @@ all: report_lean.tex report_cross.tex report # files of the two binaries. %.gcc.lean.out: LEAN_BIN = $(LEAN_GCC_BIN) %.gcc.lean: %.lean; ln -f $< $@ -%.no_reuse.lean.cpp: LEAN_BIN = $(LEAN_NO_REUSE_BIN) +%.no_reuse.lean.c: LEAN_BIN = $(LEAN_NO_REUSE_BIN) %.no_reuse.lean.out: LEAN_BIN = $(LEAN_NO_REUSE_BIN) %.no_reuse.lean: %.lean; ln -f $< $@ -%.no_borrow.lean.cpp: LEAN_BIN = $(LEAN_NO_BORROW_BIN) +%.no_borrow.lean.c: LEAN_BIN = $(LEAN_NO_BORROW_BIN) %.no_borrow.lean.out: LEAN_BIN = $(LEAN_NO_BORROW_BIN) %.no_borrow.lean: %.lean; ln -f $< $@ %.no_st.lean.out: LEAN_BIN = $(LEAN_NO_ST_BIN) diff --git a/tests/common.sh b/tests/common.sh index 077e8aca32..1fb80c718f 100644 --- a/tests/common.sh +++ b/tests/common.sh @@ -21,8 +21,8 @@ shift [ $# -eq 0 ] || fail "Usage: test_single.sh [-i] test-file.lean" function compile_lean { - lean --cpp="$f.cpp" "$f" || fail "Failed to compile $f into C++ file" - leanc -O3 -DNDEBUG -o "$f.out" "$@" "$f.cpp" || fail "Failed to compile C++ file $f.cpp" + lean --c="$f.c" "$f" || fail "Failed to compile $f into C file" + leanc -O3 -DNDEBUG -o "$f.out" "$@" "$f.c" || fail "Failed to compile C file $f.c" } function exec_check { diff --git a/tests/compiler/.gitignore b/tests/compiler/.gitignore index 54e1f44700..60b8eaa893 100644 --- a/tests/compiler/.gitignore +++ b/tests/compiler/.gitignore @@ -1,3 +1,3 @@ *.lean.out -*.lean.cpp +*.lean.c test_flags.sh \ No newline at end of file diff --git a/tests/plugin/.gitignore b/tests/plugin/.gitignore index 0536e865ea..9ce7001840 100644 --- a/tests/plugin/.gitignore +++ b/tests/plugin/.gitignore @@ -1,3 +1,3 @@ -*.cpp +*.c *.o *.so \ No newline at end of file