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

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

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<size_t>((atoi(optarg) / 4) * 4) * static_cast<size_t>(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;

tests/bench/.gitignore

@@ -1,5 +1,5 @@
 *.out
-*.lean.cpp
+*.lean.c
 *.cmi
 *.cmx
 *.o

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)

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 {

tests/compiler/.gitignore

@@ -1,3 +1,3 @@
 *.lean.out
-*.lean.cpp
+*.lean.c
 test_flags.sh

tests/plugin/.gitignore

@@ -1,3 +1,3 @@
-*.cpp
+*.c
 *.o
 *.so