feat: enable LLVM in stage1+ compiler

CMakeLists.txt

@@ -15,6 +15,9 @@ foreach(var ${vars})
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
+    if("${var}" MATCHES "LLVM*")
+      list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
+    endif()
   elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
     list(APPEND PLATFORM_ARGS "-D${var}=${${var}}")
   endif()

script/prepare-llvm-linux.sh

@@ -51,7 +51,7 @@ OPTIONS=()
 echo -n " -DLLVM=ON -DLLVM_CONFIG=$PWD/llvm-host/bin/llvm-config" # manually point to `llvm-config` location
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
-echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}' -DLEAN_EXTRA_MAKE_OPTS='${EXTRA_FLAGS:-}'"
 # use target compiler directly when not cross-compiling
 if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"

script/prepare-llvm-macos.sh

@@ -43,7 +43,7 @@ echo -n " -DLLVM=ON -DLLVM_CONFIG=$PWD/llvm-host/bin/llvm-config" # manually poi
 echo -n " -DLEAN_STANDALONE=ON"
 # do not change C++ compiler; libc++ etc. being system libraries means there's no danger of conflicts,
 # and the custom clang++ outputs a myriad of warnings when consuming the SDK
-echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}'"
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}' -DLEAN_EXTRA_MAKE_OPTS='${EXTRA_FLAGS:-}'"
 if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
   gcp $GMP/lib/libgmp.a stage1/lib/

src/CMakeLists.txt

@@ -143,7 +143,7 @@ set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")
 
 # OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.
 if ((${MULTI_THREAD} MATCHES "ON") AND (${CMAKE_SYSTEM_NAME} MATCHES "Darwin"))
-  set(LEAN_EXTRA_MAKE_OPTS -s40000 ${LEAN_EXTRA_MAKE_OPTS})
+  string(APPEND LEAN_EXTRA_MAKE_OPTS " -s40000")
 endif ()
 
 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
@@ -312,7 +312,12 @@ endif()
 string(APPEND LEANC_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 string(APPEND LEANSHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
-if(LLVM)
+if (LLVM)
+  string(APPEND LEANSHARED_LINKER_FLAGS " -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}")
+  string(APPEND CMAKE_CXX_FLAGS " -I${LLVM_CONFIG_INCLUDEDIR}")
+endif()
+
+if(LLVM AND ${STAGE} GREATER 0)
     # Here, we perform a replacement of `llvm-host` with `llvm`. This is necessary for our cross-compile
     #   builds in `script/prepare-llvm-*.sh`.
     # - Recall that the host's copy of LLVM binaries and libraries is at
@@ -326,9 +331,7 @@ if(LLVM)
     #   compiler options, and change the output of the host to point to the target.
     # - In particular, `host/bin/llvm-config` produces flags like `-Lllvm-host/lib/libLLVM`, while
     #   we need the path to be `-Lllvm/lib/libLLVM`. Thus, we perform this replacement here.
-    string(APPEND LEANSHARED_LINKER_FLAGS " -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}")
     string(REPLACE "llvm-host" "llvm" LEANSHARED_LINKER_FLAGS ${LEANSHARED_LINKER_FLAGS})
-    string(APPEND CMAKE_CXX_FLAGS  " -I${LLVM_CONFIG_INCLUDEDIR}")
     string(REPLACE "llvm-host" "llvm" LEAN_EXTRA_CXX_FLAGS ${LEAN_EXTRA_CXX_FLAGS})
     message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${LEAN_EXTR_CXX_FLAGS}'")
 endif()
@@ -508,6 +511,12 @@ else()
   endif()
 endif()
 
+# Build the compiler using the bootstraped C sources for stage0, and use
+# the LLVM build for stage1 and further.
+if (LLVM AND ${STAGE} GREATER 0)
+  set(EXTRA_LEANMAKE_OPTS "LLVM=1")
+endif()
+
 # Escape for `make`. Yes, twice.
 string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
 string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")
@@ -520,6 +529,12 @@ add_custom_target(make_stdlib ALL
   COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Lean
   VERBATIM)
 
+# if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode
+# of Lean runtime to be built.
+if (LLVM AND ${STAGE} EQUAL 1)
+   add_dependencies(make_stdlib runtime_bc)
+endif()
+
 # We declare these as separate custom targets so they use separate `make` invocations, which makes `make` recompute which dependencies
 # (e.g. `libLean.a`) are now newer than the target file
 

src/lean.mk.in

@@ -55,18 +55,26 @@ $(OLEAN_OUT)/$(PKG) $(LIB_OUT) $(BIN_OUT):
 # .olean files will be located even before any of them are actually built.
 $(TEMP_OUT)/%.depend: %.lean | $(OLEAN_OUT)/$(PKG)
 	@mkdir -p "$(TEMP_OUT)/$(*D)"
-# use separate assignment to ensure failure propagation
 # convert path separators and newlines on Windows
-	@deps=`$(LEAN) --deps $< | tr '\\\\' / | tr -d '\\r'`; echo $(OLEAN_OUT)/$(<:.lean=.olean): $$deps > $@
+	deps=`$(LEAN) --deps $<` || (echo "$(LEAN) --deps $< failed ($$?): $$deps"; exit 1); \
+  deps=`echo "$$deps" | tr '\\\\' / | tr -d '\\r'`; \
+  echo $(OLEAN_OUT)/$(<:.lean=.olean): $$deps > $@
 
 $(OLEAN_OUT)/%.olean: %.lean $(TEMP_OUT)/%.depend $(MORE_DEPS)
 ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Building $<"
 endif
 	@mkdir -p $(OLEAN_OUT)/$(*D)
+ifndef LLVM
 	$(LEAN) $(LEAN_OPTS) -o "$@" -i "$(OLEAN_OUT)/$*.ilean" --c="$(TEMP_OUT)/$*.c.tmp" $<
 # create the .c file atomically
-	mv "$(TEMP_OUT)/$*.c.tmp" "$(TEMP_OUT)/$*.c"
+	@mv "$(TEMP_OUT)/$*.c.tmp" "$(TEMP_OUT)/$*.c"
+else
+	$(LEAN) $(LEAN_OPTS) -o "$@" -i "$(OLEAN_OUT)/$*.ilean" --c="$(TEMP_OUT)/$*.c.tmp" --bc="$(TEMP_OUT)/$*.bc.tmp" $<
+	@mv "$(TEMP_OUT)/$*.c.tmp" "$(TEMP_OUT)/$*.c"
+	@mv "$(TEMP_OUT)/$*.bc.tmp" "$(TEMP_OUT)/$*.bc"
+	@mv "$(TEMP_OUT)/$*.bc.tmp.o" "$(TEMP_OUT)/$*.o"
+endif
 
 $(OLEAN_OUT)/%.ilean: $(OLEAN_OUT)/%.olean
 	@
@@ -76,6 +84,11 @@ $(TEMP_OUT)/%.c: $(OLEAN_OUT)/%.olean
 	@
 endif
 
+ifdef LLVM
+# currently built as part of `--bc`
+$(TEMP_OUT)/%.o: $(OLEAN_OUT)/%.olean
+	@
+else
 $(TEMP_OUT)/%.o: $(C_OUT)/%.c
 ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Building $<"
@@ -86,6 +99,7 @@ ifdef PROFILE
 else
 	$(LEANC) -c -o $@ $< $(LEANC_OPTS)
 endif
+endif
 
 $(BIN_OUT)/$(BIN_NAME): $(addprefix $(TEMP_OUT)/,$(REL_OS)) | $(BIN_OUT)
 ifdef CMAKE_LIKE_OUTPUT

src/shell/CMakeLists.txt

@@ -32,13 +32,6 @@ add_custom_target(lean ALL
   COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lean LEAN_SHELL="$<TARGET_OBJECTS:shell>"
   COMMAND_EXPAND_LISTS)
 
-# if we have LLVM enabled, then build `libruntime.bc` which has the LLVM bitcode
-# of Lean runtime to be built.
-if (LLVM)
-   add_dependencies(lean runtime_bc)
-endif()
-
-
 # use executable of current stage for tests
 string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
 

src/stdlib.make.in

@@ -22,6 +22,7 @@ LEANMAKE_OPTS=\
 	LEANC_OPTS+="${LEANC_OPTS}"\
 	LEAN_AR="${CMAKE_AR}"\
 	MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
+	${EXTRA_LEANMAKE_OPTS}\
 	CMAKE_LIKE_OUTPUT=1
 
 ifeq "${STAGE}" "0"

tests/compiler/foreign/Makefile

@@ -1,5 +1,6 @@
 CXX ?= c++
 CPPFLAGS = -O3
+# TODO: use Lake instead
 include lean.mk
 
 CPP_SRCS = myfuns.cpp