fix: update libleanrt.bc, rename to lean.h.bc

This adds `lean.h.bc`, a LLVM bitcode file of the Lean
runtime that is to be inlined. This is programatically generated.

1. This differs from the previous `libleanrt.ll`, since it produces an
   LLVM bitcode file, versus a textual IR file. The bitcode file
   is faster to parse and build an in-memory LLVM module from.
2. We build `lean.h.bc` by adding it as a target to `shell`,
   which ensures that it is always built.

3. We eschew the need for:

```cpp
```

which causes breakage in the build, since changing the meaning of
`static` messes with definitions in the C++ headers.

Instead, we build `lean.h.bc` by copying everything in
`src/include/lean/lean.h`, renaming `inline` to
`__attribute__(alwaysinline)` [which forces LLVM to generate
`alwaysinline` annotations], then running the `-O3` pass pipeline
to get reasonably optimised IR, and will be perfectly inlined
when linked into the generated LLVM code by
`src/Lean/Compiler/IR/EmitLLVM.lean`.

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

nix/bootstrap.nix

@@ -44,12 +44,12 @@ rec {
   leancpp = buildCMake {
     name = "leancpp";
     src = ../src;
-    buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" ];
+    buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" "runtime_bc" ];
     installPhase = ''
       mkdir -p $out
       mv lib/ $out/
       mv shell/CMakeFiles/shell.dir/lean.cpp.o $out/lib
-      mv runtime/libleanrt_initial-exec.a $out/lib
+      mv runtime/libleanrt_initial-exec.a runtime/lean.h.bc $out/lib
     '';
   };
   # rename derivation so `nix run` uses the right executable name but we still see the stage in the build log

src/runtime/CMakeLists.txt

@@ -18,11 +18,17 @@ target_compile_options(leanrt PRIVATE -ftls-model=local-exec)
 endif()
 
 if(LLVM)
+  if (NOT (CMAKE_CXX_COMPILER_ID MATCHES "Clang"))
+      message(FATAL_ERROR "building 'lean.h.bc', need CMAKE_CXX_COMPILER_ID to match Clang to build LLVM bitcode file of Lean runtime.")
+  endif()
+  FILE(READ "${CMAKE_CURRENT_SOURCE_DIR}/../include/lean/lean.h" LEAN_H)
+  # generate LLVM IR for `static inline` definitions in lean.h for the LLVM backend
+  string(REPLACE "static inline" "__attribute__((always_inline))" LEAN_H "${LEAN_H}")
+  file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c" "${LEAN_H}")
   add_custom_command(
-    OUTPUT libleanrt.bc
-    DEPENDS ${RUNTIME_OBJS} lean_inlines.c
-    # compile each runtime file with the original compile flags plus `-emit-llvm`, then `llvm-link` them together
-    COMMAND bash -ec "rm -rf runtmp || true; mkdir runtmp; for f in ${RUNTIME_OBJS_STR} lean_inlines.c; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} ${LEANC_OPTS} -I$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -I> $([[ $f = \*.cpp ]] || echo \"-x c\") \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -S -emit-llvm -o runtmp/$f.ll; done; llvm-link runtmp/*.ll -o libleanrt.bc"
+    OUTPUT lean.h.bc
+    DEPENDS ${RUNTIME_OBJS} ${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c
+    COMMAND bash -ec "${CMAKE_BINARY_DIR}/leanc.sh ${LEANC_OPTS} -I$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -I> -c ${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c -emit-llvm -o ${CMAKE_CURRENT_BINARY_DIR}/lean.h.bc"
     VERBATIM)
-  add_custom_target(runtime_bc DEPENDS libleanrt.bc)
+  add_custom_target(runtime_bc DEPENDS lean.h.bc)
 endif()

src/runtime/lean_inlines.c

@@ -1,3 +0,0 @@
-// generate LLVM IR for `static inline` definitions in lean.h for the LLVM backend
-#define static extern // work around clang not emitting code for unused `static` definitions
-#include <lean/lean.h>

src/shell/CMakeLists.txt

@@ -32,6 +32,13 @@ 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")