From 5c07c188b48bb5f28fa5ec121780e2a42dc93113 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 8 Jul 2021 09:45:31 +0200
Subject: [PATCH] feat: generate LLVM module of runtime

---
 src/runtime/CMakeLists.txt | 9 +++++++++
 src/shell/CMakeLists.txt   | 2 +-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt
index 046a45c972..0125e35d6d 100644
--- a/src/runtime/CMakeLists.txt
+++ b/src/runtime/CMakeLists.txt
@@ -5,3 +5,12 @@ platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
 process.cpp)
 add_library(runtime OBJECT ${RUNTIME_OBJS})
 add_library(leanruntime ${RUNTIME_OBJS})
+if(LLVM)
+  string(REPLACE ";" " " RUNTIME_OBJS_STR "${RUNTIME_OBJS}")
+  add_custom_command(
+    OUTPUT libleanruntime.bc
+    DEPENDS ${RUNTIME_OBJS}
+    COMMAND sh -ec "rm -rf runtmp || true; mkdir runtmp; for f in ${RUNTIME_OBJS_STR}; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -I$<JOIN:$<TARGET_PROPERTY:leanruntime,INCLUDE_DIRECTORIES>, -I> \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -S -emit-llvm -o runtmp/$f.bc; done; llvm-link runtmp/*.bc -o libleanruntime.bc"
+    VERBATIM)
+  add_custom_target(runtime_bc DEPENDS libleanruntime.bc)
+endif()
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 4f9e428dfd..817137a60c 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -27,7 +27,7 @@ string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
 add_custom_command(OUTPUT ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}
   COMMAND sh -c "LEANC_GMP=${GMP_LIBRARIES} LEAN_CXX='${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}' ${CMAKE_BINARY_DIR}/bin/leanc $<TARGET_OBJECTS:shell> ${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXE_LINKER_FLAGS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -o ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"
   VERBATIM
-  DEPENDS Init Std Lean leancpp shell)
+  DEPENDS Init Std Lean leancpp shell $<IF:$<BOOL:${LLVM}>,runtime_bc,>)
 
 add_custom_target(lean ALL
   DEPENDS ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX})