feat(bin/leanc): add simple C++ compiler wrapper script

.gitignore

@@ -24,3 +24,5 @@ settings.json
 CMakeSettings.json
 CppProperties.json
 /library/Makefile
+/bin/*.a
+/bin/leanc

bin/leanc.in

@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+# Lean 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.
+#
+# Interesting options:
+# * `-U LEAN_MULTI_THREAD` can be used to optimize programs not making use of multi-threading
+
+set -e
+bindir=$(dirname $0)
+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!"
+$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD -pthread -fPIC "-I$bindir/../src" "$@" "-L$bindir" -ldl -Wl,-Bstatic -lleanstatic -lgmp @LEANC_EXTRA_LIBS@ -static-libgcc -static-libstdc++ -Wl,-Bdynamic -Wno-unused-command-line-argument

src/CMakeLists.txt

@@ -323,7 +323,7 @@ else()
     # GMP
     find_package(GMP 5.0.5 REQUIRED)
     include_directories(${GMP_INCLUDE_DIR})
-    set(EXTRA_LIBS ${EXTRA_LIBS} ${GMP_LIBRARIES})
+    set(COPY_LIBS ${COPY_LIBS} ${GMP_LIBRARIES})
 endif()
 
 # DL
@@ -344,7 +344,8 @@ endif()
 if(JEMALLOC)
   find_package(Jemalloc)
   if(${JEMALLOC_FOUND})
-    set(EXTRA_UTIL_LIBS ${EXTRA_UTIL_LIBS} ${JEMALLOC_LIBRARIES})
+    set(COPY_LIBS ${COPY_LIBS} ${JEMALLOC_LIBRARIES})
+    set(LEANC_EXTRA_LIBS "${LEANC_EXTRA_LIBS} -ljemalloc")
     message(STATUS "Using jemalloc.")
     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D HAS_JEMALLOC")
   else()
@@ -357,7 +358,8 @@ if(NOT "${JEMALLOC_FOUND}")
  if(TCMALLOC)
    find_package(Tcmalloc)
    if(${TCMALLOC_FOUND})
-     set(EXTRA_LIBS ${EXTRA_LIBS} ${TCMALLOC_LIBRARIES})
+     set(COPY_LIBS ${COPY_LIBS} ${TCMALLOC_LIBRARIES})
+    set(LEANC_EXTRA_LIBS "${LEANC_EXTRA_LIBS} -ltcmalloc")
      message(STATUS "Using tcmalloc.")
      set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D HAS_TCMALLOC")
    else()
@@ -368,7 +370,7 @@ if(NOT "${JEMALLOC_FOUND}")
  endif()
 endif()
 
-set(EXTRA_LIBS ${EXTRA_LIBS} ${EXTRA_UTIL_LIBS})
+set(EXTRA_LIBS ${EXTRA_LIBS} ${COPY_LIBS})
 
 # Python
 find_package(PythonInterp)
@@ -479,9 +481,17 @@ endif()
 
 ADD_CUSTOM_TARGET(bin_lib ALL
    COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
-   COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/libleanstatic*" "${LEAN_SOURCE_DIR}/../bin"
+   COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "${CMAKE_CURRENT_BINARY_DIR}/libleanstatic*" "${LEAN_SOURCE_DIR}/../bin"
    DEPENDS leanstatic
 )
+# Configure leanc
+configure_file("${LEAN_SOURCE_DIR}/../bin/leanc.in" "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc")
+file(COPY "${CMAKE_CURRENT_BINARY_DIR}/tmp/leanc"
+  DESTINATION "${LEAN_SOURCE_DIR}/../bin"
+  FILE_PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
+install(FILES "${LEAN_SOURCE_DIR}/../bin/leanc"
+  DESTINATION bin
+  PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)
 
 # The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).
 # For some strange reason, it contains a copy of pthread_equal.

src/shell/CMakeLists.txt

@@ -20,9 +20,6 @@ add_executable(lean lean.cpp)
 target_link_libraries(lean leanstatic)
 install(TARGETS lean DESTINATION bin)
 
-# Configure compiler test scripts
-configure_file("${LEAN_SOURCE_DIR}/../tests/compiler/test_flags.sh.in" "${LEAN_SOURCE_DIR}/../tests/compiler/test_flags.sh")
-
 if(${EMSCRIPTEN})
     set(NODE_JS "node --stack_size=8192")
 

tests/compiler/test_flags.sh.in

@@ -1,4 +0,0 @@
-CXX='@CMAKE_CXX_COMPILER@'
-CXX_FLAGS='@CMAKE_CXX_FLAGS@ @CMAKE_CXX_FLAGS_RELEASE@'
-LINKER_FLAGS='@CMAKE_EXE_LINKER_FLAGS@'
-LIBS='@EXTRA_LIBS@'

tests/compiler/test_single.sh

@@ -4,10 +4,8 @@ if [ $# -ne 3 -a $# -ne 2 ]; then
     exit 1
 fi
 ulimit -s 8192
-source test_flags.sh
 LEAN=$1
 BIN_DIR=../../bin
-INCLUDE_DIR=../../src
 export LEAN_PATH=../../library:.
 if [ $# -ne 3 ]; then
     INTERACTIVE=no
@@ -16,16 +14,6 @@ else
 fi
 ff=$2
 
-# Hack for converting a list of libraries such as `/usr/lib/gmp.so;dl` into valid liker parameters.
-LINKER_LIBS=""
-for lib in ${LIBS//;/ }; do
-  if [[ $lib == *".so" || $lib == *".dll" || $lib == *".dylib" ]]; then
-    LINKER_LIBS="$LINKER_LIBS $lib"
-  else
-    LINKER_LIBS="$LINKER_LIBS -l$lib"
-  fi
-done
-
 if [[ "$OSTYPE" == "msys" ]]; then
     # Windows running MSYS2
     # Replace /c/ with c:, and / with \\
@@ -43,7 +31,7 @@ if [ $? -ne 0 ]; then
     exit 1
 fi
 
-$CXX -o "$ff.out" -I $INCLUDE_DIR $CXX_FLAGS $ff.cpp $BIN_DIR/libleanstatic.a $LINKER_FLAGS $LINKER_LIBS
+$BIN_DIR/leanc -o "$ff.out" $ff.cpp
 if [ $? -ne 0 ]; then
     echo "Failed to compile C++ file $ff.cpp"
     exit 1

tests/playground/compile.sh

@@ -4,23 +4,11 @@ if [ $# -eq 0 ]; then
     exit 1
 fi
 ulimit -s 8192
-source ../compiler/test_flags.sh
 BIN_DIR=../../bin
 LEAN=$BIN_DIR/lean
-INCLUDE_DIR=../../src
 export LEAN_PATH=../../library:.
 ff=$1
 
-# Hack for converting a list of libraries such as `/usr/lib/gmp.so;dl` into valid liker parameters.
-LINKER_LIBS=""
-for lib in ${LIBS//;/ }; do
-  if [[ $lib == *".so" || $lib == *".dll" || $lib == *".dylib" ]]; then
-    LINKER_LIBS="$LINKER_LIBS $lib"
-  else
-    LINKER_LIBS="$LINKER_LIBS -l$lib"
-  fi
-done
-
 if [[ "$OSTYPE" == "msys" ]]; then
     # Windows running MSYS2
     # Replace /c/ with c:, and / with \\
@@ -33,7 +21,7 @@ if [ $? -ne 0 ]; then
     exit 1
 fi
 
-$CXX -o "$ff.out" -I $INCLUDE_DIR $CXX_FLAGS $ff.cpp $BIN_DIR/libleanstatic.a $LINKER_FLAGS $LINKER_LIBS
+$BIN_DIR/leanc -o "$ff.out" $ff.cpp
 if [ $? -ne 0 ]; then
     echo "Failed to compile C++ file $ff.cpp"
     exit 1