diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 31f6a34936..03a97b20eb 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -38,7 +38,7 @@ jobs:
           - name: Linux fsanitize
             os: ubuntu-latest
             # turn off custom allocator to make LSAN do its magic
-            CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined -DSMALL_ALLOCATOR=OFF
+            CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_C_FLAGS=-fsanitize=address,undefined -DSMALL_ALLOCATOR=OFF
           - name: macOS
             os: macos-latest
             release: true
diff --git a/flake.nix b/flake.nix
index 861bdefa60..2c0ccd4fb6 100644
--- a/flake.nix
+++ b/flake.nix
@@ -34,10 +34,10 @@
       packages = lean-packages // rec {
         debug = lean-packages.override { debug = true; };
         stage0debug = lean-packages.override { stage0debug = true; };
-        sanitized = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined" "-DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined" "-DSMALL_ALLOCATOR=OFF" ]; };
+        sanitized = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined" "-DLEANC_EXTRA_C_FLAGS=-fsanitize=address,undefined" "-DSMALL_ALLOCATOR=OFF" ]; };
         sandebug = sanitized.override { debug = true; };
         tsan = lean-packages.override {
-          extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
+          extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_C_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
           stage0 = (lean-packages.override {
             # Compressed headers currently trigger data race reports in tsan.
             # Turn them off for stage 0 as well so stage 1 can read its own stdlib.
diff --git a/script/update-stage0 b/script/update-stage0
index b483a6fd09..5c24b22338 100755
--- a/script/update-stage0
+++ b/script/update-stage0
@@ -2,7 +2,11 @@
 set -euo pipefail
 
 rm -r stage0 || true
-mkdir -p stage0/
+mkdir -p stage0/stdlib/
+cat <<EOF >> stage0/stdlib/CMakeLists.txt
+set(CMAKE_C_COMPILER_LAUNCHER "env;LEAN_CXX=\${CMAKE_CXX_COMPILER_LAUNCHER} \${CMAKE_CXX_COMPILER}")
+set(CMAKE_C_COMPILER "\${CMAKE_BINARY_DIR}/bin/leanc")
+EOF
 for pkg in Init Std Lean; do
     # ensure deterministic ordering
     c_files="$pkg.c $(cd src; find $pkg -name '*.lean' | sed s/.lean/.c/ | LC_ALL=C sort | tr '\n' ' ')"
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6a62621151..fcb6b144b8 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -72,6 +72,7 @@ set(MINGW_LOCAL_DIR       "C:/msys64/mingw64/bin"      CACHE STRING "where to fi
 
 if ("${FAKE_FREE}" MATCHES "ON")
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_FAKE_FREE")
+  set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_FAKE_FREE")
 endif()
 
 if ("${LAZY_RC}" MATCHES "ON")
@@ -112,10 +113,12 @@ endif()
 
 if ("${RUNTIME_STATS}" MATCHES "ON")
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_RUNTIME_STATS")
+  set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_RUNTIME_STATS")
 endif()
 
 if (NOT("${CHECK_OLEAN_VERSION}" MATCHES "ON"))
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_IGNORE_OLEAN_VERSION")
+  set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_IGNORE_OLEAN_VERSION")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
@@ -132,10 +135,8 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     # > The simple and safe thing is to pass all -s flags at both compile and link time.
     set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -s DISABLE_EXCEPTION_CATCHING=0 -s MAIN_MODULE=1 -fexceptions")
     set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}")
+    set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}")
     set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS}")
-    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${EMSCRIPTEN_SETTINGS}")
-    set(LEANC_OPTS "${LEANC_OPTS} ${EMSCRIPTEN_SETTINGS}")
-    set(LEANC_GMP "${GMP_INSTALL_PREFIX}/lib/libgmp.a")
 endif()
 if (CMAKE_CROSSCOMPILING_EMULATOR)
   # emscripten likes to quote "node"
@@ -157,7 +158,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
     set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} /STACK:${LEAN_WIN_STACK_SIZE}")
   else()
     set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -Wl,--stack,${LEAN_WIN_STACK_SIZE}")
-    set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -Wl,--stack,${LEAN_WIN_STACK_SIZE}")
+    set(LEANC_EXTRA_LINKER_FLAGS "${LEANC_EXTRA_LINKER_FLAGS} -Wl,--stack,${LEAN_WIN_STACK_SIZE}")
     set(EXTRA_UTIL_LIBS ${EXTRA_UTIL_LIBS} -lpsapi)
   endif()
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_WINDOWS -D LEAN_WIN_STACK_SIZE=${LEAN_WIN_STACK_SIZE}")
@@ -170,14 +171,15 @@ endif ()
 
 if(NOT MULTI_THREAD)
   message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
-  set(LEANC_OPTS "${LEANC_OPTS} -U LEAN_MULTI_THREAD")
   set(AUTO_THREAD_FINALIZATION OFF)
 else()
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_MULTI_THREAD")
+  set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_MULTI_THREAD")
 endif()
 
 if(AUTO_THREAD_FINALIZATION AND NOT MSVC)
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_AUTO_THREAD_FINALIZATION")
+  set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_AUTO_THREAD_FINALIZATION")
 endif()
 
 if(LLVM)
@@ -189,6 +191,7 @@ if(LLVM)
 
   include_directories(${LLVM_INCLUDE_DIRS})
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_LLVM")
+  set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -D LEAN_LLVM")
 
   # Find the libraries that correspond to the LLVM components
   #   that we wish to use and define llvm_libs
@@ -280,6 +283,7 @@ endif ()
 
 if ("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
   include_directories(${GMP_INSTALL_PREFIX}/include)
+  set(GMP_LIBRARIES "${GMP_INSTALL_PREFIX}/lib/libgmp.a")
 else()
   # GMP
   find_package(GMP 5.0.5 REQUIRED)
@@ -312,6 +316,8 @@ include_directories(${CMAKE_BINARY_DIR}/include)
 # the linker flags necessary on other platforms.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean")
+elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
+  set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean -lnodefs.js")
 else()
   # `-pie` defaulting is not consistent on Linux distributions, so let's default to off
   set(LEANC_STATIC_LINKER_FLAGS "-no-pie -Wl,--start-group -lleancpp -lInit -lStd -lLean -Wl,--end-group")
@@ -333,7 +339,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   set(LEAN_EXTRA_MAKE_OPTS "-Dcompiler.extract_closed=false")
 else()
   set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -rdynamic")
-  set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -ldl")
+  set(LEANC_EXTRA_LINKER_FLAGS "${LEANC_EXTRA_LINKER_FLAGS} -ldl")
 endif()
 
 # Allow `lean` symbols in plugins without linking directly against it. If we linked against the
@@ -343,13 +349,13 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   # import library created by the `lean` target
   set(LEANC_SHARED_LINKER_FLAGS "$bindir/lean.exe.a")
 elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
-  set(LEANC_SHARED_LINKER_FLAGS "${LEANC_EXTRA_FLAGS} -Wl,-undefined,dynamic_lookup")
+  set(LEANC_SHARED_LINKER_FLAGS "-Wl,-undefined,dynamic_lookup")
 endif()
 # Linux ignores undefined symbols in shared libraries by default
 
 if(MULTI_THREAD AND NOT MSVC AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")))
     set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
-    set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -pthread")
+    set(LEANC_EXTRA_C_FLAGS "${LEANC_EXTRA_C_FLAGS} -pthread")
 endif()
 
 # Git HASH
diff --git a/src/bin/leanc.in b/src/bin/leanc.in
index bf5a33fb41..8748746dbb 100755
--- a/src/bin/leanc.in
+++ b/src/bin/leanc.in
@@ -16,8 +16,8 @@
 set -e
 bindir=$(dirname $0)
 
-cflags=("-I$bindir/../include")
-ldflags=("-L$bindir/../lib/lean" "${LEANC_GMP:--lgmp}" @LEANC_EXTRA_FLAGS@)
+cflags=("-I$bindir/../include" @LEANC_EXTRA_C_FLAGS@)
+ldflags=("-L$bindir/../lib/lean" "${LEANC_GMP:--lgmp}" @LEANC_EXTRA_LINKER_FLAGS@)
 ldflags_ext=(@LEANC_STATIC_LINKER_FLAGS@)
 args=("$@")
 for arg in "$@"; do
@@ -25,10 +25,10 @@ for arg in "$@"; do
     [[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@) && args=("-x" "c" "$@" "-x" "none")
     # Note the `-x c` for treating all input as C code
     [[ $arg == "-c" ]] && ldflags=() && ldflags_ext=() && args=("-x" "c" "$@" "-x" "none")
-    [[ $arg == "-print-cflags" ]] && echo "${cflags[@]} ${cflags_ext[@]}" && exit
-    [[ $arg == "-print-ldflags" ]] && echo "${ldflags_ext[@]} ${ldflags[@]}" && exit
+    [[ $arg == "-print-cflags" ]] && echo "${cflags[@]}" && exit
+    [[ $arg == "-print-ldflags" ]] && echo "${cflags[@]} ${ldflags_ext[@]} ${ldflags[@]}" && exit
 done
 
 [ -n "$LEAN_CXX" ] || LEAN_CXX=c++
 
-$LEAN_CXX -D LEAN_MULTI_THREAD "${cflags[@]}" "${args[@]}" "${ldflags_ext[@]}" "${ldflags[@]}" -Wno-unused-command-line-argument
+$LEAN_CXX "${cflags[@]}" "${args[@]}" "${ldflags_ext[@]}" "${ldflags[@]}" -Wno-unused-command-line-argument
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index aeee171b97..765a02b07c 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -1,16 +1,12 @@
-if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  add_executable(lean lean.cpp)
-  set_target_properties(lean PROPERTIES
-    RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin/")
-  target_link_libraries(lean Init Std Lean leancpp "${GMP_INSTALL_PREFIX}/lib/libgmp.a" "-lnodefs.js")
-else ()
-  add_library(shell OBJECT lean.cpp)
-  add_custom_command(OUTPUT ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}
-    COMMAND sh -c "LEANC_GMP=${GMP_LIBRARIES} ${CMAKE_BINARY_DIR}/bin/leanc -x none ${CMAKE_EXE_LINKER_FLAGS} $<TARGET_OBJECTS:shell> -o ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"
-    DEPENDS Init Std Lean leancpp shell)
-  add_custom_target(lean ALL
-    DEPENDS ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX})
-endif ()
+add_library(shell OBJECT lean.cpp)
+
+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 ${CMAKE_EXE_LINKER_FLAGS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}  $<TARGET_OBJECTS:shell> -o ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"
+  DEPENDS Init Std Lean leancpp shell)
+
+add_custom_target(lean ALL
+  DEPENDS ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX})
 
 install(FILES ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}
   DESTINATION bin
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index d4a5febf6d..2d87c4acd9 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -16,7 +16,6 @@ LEANMAKE_OPTS=\
 	BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
 	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
 	LEANC_OPTS+="${LEANC_OPTS}"\
-	LEANC_GMP="${LEANC_GMP}"\
 	LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\
 	LEAN_AR="${CMAKE_AR}"\
 	MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\