diff --git a/bin/leanc.in b/bin/leanc.in
index b76c697c5d..0f77ca10f4 100644
--- a/bin/leanc.in
+++ b/bin/leanc.in
@@ -16,4 +16,4 @@ for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do
     fi
 done
 [ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"
-$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD -pthread -fPIC "-I$bindir/../src" "$@" "-L$bindir" -ldl -Wl,-Bstatic -lleanstatic -lgmp @LEANC_EXTRA_LIBS@ -static-libgcc -static-libstdc++ -Wl,-Bdynamic -Wno-unused-command-line-argument
+$LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD -pthread -fPIC "-I$bindir/../src" "$@" "-L$bindir" -ldl -Wl,-Bstatic -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_LIBS@ -static-libgcc -static-libstdc++ -Wl,-Bdynamic -Wno-unused-command-line-argument
diff --git a/library/Makefile.in b/library/Makefile.in
index cfe9cf4c29..b14a814ff9 100644
--- a/library/Makefile.in
+++ b/library/Makefile.in
@@ -34,16 +34,17 @@ $(STAGE1_DIR)/%.cpp: %.lean %.olean
 	@mkdir -p $(@D)
 	$(LEAN) $(OPTS) --cpp=$@ $<
 
-$(STAGE1_DIR)/CMakeLists.txt: $(CPPS)
-	echo "add_library (cpp_stage1 OBJECT $(CPPS_CORE))" > $(STAGE1_DIR)/CMakeLists.txt
+$(STAGE1_DIR)/%.o: $(STAGE1_DIR)/%.cpp
+	../bin/leanc -c -o $@ $< -O3
 
-export-stage1: $(STAGE1_DIR)/CMakeLists.txt
+$(STAGE1_DIR)/libleanstdlib.a: $(patsubst %.cpp,%.o,$(CPPS))
+	@ar rcs $@ $^
 
 update-stage0:
 	rm -r $(STAGE0_DIR)/init
 	cp -R $(STAGE1_DIR)/init $(STAGE0_DIR)/init
 	echo "add_library (boot OBJECT $(CPPS_CORE))" > $(STAGE0_DIR)/CMakeLists.txt
 
-.PRECIOUS: %.depend
+.PRECIOUS: %.depend $(STAGE1_DIR)/%.cpp
 
 include $(DEPS)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d85755e6ce..b47a242061 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -457,31 +457,20 @@ endif()
 add_library(leanstatic_stage0 ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS} $<TARGET_OBJECTS:boot>)
 target_link_libraries(leanstatic_stage0 ${EXTRA_LIBS})
 
-if(STAGE1)
-  add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS} $<TARGET_OBJECTS:cpp_stage1>)
-  target_link_libraries(leanstatic ${EXTRA_LIBS})
-else()
-  # Build `leanstatic` after `export-stage1`, triggering a CMake re-run after (potentially) updating
-  # `src/stage1/CMakeLists.txt`
-  add_custom_target(boot_leanstatic
-    # '-G Ninja' complains otherwise
-    BYPRODUCTS libleanstatic.a
-    WORKING_DIRECTORY "${CMAKE_BINARY_DIR}"
-    COMMAND "${CMAKE_COMMAND}" "${CMAKE_SOURCE_DIR}" -DSTAGE1=ON
-    COMMAND "${CMAKE_COMMAND}" --build . --target leanstatic
-    COMMAND "${CMAKE_COMMAND}" "${CMAKE_SOURCE_DIR}" -DSTAGE1=OFF
-    DEPENDS export-stage1)
-  # import the output from the nested CMake run
-  add_library(leanstatic ${LEAN_LIBRARY_TYPE} IMPORTED)
-  set_target_properties(leanstatic PROPERTIES
-    IMPORTED_LOCATION "${CMAKE_CURRENT_BINARY_DIR}/libleanstatic.a"
-    INTERFACE_LINK_LIBRARIES "${EXTRA_LIBS}")
-  add_dependencies(leanstatic boot_leanstatic)
-endif()
+add_custom_target(build_leanstdlib
+  # '-G Ninja' complains otherwise
+  BYPRODUCTS "${LEAN_SOURCE_DIR}/stage1/libleanstdlib.a"
+  WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
+  COMMAND make -j8 ../src/stage1/libleanstdlib.a "LEAN=$<TARGET_FILE:lean_stage0>"
+  DEPENDS lean_stage0)
+
+add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS})
+target_link_libraries(leanstatic "${LEAN_SOURCE_DIR}/stage1/libleanstdlib.a" ${EXTRA_LIBS})
+add_dependencies(leanstatic build_leanstdlib)
 
 ADD_CUSTOM_TARGET(bin_lib ALL
    COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin"
-   COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "${CMAKE_CURRENT_BINARY_DIR}/libleanstatic*" "${LEAN_SOURCE_DIR}/../bin"
+   COMMAND "${CMAKE_COMMAND}" -E copy ${COPY_LIBS} "${LEAN_SOURCE_DIR}/stage1/libleanstdlib*" "${CMAKE_CURRENT_BINARY_DIR}/libleanstatic*" "${LEAN_SOURCE_DIR}/../bin"
    DEPENDS leanstatic
 )
 # Configure leanc
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index aad6899c53..e718fa0b24 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -6,14 +6,9 @@ else()
   set_target_properties(lean_stage0 PROPERTIES IMPORTED_LOCATION "${CMAKE_CURRENT_BINARY_DIR}/lean_stage0")
 endif()
 
-add_custom_target(export-stage1
-  COMMAND make -j8 export-stage1 "LEAN=$<TARGET_FILE:lean_stage0>"
-  DEPENDS lean_stage0
-  WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/../library")
-
 add_custom_target(update-stage0
   COMMAND make update-stage0
-  DEPENDS export-stage1
+  DEPENDS lean
   WORKING_DIRECTORY "${CMAKE_SOURCE_DIR}/../library")
 
 add_executable(lean lean.cpp)