diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8cd477dcb824..0120f18bdb2d 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -421,19 +421,21 @@ jobs:
             progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
             echo bt | $GDB/bin/gdb -q $progbin $c || true
           done
-      - name: Upload coredumps
-        uses: actions/upload-artifact@v3
-        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
-        with:
-          name: coredumps-${{ matrix.name }}
-          path: |
-            ./coredumps
-            ./build/stage0/bin/lean
-            ./build/stage0/lib/lean/libleanshared.so
-            ./build/stage1/bin/lean
-            ./build/stage1/lib/lean/libleanshared.so
-            ./build/stage2/bin/lean
-            ./build/stage2/lib/lean/libleanshared.so
+      # has not been used in a long while, would need to be adapted to new
+      # shared libs
+      #- name: Upload coredumps
+      #  uses: actions/upload-artifact@v3
+      #  if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+      #  with:
+      #    name: coredumps-${{ matrix.name }}
+      #    path: |
+      #      ./coredumps
+      #      ./build/stage0/bin/lean
+      #      ./build/stage0/lib/lean/libleanshared.so
+      #      ./build/stage1/bin/lean
+      #      ./build/stage1/lib/lean/libleanshared.so
+      #      ./build/stage2/bin/lean
+      #      ./build/stage2/lib/lean/libleanshared.so
 
   # This job collects results from all the matrix jobs
   # This can be made the “required” job, instead of listing each
diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index 1dfe9b6d5609..d2ed69660b97 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -65,12 +65,7 @@ rec {
     installPhase = ''
       mkdir -p $out/bin $out/lib/lean
       mv bin/lean $out/bin/
-      mv lib/lean/libleanshared.* $out/lib/lean
-   '' + lib.optionalString stdenv.isDarwin ''
-      for lib in $(otool -L $out/bin/lean | tail -n +2 | cut -d' ' -f1); do
-        if [[ "$lib" == *lean* ]]; then install_name_tool -change "$lib" "$out/lib/lean/$(basename $lib)" $out/bin/lean; fi
-      done
-      otool -L $out/bin/lean
+      mv lib/lean/*.so $out/lib/lean
     '';
     meta.mainProgram = "lean";
   });
@@ -120,29 +115,35 @@ rec {
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
       stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
+      libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
+        mkdir $out
+        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared -Wl,-Bsymbolic \
+          -Wl,--whole-archive -lInit ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ -lm ${stdlibLinkFlags} \
+          $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
+          -o $out/$libName
+      '';
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
-        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
-          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
-            else "-Wl,--whole-archive -lInit -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
+        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared -Wl,-Bsymbolic \
+          ${libInit_shared}/* -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lstdc++ -lm ${stdlibLinkFlags} \
           $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
           -o $out/$libName
       '';
       mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
       print-paths = Lean.makePrintPathsFor [] mods;
       leanc = writeShellScriptBin "leanc" ''
-        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${leanshared} "$@"
+        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared} "$@"
       '';
       lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
         mkdir -p $out/bin
-        ${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${leanshared}/* -o $out/bin/lean
+        ${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${libInit_shared}/* ${leanshared}/* -o $out/bin/lean
       '';
       # derivation following the directory layout of the "basic" setup, mostly useful for running tests
       lean-all = stdenv.mkDerivation {
         name = "lean-${desc}";
         buildCommand = ''
           mkdir -p $out/bin $out/lib/lean
-          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${leanshared}/* $out/lib/lean/
+          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared}/* $out/lib/lean/
           # put everything in a single final derivation so `IO.appDir` references work
           cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
           # NOTE: `lndir` will not override existing `bin/leanc`
diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix
index 4ae908836d63..9f478b46255c 100644
--- a/nix/buildLeanPackage.nix
+++ b/nix/buildLeanPackage.nix
@@ -10,7 +10,7 @@ lib.makeOverridable (
   staticLibDeps ? [],
   # Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
   groupStaticLibs ? false,
-  # Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a 
+  # Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a
   # shared library at the path `${shared}/${shared.libName or shared.name}` and a name to link to like `-l${shared.linkName or shared.name}`.
   # These libs are also linked to in packages that depend on this one.
   nativeSharedLibs ? [],
@@ -88,9 +88,9 @@ with builtins; let
   allNativeSharedLibs =
     lib.unique (lib.flatten (nativeSharedLibs ++ (map (dep: dep.allNativeSharedLibs or []) allExternalDeps)));
 
-  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`, 
+  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`,
   # plus every dep module itself: `dep.staticLib`
-  allStaticLibDeps = 
+  allStaticLibDeps =
     lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) allExternalDeps)));
 
   pathOfSharedLib = dep: dep.libPath or "${dep}/${dep.libName or dep.name}";
@@ -249,7 +249,7 @@ in rec {
     ${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
     ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
   executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
-      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.leanshared}/*";
+      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.libInit_shared}/* ${lean-final.leanshared}/*";
     in runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
       mkdir -p $out/bin
       leanc ${staticLibLinkWrapper (lib.concatStringsSep " " (objPaths ++ map (d: "${d}/*.a") allStaticLibDeps))} \
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index de76e3ce42ba..976841c15455 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -299,13 +299,12 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
     cmake_path(GET ZLIB_LIBRARY PARENT_PATH ZLIB_LIBRARY_PARENT_PATH)
     string(APPEND LEANSHARED_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}")
   endif()
-  string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt")
+  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lnodefs.js -lleanrt")
+  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lnodefs.js -lleanrt")
 else()
-  string(APPEND LEANC_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
+  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
 endif()
-string(APPEND LEANC_STATIC_LINKER_FLAGS " -lLake")
 
 set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
 
@@ -313,8 +312,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEAN_CXX_STDLIB "-lc++")
 endif()
 
-string(APPEND LEANC_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
-string(APPEND LEANSHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
+string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
+string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
+
+# flags for user binaries = flags for toolchain binaries + Lake
+string(APPEND LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
 
 if (LLVM)
   string(APPEND LEANSHARED_LINKER_FLAGS " -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}")
@@ -342,9 +344,9 @@ endif()
 
 # get rid of unused parts of C++ stdlib
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-dead_strip")
+  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-dead_strip")
 elseif(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--gc-sections")
+  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,--gc-sections")
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
@@ -354,26 +356,20 @@ endif()
 if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
   if(BSYMBOLIC)
     string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
-    string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
+    string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
   endif()
   string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
   string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
-  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
+  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
+  string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
   string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   string(APPEND CMAKE_CXX_FLAGS " -fPIC")
   string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
-  # We do not use dynamic linking via leanshared for Emscripten to keep things
-  # simple. (And we are not interested in `Lake` anyway.) To use dynamic
-  # linking, we would probably have to set MAIN_MODULE=2 on `leanshared`,
-  # SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js".
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,--whole-archive -lInit -lLean -lleancpp -lleanrt ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1")
-elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
@@ -399,7 +395,7 @@ endif()
 # are already loaded) and probably fail unless we set up LD_LIBRARY_PATH.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   # import library created by the `leanshared` target
-  string(APPEND LEANC_SHARED_LINKER_FLAGS " -lleanshared")
+  string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared")
 elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
   string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-undefined,dynamic_lookup")
 endif()
@@ -506,13 +502,31 @@ string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
 file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
+  string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a")
 else()
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
+  string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive")
+  if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+    string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
+  endif()
+endif()
+
+if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
+else()
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive")
   if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
     string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
   endif()
 endif()
+string(APPEND LEANSHARED_LINKER_FLAGS " -lInit_shared")
+
+if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
+  # We do not use dynamic linking via leanshared for Emscripten to keep things
+  # simple. (And we are not interested in `Lake` anyway.) To use dynamic
+  # linking, we would probably have to set MAIN_MODULE=2 on `leanshared`,
+  # SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js".
+  string(APPEND LEAN_EXE_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1")
+endif()
 
 # Build the compiler using the bootstrapped C sources for stage0, and use
 # the LLVM build for stage1 and further.
@@ -520,10 +534,6 @@ 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}")
-configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
 add_custom_target(make_stdlib ALL
   WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
   # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
@@ -541,13 +551,33 @@ 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
 
-add_custom_target(leanshared ALL
-  WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
-  DEPENDS make_stdlib leancpp leanrt_initial-exec
-  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
-  VERBATIM)
+if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
+  # dummy targets, see `MAIN_MODULE` discussion above
+  add_custom_target(Init_shared ALL
+    DEPENDS make_stdlib leanrt_initial-exec
+    COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
+  )
+  add_custom_target(leanshared ALL
+    DEPENDS Init_shared leancpp
+    COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
+  )
+else()
+  add_custom_target(Init_shared ALL
+    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
+    DEPENDS make_stdlib leanrt_initial-exec
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init_shared
+    VERBATIM)
+
+  add_custom_target(leanshared ALL
+    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
+    DEPENDS Init_shared leancpp
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
+    VERBATIM)
 
-if(${STAGE} GREATER 0)
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared")
+endif()
+
+if(${STAGE} GREATER 0 AND NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   if(NOT EXISTS ${LEAN_SOURCE_DIR}/lake/Lake.lean)
     message(FATAL_ERROR "src/lake does not exist. Please check out the Lake submodule using `git submodule update --init src/lake`.")
   endif()
@@ -568,7 +598,7 @@ endif()
 
 # use Bash version for building, use Lean version in bin/ for tests & distribution
 configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/leanc.sh" @ONLY)
-if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean)
+if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean AND NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   configure_file("${LEAN_SOURCE_DIR}/Leanc.lean" "${CMAKE_BINARY_DIR}/leanc/Leanc.lean" @ONLY)
   add_custom_target(leanc ALL
     WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc
@@ -619,3 +649,8 @@ if(LEAN_INSTALL_PREFIX)
   set(LEAN_INSTALL_SUFFIX "-${LOWER_SYSTEM_NAME}" CACHE STRING "If LEAN_INSTALL_PREFIX is set, append this value to CMAKE_INSTALL_PREFIX")
   set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
 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}")
+configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
diff --git a/src/lake/examples/reverse-ffi/Makefile b/src/lake/examples/reverse-ffi/Makefile
index 4d3e21f4b669..1942659b1b5e 100644
--- a/src/lake/examples/reverse-ffi/Makefile
+++ b/src/lake/examples/reverse-ffi/Makefile
@@ -23,7 +23,7 @@ endif
 
 $(OUT_DIR)/main: main.c lake | $(OUT_DIR)
 # Add library paths for Lake package and for Lean itself
-	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/.lake/build/lib -lRFFI -lleanshared $(LINK_FLAGS)
+	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/.lake/build/lib -lRFFI -lInit_shared -lleanshared $(LINK_FLAGS)
 
 run: $(OUT_DIR)/main
 ifeq ($(OS),Windows_NT)
@@ -39,7 +39,7 @@ endif
 ifeq ($(OS),Windows_NT)
 SHLIB_PREFIX :=
 SHLIB_EXT := dll
-LEAN_SHLIB := $(LEAN_SYSROOT)/bin/libleanshared.$(SHLIB_EXT)
+LEAN_SHLIB_ROOT := $(shell cygpath $(LEAN_SYSROOT)/bin)
 else
 SHLIB_PREFIX := lib
 # Add current directory to loader path (default on Windows)
@@ -50,12 +50,12 @@ else
 LINK_FLAGS_LOCAL := -Wl,-rpath,'$${ORIGIN}'
 SHLIB_EXT := so
 endif
-LEAN_SHLIB=$(LEAN_LIBDIR)/libleanshared.$(SHLIB_EXT)
+LEAN_SHLIB_ROOT := $(LEAN_LIBDIR)
 endif
 
 $(OUT_DIR)/main-local: main.c lake | $(OUT_DIR)
-	cp -f $(LEAN_SHLIB) lib/.lake/build/lib/$(SHLIB_PREFIX)RFFI.$(SHLIB_EXT) $(OUT_DIR)
-	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -lRFFI -lleanshared $(LINK_FLAGS_LOCAL)
+	cp -f $(LEAN_SHLIB_ROOT)/*.$(SHLIB_EXT) lib/.lake/build/lib/$(SHLIB_PREFIX)RFFI.$(SHLIB_EXT) $(OUT_DIR)
+	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -lRFFI -lInit_shared -lleanshared $(LINK_FLAGS_LOCAL)
 
 run-local: $(OUT_DIR)/main-local
 	$(OUT_DIR)/main-local
diff --git a/src/runtime/apply.h b/src/runtime/apply.h
index 7a08d58d1cd0..7b297951b7c7 100644
--- a/src/runtime/apply.h
+++ b/src/runtime/apply.h
@@ -7,5 +7,5 @@ Author: Leonardo de Moura
 #pragma once
 #include "runtime/object.h"
 namespace lean {
-object * curry(void * f, unsigned n, object ** as);
+LEAN_EXPORT object * curry(void * f, unsigned n, object ** as);
 }
diff --git a/src/runtime/compact.h b/src/runtime/compact.h
index 8664c0614d35..2bb05a4fca13 100644
--- a/src/runtime/compact.h
+++ b/src/runtime/compact.h
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 namespace lean {
 typedef lean_object * object_offset;
 
-class object_compactor {
+class LEAN_EXPORT object_compactor {
     struct max_sharing_table;
     friend struct max_sharing_hash;
     friend struct max_sharing_eq;
@@ -55,7 +55,7 @@ class object_compactor {
     void const * data() const { return m_begin; }
 };
 
-class compacted_region {
+class LEAN_EXPORT compacted_region {
     // see `object_compactor::m_base_addr`
     void * m_base_addr;
     bool m_is_mmap;
diff --git a/src/runtime/debug.h b/src/runtime/debug.h
index d3d857a66f0c..1ddc06445c3a 100644
--- a/src/runtime/debug.h
+++ b/src/runtime/debug.h
@@ -27,89 +27,20 @@ Author: Leonardo de Moura
 #define lean_verify(COND) (COND)
 #endif
 
-// LEAN_NARG(ARGS...) return the number of arguments.
-// This is a hack based on the following stackoverflow post:
-// http://stackoverflow.com/questions/11317474/macro-to-count-number-of-arguments
-#define LEAN_COMMASEQ_N() 1,   1,  1,  1,  1,  1,  1,  1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0
-#define LEAN_RSEQ_N()     17, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0
-#define LEAN_ARG_N(_1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, N, ...) N
-#define LEAN_EXPAND(x) x
-#ifdef _MSC_VER
-#define LEAN_AUGMENT(...) dummy, __VA_ARGS__
-#define LEAN_NARG_1(...) LEAN_EXPAND(LEAN_ARG_N(__VA_ARGS__, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0))
-#define LEAN_NARG(...) LEAN_NARG_1(LEAN_AUGMENT(__VA_ARGS__))
-#else
-#define LEAN_NARG_(ARGS...)    LEAN_ARG_N(ARGS)
-#define LEAN_HASCOMMA(ARGS...) LEAN_NARG_(ARGS, LEAN_COMMASEQ_N())
-#define LEAN_COMMA() ,
-#define LEAN_NARG_HELPER3_01(N)    0
-#define LEAN_NARG_HELPER3_00(N)    1
-#define LEAN_NARG_HELPER3_11(N)    N
-#define LEAN_NARG_HELPER2(a, b, N) LEAN_NARG_HELPER3_ ## a ## b(N)
-#define LEAN_NARG_HELPER1(a, b, N) LEAN_NARG_HELPER2(a, b, N)
-#define LEAN_NARG(ARGS...)         LEAN_NARG_HELPER1(LEAN_HASCOMMA(ARGS), LEAN_HASCOMMA(LEAN_COMMA ARGS ()), LEAN_NARG_(ARGS, LEAN_RSEQ_N()))
-#endif
-
-// Hack for LEAN_DISPLAY(ARGS...)
-// It works for at most 16 arguments.
-#define LEAN_DISPLAY1_CORE(V)       lean::debug::display_var(#V, V);
-#define LEAN_DISPLAY2_CORE(V, ...)  lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY1_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY3_CORE(V, ...)  lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY2_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY4_CORE(V, ...)  lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY3_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY5_CORE(V, ...)  lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY4_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY6_CORE(V, ...)  lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY5_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY7_CORE(V, ...)  lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY6_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY8_CORE(V, ...)  lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY7_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY9_CORE(V, ...)  lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY8_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY10_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY9_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY11_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY10_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY12_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY11_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY13_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY12_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY14_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY13_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY15_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY14_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY16_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY15_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY0(...)
-#define LEAN_DISPLAY1(ARG)          std::cerr << "Argument\n";  LEAN_DISPLAY1_CORE(ARG)
-#define LEAN_DISPLAY2(...)          std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY2_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY3(...)          std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY3_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY4(...)          std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY4_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY5(...)          std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY5_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY6(...)          std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY6_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY7(...)          std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY7_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY8(...)          std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY8_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY9(...)          std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY9_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY10(...)         std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY10_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY11(...)         std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY11_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY12(...)         std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY12_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY13(...)         std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY13_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY14(...)         std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY14_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY15(...)         std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY15_CORE(__VA_ARGS__))
-#define LEAN_DISPLAY16(...)         std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY16_CORE(__VA_ARGS__))
-#define LEAN_JOIN0(A, B) A ## B
-#define LEAN_JOIN(A, B) LEAN_JOIN0(A, B)
-#define LEAN_DISPLAY(...) { LEAN_JOIN(LEAN_DISPLAY, LEAN_NARG(__VA_ARGS__))(__VA_ARGS__) }
-
-#define lean_assert(COND, ...) DEBUG_CODE({if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(__VA_ARGS__); lean::invoke_debugger(); }})
-#define lean_cond_assert(TAG, COND, ...) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(__VA_ARGS__); lean::invoke_debugger(); }})
-#define lean_always_assert(COND, ...) { if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(__VA_ARGS__); lean_unreachable(); } }
-
-#define lean_assert_eq(A, B) lean_assert(A == B, A, B)
-#define lean_assert_ne(A, B) lean_assert(A != B, A, B)
-#define lean_assert_gt(A, B) lean_assert(A > B, A, B)
-#define lean_assert_lt(A, B) lean_assert(A < B, A, B)
-#define lean_assert_ge(A, B) lean_assert(A >= B, A, B)
-#define lean_assert_le(A, B) lean_assert(A <= B, A, B)
+#define lean_assert(COND) DEBUG_CODE({if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }})
+#define lean_cond_assert(TAG, COND) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); }})
+#define lean_always_assert(COND) { if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean_unreachable(); } }
 
 namespace lean {
 void initialize_debug();
 void finalize_debug();
-void notify_assertion_violation(char const * file_name, int line, char const * condition);
-void enable_debug(char const * tag);
-void disable_debug(char const * tag);
-bool is_debug_enabled(char const * tag);
-void invoke_debugger();
-bool has_violations();
-void enable_debug_dialog(bool flag);
+LEAN_EXPORT void notify_assertion_violation(char const * file_name, int line, char const * condition);
+LEAN_EXPORT void enable_debug(char const * tag);
+LEAN_EXPORT void disable_debug(char const * tag);
+LEAN_EXPORT bool is_debug_enabled(char const * tag);
+LEAN_EXPORT void invoke_debugger();
+LEAN_EXPORT bool has_violations();
+LEAN_EXPORT void enable_debug_dialog(bool flag);
 // LCOV_EXCL_START
 /** \brief Exception used to sign that unreachable code was reached */
 class unreachable_reached : public exception {
@@ -118,12 +49,5 @@ class unreachable_reached : public exception {
     virtual ~unreachable_reached() noexcept {}
     virtual char const * what() const noexcept { return "'unreachable' code was reached"; }
 };
-namespace debug {
-template<typename T> void display_var(char const * name, T const & value) {
-    // commented typeid(value).name() since the name is mangled
-    std::cerr << name << /* " : " << typeid(value).name() << */ " := "
-              << std::boolalpha << value << std::noboolalpha
-              << std::endl; }
-}
 // LCOV_EXCL_STOP
 }
diff --git a/src/runtime/exception.h b/src/runtime/exception.h
index ed4fb4fa3f18..0004494591da 100644
--- a/src/runtime/exception.h
+++ b/src/runtime/exception.h
@@ -8,11 +8,12 @@ Author: Leonardo de Moura
 #include <exception>
 #include <string>
 #include <memory>
+#include "lean/lean.h"
 
 namespace lean {
 class sstream;
 /** \brief Base class for all Lean exceptions */
-class throwable : public std::exception {
+class LEAN_EXPORT throwable : public std::exception {
 protected:
     std::string m_msg;
     throwable() {}
@@ -26,7 +27,7 @@ class throwable : public std::exception {
 
 /** \brief Base class for all Lean "logical" exceptions, that is, exceptions not related
     to resource constraints, and runtime errors */
-class exception : public throwable {
+class LEAN_EXPORT exception : public throwable {
 protected:
     exception() {}
 public:
@@ -36,14 +37,14 @@ class exception : public throwable {
 };
 
 /** \brief Exception used to sign that a computation was interrupted */
-class interrupted {
+class LEAN_EXPORT interrupted {
 public:
     interrupted() {}
     virtual ~interrupted() noexcept {}
     virtual char const * what() const noexcept { return "interrupted"; }
 };
 
-class stack_space_exception : public throwable {
+class LEAN_EXPORT stack_space_exception : public throwable {
     std::string m_msg;
     stack_space_exception(std::string const & msg):m_msg(msg) {}
 public:
@@ -51,7 +52,7 @@ class stack_space_exception : public throwable {
     virtual char const * what() const noexcept { return m_msg.c_str(); }
 };
 
-class memory_exception : public throwable {
+class LEAN_EXPORT memory_exception : public throwable {
     std::string m_msg;
     memory_exception(std::string const & msg):m_msg(msg) {}
 public:
@@ -59,7 +60,7 @@ class memory_exception : public throwable {
     virtual char const * what() const noexcept { return m_msg.c_str(); }
 };
 
-class heartbeat_exception : public throwable {
+class LEAN_EXPORT heartbeat_exception : public throwable {
 public:
     heartbeat_exception() {}
     virtual char const * what() const noexcept;
diff --git a/src/runtime/init_module.cpp b/src/runtime/init_module.cpp
index f562dca69814..8bf949d8bd5d 100644
--- a/src/runtime/init_module.cpp
+++ b/src/runtime/init_module.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "runtime/stack_overflow.h"
 #include "runtime/process.h"
 #include "runtime/mutex.h"
+#include "runtime/init_module.h"
 
 namespace lean {
 extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
diff --git a/src/runtime/init_module.h b/src/runtime/init_module.h
index b28dfb4cd233..bb80d361bf2b 100644
--- a/src/runtime/init_module.h
+++ b/src/runtime/init_module.h
@@ -5,8 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <lean/lean.h>
 
 namespace lean {
-void initialize_runtime_module();
-void finalize_runtime_module();
+LEAN_EXPORT void initialize_runtime_module();
+LEAN_EXPORT void finalize_runtime_module();
 }
diff --git a/src/runtime/interrupt.h b/src/runtime/interrupt.h
index 4746701f3111..ccc679319305 100644
--- a/src/runtime/interrupt.h
+++ b/src/runtime/interrupt.h
@@ -13,10 +13,10 @@ Author: Leonardo de Moura
 
 namespace lean {
 /** \brief Increment thread local counter for approximating elapsed time. */
-void inc_heartbeat();
+LEAN_EXPORT void inc_heartbeat();
 
 /** \brief Reset thread local counter for approximating elapsed time. */
-void reset_heartbeat();
+LEAN_EXPORT void reset_heartbeat();
 
 /* Update the current heartbeat */
 class scope_heartbeat : flet<size_t> {
@@ -30,9 +30,9 @@ class scope_heartbeat : flet<size_t> {
 
     This is a thread local value. The class lthread uses the
     maximum of the parent thread. */
-void set_max_heartbeat(size_t max);
-void set_max_heartbeat_thousands(unsigned max);
-size_t get_max_heartbeat();
+LEAN_EXPORT void set_max_heartbeat(size_t max);
+LEAN_EXPORT void set_max_heartbeat_thousands(unsigned max);
+LEAN_EXPORT size_t get_max_heartbeat();
 
 /* Update the thread local max heartbeat */
 class scope_max_heartbeat : flet<size_t> {
@@ -40,12 +40,12 @@ class scope_max_heartbeat : flet<size_t> {
     scope_max_heartbeat(size_t max);
 };
 
-void check_heartbeat();
+LEAN_EXPORT void check_heartbeat();
 
 /**
    \brief Throw an interrupted exception if the current task is marked cancelled.
 */
-void check_interrupted();
+LEAN_EXPORT void check_interrupted();
 
 /**
    \brief Check system resources: stack, memory, and (if `do_check_interrupted` is true) heartbeat
@@ -55,7 +55,7 @@ void check_interrupted();
    would not bring down the entire process as interruption (via heartbeat limit or flag) should not
    be a fatal error.
 */
-void check_system(char const * component_name, bool do_check_interrupted = false);
+LEAN_EXPORT void check_system(char const * component_name, bool do_check_interrupted = false);
 
 constexpr unsigned g_small_sleep = 10;
 
@@ -64,6 +64,6 @@ constexpr unsigned g_small_sleep = 10;
 
    \remark check_interrupted is invoked every \c step_ms milliseconds;
 */
-void sleep_for(unsigned ms, unsigned step_ms = g_small_sleep);
-inline void sleep_for(chrono::milliseconds const & ms) { sleep_for(ms.count(), 10); }
+LEAN_EXPORT void sleep_for(unsigned ms, unsigned step_ms = g_small_sleep);
+LEAN_EXPORT inline void sleep_for(chrono::milliseconds const & ms) { sleep_for(ms.count(), 10); }
 }
diff --git a/src/runtime/io.h b/src/runtime/io.h
index 6fe6f2a1bce5..783f2fc08bbd 100644
--- a/src/runtime/io.h
+++ b/src/runtime/io.h
@@ -12,10 +12,10 @@ Author: Leonardo de Moura
 namespace lean {
 inline lean_obj_res io_result_mk_ok(lean_obj_arg a) { return lean_io_result_mk_ok(a); }
 inline lean_obj_res io_result_mk_error(lean_obj_arg e) { return lean_io_result_mk_error(e); }
-lean_obj_res io_result_mk_error(char const * msg);
-lean_obj_res io_result_mk_error(std::string const & msg);
+LEAN_EXPORT lean_obj_res io_result_mk_error(char const * msg);
+LEAN_EXPORT lean_obj_res io_result_mk_error(std::string const & msg);
 inline lean_obj_res decode_io_error(int errnum, b_lean_obj_arg fname) { return lean_decode_io_error(errnum, fname); }
-lean_obj_res io_wrap_handle(FILE * hfile);
+LEAN_EXPORT lean_obj_res io_wrap_handle(FILE * hfile);
 void initialize_io();
 void finalize_io();
 }
diff --git a/src/runtime/load_dynlib.h b/src/runtime/load_dynlib.h
index 5f58fd9d6655..e294daf9375d 100644
--- a/src/runtime/load_dynlib.h
+++ b/src/runtime/load_dynlib.h
@@ -8,5 +8,5 @@ Author: Mac Malone
 #include <string>
 
 namespace lean {
-void load_dynlib(std::string path);
+LEAN_EXPORT void load_dynlib(std::string path);
 }
diff --git a/src/runtime/memory.h b/src/runtime/memory.h
index e57f757f3690..e2d775f5946d 100644
--- a/src/runtime/memory.h
+++ b/src/runtime/memory.h
@@ -6,12 +6,13 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <cstdlib>
+#include <lean/lean.h>
 
 namespace lean {
 /** \brief Set maximum amount of memory in bytes */
-void set_max_memory(size_t max);
+LEAN_EXPORT void set_max_memory(size_t max);
 /** \brief Set maximum amount of memory in megabytes */
-void set_max_memory_megabyte(unsigned max);
-void check_memory(char const * component_name);
-size_t get_allocated_memory();
+LEAN_EXPORT void set_max_memory_megabyte(unsigned max);
+LEAN_EXPORT void check_memory(char const * component_name);
+LEAN_EXPORT size_t get_allocated_memory();
 }
diff --git a/src/runtime/mpz.h b/src/runtime/mpz.h
index e0680916f4af..68127c4606fd 100644
--- a/src/runtime/mpz.h
+++ b/src/runtime/mpz.h
@@ -21,7 +21,7 @@ Author: Leonardo de Moura
 namespace lean {
 
 /** \brief Wrapper for GMP integers */
-class mpz {
+class LEAN_EXPORT mpz {
     friend class object_compactor;
     friend class compacted_region;
 #ifdef LEAN_USE_GMP
@@ -146,9 +146,9 @@ class mpz {
     mpz & operator=(unsigned int v);
     mpz & operator=(int v);
 
-    friend int cmp(mpz const & a, mpz const & b);
-    friend int cmp(mpz const & a, unsigned b);
-    friend int cmp(mpz const & a, int b);
+    LEAN_EXPORT friend int cmp(mpz const & a, mpz const & b);
+    LEAN_EXPORT friend int cmp(mpz const & a, unsigned b);
+    LEAN_EXPORT friend int cmp(mpz const & a, int b);
 
     friend bool operator<(mpz const & a, mpz const & b) { return cmp(a, b) < 0; }
     friend bool operator<(mpz const & a, unsigned b) { return cmp(a, b) < 0; }
@@ -284,7 +284,7 @@ class mpz {
     friend void gcd(mpz & g, mpz const & a, mpz const & b);
     friend mpz gcd(mpz const & a, mpz const & b) { mpz r; gcd(r, a, b); return r; }
 
-    friend std::ostream & operator<<(std::ostream & out, mpz const & v);
+    LEAN_EXPORT friend std::ostream & operator<<(std::ostream & out, mpz const & v);
 
     std::string to_string() const;
 };
diff --git a/src/runtime/object.h b/src/runtime/object.h
index f93ccd621e8c..04f13fe1b642 100644
--- a/src/runtime/object.h
+++ b/src/runtime/object.h
@@ -99,7 +99,6 @@ inline void cnstr_set_float(b_obj_arg o, unsigned offset, double v) { lean_ctor_
 // =======================================
 // Closures
 
-void free_closure_obj(object * o);
 inline void * closure_fun(object * o) { return lean_closure_fun(o); }
 inline unsigned closure_arity(object * o) { return lean_closure_arity(o); }
 inline unsigned closure_num_fixed(object * o) { return lean_closure_num_fixed(o); }
@@ -178,7 +177,7 @@ inline object* apply_m(object* f, unsigned n, object** args) { return lean_apply
 // =======================================
 // MPZ
 
-object * alloc_mpz(mpz const &);
+LEAN_EXPORT object * alloc_mpz(mpz const &);
 inline mpz_object * to_mpz(object * o) { lean_assert(is_mpz(o)); return (mpz_object*)o; }
 
 // =======================================
@@ -187,7 +186,7 @@ inline mpz_object * to_mpz(object * o) { lean_assert(is_mpz(o)); return (mpz_obj
 inline size_t array_capacity(object * o) { return lean_array_capacity(o); }
 inline object ** array_cptr(object * o) { return lean_array_cptr(o); }
 inline obj_res alloc_array(size_t size, size_t capacity) { return lean_alloc_array(size, capacity); }
-object * array_mk_empty();
+LEAN_EXPORT object * array_mk_empty();
 inline size_t array_size(b_obj_arg o) { return lean_array_size(o); }
 inline void array_set_size(u_obj_arg o, size_t sz) { lean_array_set_size(o, sz); }
 inline b_obj_res array_get(b_obj_arg o, size_t i) { return lean_array_get_core(o, i); }
@@ -239,8 +238,8 @@ inline size_t string_capacity(object * o) { return lean_string_capacity(o); }
 inline uint32 char_default_value() { return lean_char_default_value(); }
 inline obj_res alloc_string(size_t size, size_t capacity, size_t len) { return lean_alloc_string(size, capacity, len); }
 inline obj_res mk_string(char const * s) { return lean_mk_string(s); }
-obj_res mk_string(std::string const & s);
-std::string string_to_std(b_obj_arg o);
+LEAN_EXPORT obj_res mk_string(std::string const & s);
+LEAN_EXPORT std::string string_to_std(b_obj_arg o);
 inline char const * string_cstr(b_obj_arg o) { return lean_string_cstr(o); }
 inline size_t string_size(b_obj_arg o) { return lean_string_size(o); }
 inline size_t string_len(b_obj_arg o) { return lean_string_len(o); }
@@ -257,7 +256,7 @@ inline uint8 string_utf8_at_end(b_obj_arg s, b_obj_arg i) { return lean_string_u
 inline obj_res string_utf8_extract(b_obj_arg s, b_obj_arg b, b_obj_arg e) { return lean_string_utf8_extract(s, b, e); }
 inline obj_res string_utf8_byte_size(b_lean_obj_arg s) { return lean_string_utf8_byte_size(s); }
 inline bool string_eq(b_obj_arg s1, b_obj_arg s2) { return lean_string_eq(s1, s2); }
-bool string_eq(b_obj_arg s1, char const * s2);
+LEAN_EXPORT bool string_eq(b_obj_arg s1, char const * s2);
 inline bool string_ne(b_obj_arg s1, b_obj_arg s2) { return lean_string_ne(s1, s2); }
 inline bool string_lt(b_obj_arg s1, b_obj_arg s2) { return lean_string_lt(s1, s2); }
 inline uint8 string_dec_eq(b_obj_arg s1, b_obj_arg s2) { return string_eq(s1, s2); }
@@ -275,7 +274,7 @@ inline obj_res thunk_get_own(b_obj_arg t) { return lean_thunk_get_own(t); }
 // =======================================
 // Tasks
 
-class scoped_task_manager {
+class LEAN_EXPORT scoped_task_manager {
 public:
     scoped_task_manager(unsigned num_workers);
     ~scoped_task_manager();
@@ -309,7 +308,7 @@ inline obj_res mk_option_some(obj_arg v) { obj_res r = alloc_cnstr(1, 1, 0); cns
 // Natural numbers
 
 inline mpz const & mpz_value(b_obj_arg o) { return to_mpz(o)->m_value; }
-object * mpz_to_nat_core(mpz const & m);
+LEAN_EXPORT object * mpz_to_nat_core(mpz const & m);
 inline object * mk_nat_obj_core(mpz const & m) { return mpz_to_nat_core(m); }
 inline obj_res mk_nat_obj(mpz const & m) {
     if (m.is_size_t() && m.get_size_t() <= LEAN_MAX_SMALL_NAT)
@@ -341,7 +340,7 @@ inline obj_res nat_lxor(b_obj_arg a1, b_obj_arg a2) { return lean_nat_lxor(a1, a
 
 // =======================================
 // Integers
-object * mk_int_obj_core(mpz const & m);
+LEAN_EXPORT object * mk_int_obj_core(mpz const & m);
 inline obj_res mk_int_obj(mpz const & m) {
     if (m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT)
         return mk_int_obj_core(m);
@@ -463,7 +462,7 @@ inline b_obj_res io_result_get_value(b_obj_arg r) { return lean_io_result_get_va
 inline b_obj_res io_result_get_error(b_obj_arg r) { return lean_io_result_get_error(r); }
 inline void io_result_show_error(b_obj_arg r) { return lean_io_result_show_error(r); }
 inline void io_mark_end_initialization() { return lean_io_mark_end_initialization(); }
-void io_eprintln(obj_arg s);
+LEAN_EXPORT void io_eprintln(obj_arg s);
 
 // =======================================
 // ST ref primitives
diff --git a/src/runtime/object_ref.h b/src/runtime/object_ref.h
index e00a2b95eb5f..c0209676f329 100644
--- a/src/runtime/object_ref.h
+++ b/src/runtime/object_ref.h
@@ -42,7 +42,7 @@ class object_ref {
 };
 
 /* Remark: this function doesn't increase the reference counter of objs */
-object_ref mk_cnstr(unsigned tag, unsigned num_objs, object ** objs, unsigned scalar_sz = 0);
+LEAN_EXPORT object_ref mk_cnstr(unsigned tag, unsigned num_objs, object ** objs, unsigned scalar_sz = 0);
 inline object_ref mk_cnstr(unsigned tag, object * o, unsigned scalar_sz = 0) { return mk_cnstr(tag, 1, &o, scalar_sz); }
 inline object_ref mk_cnstr(unsigned tag, object * o1, object * o2, unsigned scalar_sz = 0) {
     object * os[2] = { o1, o2 };
diff --git a/src/runtime/stackinfo.cpp b/src/runtime/stackinfo.cpp
index 48f4c7a3946d..b27c10cdaeb0 100644
--- a/src/runtime/stackinfo.cpp
+++ b/src/runtime/stackinfo.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include "runtime/thread.h"
 #include "runtime/exception.h"
+#include "runtime/stackinfo.h"
 
 #if !defined(LEAN_USE_SPLIT_STACK)
 #if defined(LEAN_WINDOWS)
@@ -29,7 +30,7 @@ void throw_get_stack_size_failed() {
 }
 
 #if defined(LEAN_WINDOWS)
-size_t get_stack_size(int main) {
+size_t get_stack_size(bool main) {
     if (main) {
         return LEAN_WIN_STACK_SIZE;
     } else {
@@ -37,7 +38,7 @@ size_t get_stack_size(int main) {
     }
 }
 #elif defined (__APPLE__)
-size_t get_stack_size(int main) {
+size_t get_stack_size(bool main) {
     if (main) {
         // Retrieve stack size of the main thread.
         struct rlimit curr;
@@ -50,7 +51,7 @@ size_t get_stack_size(int main) {
     }
 }
 #elif defined(LEAN_EMSCRIPTEN)
-size_t get_stack_size(int main) {
+size_t get_stack_size(bool main) {
     if (main) {
         return emscripten_stack_get_end() - emscripten_stack_get_base();
     } else {
@@ -58,7 +59,7 @@ size_t get_stack_size(int main) {
     }
 }
 #else
-size_t get_stack_size(int main) {
+size_t get_stack_size(bool main) {
     if (main) {
         // Retrieve stack size of the main thread.
         struct rlimit curr;
diff --git a/src/runtime/stackinfo.h b/src/runtime/stackinfo.h
index 8469406bccab..0181a530d28a 100644
--- a/src/runtime/stackinfo.h
+++ b/src/runtime/stackinfo.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <cstdlib>
+#include <lean/lean.h>
 
 namespace lean {
 #if defined(LEAN_USE_SPLIT_STACK)
@@ -16,16 +17,17 @@ inline void save_stack_info(bool = true) {}
 inline size_t get_used_stack_size() { return 0; }
 inline size_t get_available_stack_size() { return 8192*1024; }
 #else
-size_t get_stack_size(bool main);
-void save_stack_info(bool main = true);
-size_t get_used_stack_size();
-size_t get_available_stack_size();
+LEAN_EXPORT size_t get_stack_size(bool main);
+LEAN_EXPORT void save_stack_info(bool main = true);
+LEAN_EXPORT size_t get_used_stack_size();
+LEAN_EXPORT size_t get_available_stack_size();
 /**
    \brief Throw an exception if the amount of available stack space is low.
 
    \remark The optional argument \c component_name is used to inform the
    user which module is the potential offender.
 */
-void check_stack(char const * component_name);
+LEAN_EXPORT void check_stack(char const * component_name);
 #endif
+
 }
diff --git a/src/runtime/thread.h b/src/runtime/thread.h
index cc1b14ec0060..decebaeae0e8 100644
--- a/src/runtime/thread.h
+++ b/src/runtime/thread.h
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <chrono>
 #include <functional>
+#include <lean/lean.h>
 
 #ifndef LEAN_STACK_BUFFER_SPACE
 #define LEAN_STACK_BUFFER_SPACE 128*1024  // 128 Kb
@@ -50,7 +51,7 @@ namespace this_thread = std::this_thread;
 inline unsigned hardware_concurrency() { return std::thread::hardware_concurrency(); }
 /** Simple thread class that allows us to set the thread stack size.
     We implement it using pthreads on OSX/Linux and WinThreads on Windows. */
-class lthread {
+class LEAN_EXPORT lthread {
     static size_t m_thread_stack_size;
     struct imp;
     std::unique_ptr<imp> m_imp;
@@ -220,13 +221,13 @@ void initialize_thread();
 void finalize_thread();
 
 typedef void (*thread_finalizer)(void *); // NOLINT
-void register_post_thread_finalizer(thread_finalizer fn, void * p);
-void register_thread_finalizer(thread_finalizer fn, void * p);
-void run_thread_finalizers();
-void run_post_thread_finalizers();
-void delete_thread_finalizer_manager();
+LEAN_EXPORT void register_post_thread_finalizer(thread_finalizer fn, void * p);
+LEAN_EXPORT void register_thread_finalizer(thread_finalizer fn, void * p);
+LEAN_EXPORT void run_thread_finalizers();
+LEAN_EXPORT void run_post_thread_finalizers();
+LEAN_EXPORT void delete_thread_finalizer_manager();
 
-bool in_thread_finalization();
+LEAN_EXPORT bool in_thread_finalization();
 
 /**
     \brief Add \c fn to the list of functions used to reset thread local storage.
@@ -237,7 +238,7 @@ bool in_thread_finalization();
     contains cached data that may not be valid anymore.
 
     \see reset_thread_local */
-void register_thread_local_reset_fn(std::function<void()> fn);
+LEAN_EXPORT void register_thread_local_reset_fn(std::function<void()> fn);
 
 /**
    \brief Reset thread local storage that contains cached
@@ -245,5 +246,5 @@ void register_thread_local_reset_fn(std::function<void()> fn);
 
    We invoke this function before processing a command
    and before executing a task. */
-void reset_thread_local();
+LEAN_EXPORT void reset_thread_local();
 }
diff --git a/src/runtime/utf8.h b/src/runtime/utf8.h
index fdbcbff52005..3eeb6c96ff82 100644
--- a/src/runtime/utf8.h
+++ b/src/runtime/utf8.h
@@ -8,24 +8,25 @@ Author: Leonardo de Moura
 #include <vector>
 #include <string>
 #include "runtime/optional.h"
+#include "lean/lean.h"
 
 namespace lean {
 using uchar = unsigned char;
 
-bool is_utf8_next(unsigned char c);
-unsigned get_utf8_size(unsigned char c);
+LEAN_EXPORT bool is_utf8_next(unsigned char c);
+LEAN_EXPORT unsigned get_utf8_size(unsigned char c);
 /* Return the length of the null terminated string encoded using UTF8 */
-size_t utf8_strlen(char const * str);
+LEAN_EXPORT size_t utf8_strlen(char const * str);
 /* Return the length of the string `str` encoded using UTF8.
    `str` may contain null characters. */
-size_t utf8_strlen(std::string const & str);
+LEAN_EXPORT size_t utf8_strlen(std::string const & str);
 /* Return the length of the string `str` encoded using UTF8.
    `str` may contain null characters. */
-size_t utf8_strlen(char const * str, size_t sz);
-optional<size_t> utf8_char_pos(char const * str, size_t char_idx);
-char const * get_utf8_last_char(char const * str);
-std::string utf8_trim(std::string const & s);
-unsigned utf8_to_unicode(uchar const * begin, uchar const * end);
+LEAN_EXPORT size_t utf8_strlen(char const * str, size_t sz);
+LEAN_EXPORT optional<size_t> utf8_char_pos(char const * str, size_t char_idx);
+LEAN_EXPORT char const * get_utf8_last_char(char const * str);
+LEAN_EXPORT std::string utf8_trim(std::string const & s);
+LEAN_EXPORT unsigned utf8_to_unicode(uchar const * begin, uchar const * end);
 inline unsigned utf8_to_unicode(char const * begin, char const * end) {
     return utf8_to_unicode(reinterpret_cast<uchar const *>(begin),
                            reinterpret_cast<uchar const *>(end));
@@ -34,20 +35,20 @@ inline unsigned utf8_to_unicode(char const * begin, char const * end) {
 /* If `c` is the first byte of an utf-8 encoded unicode scalar value,
    then return `some(n)` where `n` is the number of bytes needed to encode
    the unicode scalar value. Otherwise, return `none` */
-optional<unsigned> get_utf8_first_byte_opt(unsigned char c);
+LEAN_EXPORT optional<unsigned> get_utf8_first_byte_opt(unsigned char c);
 
 /* "Read" next unicode character starting at position i in a string using UTF-8 encoding.
    Return the unicode character and update i. */
-unsigned next_utf8(std::string const & str, size_t & i);
-unsigned next_utf8(char const * str, size_t size, size_t & i);
+LEAN_EXPORT unsigned next_utf8(std::string const & str, size_t & i);
+LEAN_EXPORT unsigned next_utf8(char const * str, size_t size, size_t & i);
 
 /* Decode a UTF-8 encoded string `str` into unicode scalar values */
-void utf8_decode(std::string const & str, std::vector<unsigned> & out);
+LEAN_EXPORT void utf8_decode(std::string const & str, std::vector<unsigned> & out);
 
 /* Push a unicode scalar value into a utf-8 encoded string */
-void push_unicode_scalar(std::string & s, unsigned code);
+LEAN_EXPORT void push_unicode_scalar(std::string & s, unsigned code);
 
 /* Store unicode scalar value at `d`, `d` must point to memory with enough space to store `c`.
    Return the number of bytes consumed. */
-unsigned push_unicode_scalar(char * d, unsigned code);
+LEAN_EXPORT unsigned push_unicode_scalar(char * d, unsigned code);
 }
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 85d0b9d27df4..d2f6f7ddbb26 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -42,11 +42,19 @@ Lean: Init
 # the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt
 
 # we specify the precise file names here to avoid rebuilds
-${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${LIB}/lean/libLean.a ${LIB}/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a
+${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a
 	@echo "[    ] Building $@"
 # on Windows, must remove file before writing a new one (since the old one may be in use)
 	@rm -f $@
-	"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS}
+	"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${INIT_SHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
+
+Init_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
+
+${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/lean/libLean.a ${LIB}/lean/libleancpp.a
+	@echo "[    ] Building $@"
+# on Windows, must remove file before writing a new one (since the old one may be in use)
+	@rm -f $@
+	"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
 
 leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
 
@@ -54,7 +62,7 @@ Lake:
 # lake is in its own subdirectory, so must adjust relative paths...
 	+"${LEAN_BIN}/leanmake" -C lake bin lib PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean"
 
-${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} $(LEAN_SHELL)
+${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} $(LEAN_SHELL)
 	@echo "[    ] Building $@"
 # on Windows, must remove file before writing a new one (since the old one may be in use)
 	@rm -f $@
diff --git a/tests/compiler/foreign/Makefile b/tests/compiler/foreign/Makefile
index f73add9b1377..7c836f30047d 100644
--- a/tests/compiler/foreign/Makefile
+++ b/tests/compiler/foreign/Makefile
@@ -27,7 +27,7 @@ $(BIN_OUT)/testcpp.so: $(CPP_OBJS) | $(BIN_OUT)
 	$(CXX) -shared -o $@ $^ `leanc -shared --print-ldflags`
 
 $(BIN_OUT)/test: $(LIB_OUT)/libMain.a $(CPP_OBJS) | $(BIN_OUT)
-	$(CXX) -o $@ $^ `leanc -shared --print-ldflags` -lleanshared $(TEST_SHARED_LINK_FLAGS)
+	$(CXX) -o $@ $^ `leanc -shared --print-ldflags` -lInit_shared -lleanshared $(TEST_SHARED_LINK_FLAGS)
 
 run_test: $(BIN_OUT)/test
 	$^