diff --git a/CMakeLists.txt b/CMakeLists.txt
index 6aa7bf15479d..18272d6631bd 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -25,7 +25,7 @@ foreach(var ${vars})
     if(var MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
-    elseif(var MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
+    elseif(var MATCHES "LLVM*|PKG_CONFIG|USE_MIMALLOC")
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
   elseif(var MATCHES "USE_MIMALLOC")
diff --git a/doc/dev/bootstrap.md b/doc/dev/bootstrap.md
index 0cc10355202d..df7aa424b9f7 100644
--- a/doc/dev/bootstrap.md
+++ b/doc/dev/bootstrap.md
@@ -17,8 +17,6 @@ stage1/
   include/
     config.h  # config variables used to build `lean` such as used allocator
     runtime/lean.h  # runtime header, used by extracted C code, uses `config.h`
-  share/lean/
-    lean.mk  # used by `leanmake`
   lib/
     lean/**/*.olean  # the Lean library (incl. the compiler) compiled by the previous stage's `lean`
     temp/**/*.{c,o}  # the library extracted to C and compiled by `leanc`
@@ -28,7 +26,6 @@ stage1/
   bin/
     lean  # the Lean compiler & server, a small executable that calls directly into libleanshared.so
     leanc  # a wrapper around a C compiler supplying search paths etc
-    leanmake  # a wrapper around `make` supplying the Makefile above
 stage2/...
 stage3/...
 ```
diff --git a/doc/dev/index.md b/doc/dev/index.md
index 416271addadf..fa8c9d128f27 100644
--- a/doc/dev/index.md
+++ b/doc/dev/index.md
@@ -17,7 +17,7 @@ Please see below for specific instructions for VS Code.
 
 You can use [`elan`](https://github.com/leanprover/elan) to easily
 switch between stages and build configurations based on the current
-directory, both for the `lean`, `leanc`, and `leanmake` binaries in your shell's
+directory, both for the `lean` and `leanc` binaries in your shell's
 PATH and inside your editor.
 
 To install elan, you can do so, without installing a default version of Lean, using (Unix)
diff --git a/doc/examples/compiler/.gitignore b/doc/examples/compiler/.gitignore
deleted file mode 100644
index fcb6a2f4c6b9..000000000000
--- a/doc/examples/compiler/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-build
diff --git a/doc/examples/compiler/README.md b/doc/examples/compiler/README.md
deleted file mode 100644
index 59a10315e2ac..000000000000
--- a/doc/examples/compiler/README.md
+++ /dev/null
@@ -1,9 +0,0 @@
-In this example, we use the Lean C code generator to construct a simple program.
-
-1- Generate `build/bin/test` program using `leanmake bin` (assuming `bin/` from e.g. the stage 0.5 build directory is in your `PATH`)
-
-2- Execute test program
-```
-./build/bin/test hello world
-```
-It should produce `Result: [hello, world]`
diff --git a/doc/examples/compiler/run_test.sh b/doc/examples/compiler/run_test.sh
deleted file mode 100644
index 000aabbbdb4c..000000000000
--- a/doc/examples/compiler/run_test.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-leanmake --always-make bin
-
-capture ./build/bin/test hello world
-check_out_contains "[hello, world]"
diff --git a/doc/examples/compiler/test.lean b/doc/examples/compiler/test.lean
deleted file mode 100644
index 719dd1a87295..000000000000
--- a/doc/examples/compiler/test.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-#lang lean4
-def main (n : List String) : IO UInt32 := do
-   IO.println (toString n)
-   pure 0
diff --git a/doc/examples/compiler/test.lean.out.expected b/doc/examples/compiler/test.lean.out.expected
deleted file mode 100644
index 1f3b70c6840a..000000000000
--- a/doc/examples/compiler/test.lean.out.expected
+++ /dev/null
@@ -1 +0,0 @@
-[hello, world]
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6199a89b8c38..3c7de3f359a5 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -114,12 +114,10 @@ set(LEAN_MI_SECURE 0 CACHE STRING "Configure mimalloc memory safety mitigations
 
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
-option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
-option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
+option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds" OFF)
 
-set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
+set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake)")
 set(LEAN_EXTRA_LAKE_OPTS "" CACHE STRING "extra options to lake")
-set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
 # Temporary, core-only flags. Must be synced with stdlib_flags.h.
@@ -129,7 +127,6 @@ string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
 option(WFAIL "Fail build if warnings are emitted by Lean" ON)
 if(WFAIL MATCHES "ON")
   string(APPEND LEAN_EXTRA_LAKE_OPTS " --wfail")
-  string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
 endif()
 
 if(LAZY_RC MATCHES "ON")
@@ -618,7 +615,7 @@ if(USE_GITHASH)
     message(STATUS "git commit sha1: ${GIT_SHA1}")
   endif()
 else()
-  if(USE_LAKE AND STAGE EQUAL 0)
+  if(STAGE EQUAL 0)
     # we need to embed *some* hash for Lake to invalidate stage 1 on stage 0 changes
     execute_process(
       COMMAND git ls-tree HEAD "${CMAKE_CURRENT_SOURCE_DIR}/../../stage0" --object-only
@@ -658,30 +655,12 @@ else()
       endif()
     endif()
     message(STATUS "stage0 sha1: ${GIT_SHA1}")
-    # Now that we've prepared the information for the next stage, we can forget that we will use
-    # Lake in the future as we won't use it in this stage
-    set(USE_LAKE OFF)
   else()
     set(GIT_SHA1 "")
   endif()
 endif()
 configure_file("${LEAN_SOURCE_DIR}/githash.h.in" "${LEAN_BINARY_DIR}/githash.h")
 
-if(USE_LAKE AND STAGE EQUAL 0)
-  # Now that we've prepared the information for the next stage, we can forget that we will use
-  # Lake in the future as we won't use it in this stage
-  set(USE_LAKE OFF)
-endif()
-
-# Windows uses ";" as a path separator. We use `LEAN_PATH_SEPARATOR` on scripts such as lean.mk.in
-if(CMAKE_SYSTEM_NAME MATCHES "Windows")
-  set(LEAN_PATH_SEPARATOR ";")
-else()
-  set(LEAN_PATH_SEPARATOR ":")
-endif()
-
-# inherit genral options for lean.mk.in and stdlib.make.in
-string(APPEND LEAN_EXTRA_MAKE_OPTS " ${LEAN_EXTRA_OPTS}")
 
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
@@ -698,8 +677,6 @@ if(USE_MIMALLOC)
   )
 endif()
 install(DIRECTORY ${LEAN_BINARY_DIR}/include/ DESTINATION include)
-configure_file(${LEAN_SOURCE_DIR}/lean.mk.in ${LEAN_BINARY_DIR}/share/lean/lean.mk)
-install(DIRECTORY ${LEAN_BINARY_DIR}/share/ DESTINATION share)
 
 include_directories(${LEAN_SOURCE_DIR})
 include_directories(${CMAKE_BINARY_DIR}) # version.h etc., "private" headers
@@ -816,10 +793,7 @@ if(LEANTAR AND INSTALL_LEANTAR)
   add_dependencies(leancpp copy-leantar)
 endif()
 
-# MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
-string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
-
-# ...and Make doesn't like absolute Windows paths either
+# Make doesn't like absolute Windows paths
 # (also looks nicer in the build log)
 file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
@@ -837,12 +811,6 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   )
 endif()
 
-# Build the compiler using the bootstrapped C sources for stage0, and use
-# the LLVM build for stage1 and further.
-if(LLVM AND STAGE GREATER 0)
-  set(EXTRA_LEANMAKE_OPTS "LLVM=1")
-endif()
-
 set(
   STDLIBS
   Init
@@ -975,8 +943,6 @@ if(STAGE GREATER 0 AND NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   )
 endif()
 
-file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin)
-
 install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin)
 
 if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
@@ -1083,7 +1049,7 @@ else()
   set(CMAKE_BUILD_TYPE_TOML "Release")
 endif()
 
-if(USE_LAKE)
+if(STAGE GREATER 0)
   configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${CMAKE_BINARY_DIR}/lakefile.toml)
   # copy for editing
   if(STAGE EQUAL 1)
diff --git a/src/bin/leanmake b/src/bin/leanmake
deleted file mode 100755
index 7a04a26417fe..000000000000
--- a/src/bin/leanmake
+++ /dev/null
@@ -1,21 +0,0 @@
-#!/usr/bin/env bash
-# A simple wrapper around `make` and the `lean.mk` makefile
-# When called from a directory containing a `Makefile` file, calls `make` with
-# the directory containing `lean.mk` in its path so that you can use
-# `include lean.mk` in your code. Otherwise, run `lean.mk` directly.
-# Interesting targets:
-# * `leanmake PKG=Foo`  # compile package Foo into .olean files (in `build/Foo`, by default)
-# * `leanmake bin PKG=Foo`  # build the binary `build/bin/Foo`
-# * `leanmake lib PKG=Foo`  # build the library `build/lib/libFoo.a`
-# If there is exactly one .lean file in the current directory, you can omit `PKG`
-
-set -euo pipefail
-
-bindir=$(dirname $0)
-if [ -f Makefile ]; then
-    args=(-I "$bindir/../share/lean")
-else
-    args=(-f "$bindir/../share/lean/lean.mk")
-fi
-
-PATH="$bindir:$PATH" ${MAKE:-make} "${args[@]}" "$@"
diff --git a/src/lean.mk.in b/src/lean.mk.in
deleted file mode 100644
index 131a73a48abd..000000000000
--- a/src/lean.mk.in
+++ /dev/null
@@ -1,169 +0,0 @@
-# Copyright (c) 2018 Simon Hudon. All rights reserved.
-# Released under Apache 2.0 license as described in the file LICENSE.
-# Authors: Simon Hudon, Sebastian Ullrich, Leonardo de Moura
-
-# We compile all source files in $PKG/ as well as $PKG.lean. $PKG is also used for naming binary files.
-ifndef PKG
-  PKG = $(strip $(subst .lean,, $(wildcard *.lean)))
-  ifneq ($(words $(PKG)), 1)
-    $(error no unique .lean file found in current directory, please specify PKG)
-  endif
-endif
-
-LEAN = lean
-LEANC = leanc
-LEAN_AR = @CMAKE_AR@
-OUT = build
-OLEAN_OUT = $(OUT)
-TEMP_OUT = $(OUT)/temp
-C_OUT = $(TEMP_OUT)
-BC_OUT = $(TEMP_OUT)
-BIN_OUT = $(OUT)/bin
-LIB_OUT = $(OUT)/lib
-BIN_NAME = $(PKG)
-STATIC_LIB_NAME = lib$(PKG).a
-LEAN_OPTS += @LEAN_EXTRA_MAKE_OPTS@
-LEANC_OPTS = -O3 -DNDEBUG
-LINK_OPTS =
-
-# more FS entries to build SRCS from, for parallel build of .oleans (but not .os)
-EXTRA_SRC_ROOTS =
-
-# ignore error messages from missing parts, e.g. Leanc/
-SRCS = $(shell find $(PKG) $(PKG).lean $(EXTRA_SRC_ROOTS) -name '*.lean' 2> /dev/null)
-DEPS = $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.depend))
-export LEAN_PATH += @LEAN_PATH_SEPARATOR@$(OLEAN_OUT)
-OBJS = $(addprefix $(OLEAN_OUT)/, $(SRCS:.lean=.olean))
-ifdef C_ONLY
-# There are no .lean files in stage0/src/
-NAT_OBJS = $(patsubst %.c,$(TEMP_OUT)/%.o,$(shell cd $(C_OUT); find $(PKG) $(PKG).c -name '*.c' 2> /dev/null))
-ALL_NAT_OBJS = $(NAT_OBJS)
-else
-NAT_OBJS = $(patsubst %.lean,$(TEMP_OUT)/%.o,$(shell find $(PKG) $(PKG).lean -name '*.lean' 2> /dev/null))
-# include `EXTRA_SRC_ROOTS` when compiling individual `.o`s but not when building libraries
-ALL_NAT_OBJS = $(patsubst %.lean,$(TEMP_OUT)/%.o,$(SRCS))
-endif
-
-SHELL = /usr/bin/env bash -euo pipefail
-
-.PHONY: all bin lib depends clean
-# Disable all default make rules
-.SUFFIXES:
-
-objs: $(OBJS) $(ALL_NAT_OBJS)
-
-bin: $(BIN_OUT)/$(BIN_NAME)
-
-lib: $(LIB_OUT)/$(STATIC_LIB_NAME)
-lib.export: $(LIB_OUT)/$(STATIC_LIB_NAME).export
-
-depends: $(DEPS)
-
-$(OLEAN_OUT)/$(PKG) $(LIB_OUT) $(BIN_OUT):
-	@mkdir -p "$@"
-
-# Make sure the .olean output directory exists so that `lean --deps` knows where this package's
-# .olean files will be located even before any of them are actually built.
-$(TEMP_OUT)/%.depend: %.lean | $(OLEAN_OUT)/$(PKG)
-	@mkdir -p "$(TEMP_OUT)/$(*D)"
-# convert path separators and newlines on Windows
-	deps=`$(LEAN) --deps $<` || (echo "$(LEAN) --deps $< failed ($$?): $$deps"; exit 1); \
-  deps=`echo "$$deps" | tr '\\\\' / | tr -d '\\r'`; \
-  echo $(OLEAN_OUT)/$*.olean: $$deps > $@
-
-$(OLEAN_OUT)/%.olean: %.lean $(TEMP_OUT)/%.depend $(MORE_DEPS)
-ifdef CMAKE_LIKE_OUTPUT
-	@echo "[    ] Building $<"
-endif
-	@mkdir -p $(OLEAN_OUT)/$(*D)
-	LEAN_OPTS="$(LEAN_OPTS)"; \
-	[[ -z "$(LLVM)" ]] || LEAN_OPTS+=" --bc=$(TEMP_OUT)/$*.bc.tmp"; \
-	$(LEAN) $$LEAN_OPTS -o "$@" -i "$(OLEAN_OUT)/$*.ilean" --c="$(TEMP_OUT)/$*.c.tmp" "$<"
-# create the .c file atomically
-	@mv "$(TEMP_OUT)/$*.c.tmp" "$(C_OUT)/$*.c"
-ifdef LLVM
-	@mv "$(TEMP_OUT)/$*.bc.tmp" "$(BC_OUT)/$*.bc"
-endif
-
-$(OLEAN_OUT)/%.ilean: $(OLEAN_OUT)/%.olean
-	@
-
-ifndef C_ONLY
-$(C_OUT)/%.c: $(OLEAN_OUT)/%.olean
-	@
-
-$(BC_OUT)/%.bc: $(OLEAN_OUT)/%.olean
-	@
-endif
-
-ifdef LLVM
-$(TEMP_OUT)/%.o.export: $(BC_OUT)/%.bc
-else
-$(TEMP_OUT)/%.o.export: $(C_OUT)/%.c
-endif
-ifdef CMAKE_LIKE_OUTPUT
-	@echo "[    ] Building $<"
-endif
-	@mkdir -p "$(@D)"
-	$(LEANC) -c -o $@ $< $(LEANC_OPTS) -DLEAN_EXPORTING
-
-# On Windows, rebuild .o not intended for shared libraries
-# without dllexport because of symbol limit;
-# on other platforms, no point in bothering
-ifeq (@CMAKE_SYSTEM_NAME@, Windows)
-ifdef LLVM
-$(TEMP_OUT)/%.o: $(BC_OUT)/%.bc
-else
-$(TEMP_OUT)/%.o: $(C_OUT)/%.c
-endif
-ifdef CMAKE_LIKE_OUTPUT
-	@echo "[    ] Building $<"
-endif
-	@mkdir -p "$(@D)"
-	$(LEANC) -c -o $@ $< $(LEANC_OPTS)
-else
-$(TEMP_OUT)/%.o: $(TEMP_OUT)/%.o.export
-	ln -f $< $@
-endif
-
-$(BIN_OUT)/$(BIN_NAME): $(LIB_OUT)/$(STATIC_LIB_NAME).export | $(BIN_OUT)
-ifdef CMAKE_LIKE_OUTPUT
-	@echo "[    ] Linking $@"
-endif
-# on Windows, must remove binary before writing a new one (since the old one may be in use)
-	@rm -f $@
-	$(LEANC) -o "$@" $< $(LEANC_OPTS) $(LINK_OPTS)
-
-ifeq (@CMAKE_SYSTEM_NAME@, Windows)
-$(LIB_OUT)/$(STATIC_LIB_NAME): $(NAT_OBJS) | $(LIB_OUT)
-	@rm -f $@
-	$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
-	@$(LEAN_AR) rcs $@ @$@.in
-	@rm -f $@.in
-$(LIB_OUT)/$(STATIC_LIB_NAME).export: $(addsuffix .export,$(NAT_OBJS)) | $(LIB_OUT)
-	@rm -f $@
-	$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
-	# "T"hin archive seems necessary to preserve paths so that we can distinguish
-	# between object files with the same file name when manipulating the archive for
-	# `libleanshared_*`
-	@$(LEAN_AR) rcsT $@ @$@.in
-	@rm -f $@.in
-else
-$(LIB_OUT)/$(STATIC_LIB_NAME): $(NAT_OBJS) | $(LIB_OUT)
-	@rm -f $@
-# no response file support on macOS, but also no need for them
-	@$(LEAN_AR) rcs $@ $^
-$(LIB_OUT)/$(STATIC_LIB_NAME).export: $(LIB_OUT)/$(STATIC_LIB_NAME)
-	ln -f $< $@
-endif
-
-clean:
-	rm -rf $(OUT)
-
-.PRECIOUS: $(BC_OUT)/%.bc $(C_OUT)/%.c $(TEMP_OUT)/%.o $(TEMP_OUT)/%.o.export
-
-ifndef C_ONLY
-ifndef UNSAFE_ASSUME_OLD
-include $(DEPS)
-endif
-endif
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 45feac318313..e09dd3c34626 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -4,9 +4,13 @@
 LEAN_BASH ?= /usr/bin/env bash
 SHELL := $(LEAN_BASH) -eo pipefail
 
+# This makefile uses only explicit and pattern rules; disable make's built-in
+# rules so a stray `.c` next to a `.o` cannot trigger an unintended C compile.
+MAKEFLAGS += -r
+
 # any absolute path to the stdlib breaks the Makefile
 export LEAN_PATH=
-ifeq "${USE_LAKE}" "ON"
+ifneq "${STAGE}" "0"
   export LEAN_CC=${CMAKE_C_COMPILER}
 else
   export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER}
@@ -28,29 +32,11 @@ define link-preamble
 @rm -f $@
 endef
 
-# MORE_DEPS: rebuild the stdlib whenever the compiler has changed
-LEANMAKE_OPTS=\
-	LEAN="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\
-	LEANC="${CMAKE_BINARY_DIR}/leanc.sh"\
-	OUT="${LIB}"\
-	LIB_OUT="${LIB}/lean"\
-	OLEAN_OUT="${LIB}/lean"\
-	BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
-	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS}"\
-	LEANC_OPTS+="${LEANC_OPTS}"\
-	LEAN_AR="${CMAKE_AR}"\
-	MORE_DEPS+="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\
-	${EXTRA_LEANMAKE_OPTS}\
-	CMAKE_LIKE_OUTPUT=1
-
-ifeq "${STAGE}" "0"
-  LEANMAKE_OPTS+=C_ONLY=1 C_OUT=${LEAN_SOURCE_DIR}/../stdlib/
-endif
-
-# These can be phony since the inner Makefile/Lake will have the correct dependencies and avoid rebuilds
+# `Init` etc. below are phony aliases; the real dependencies are tracked by Lake
+# (stage 1+) or by the archive rules (stage 0).
 .PHONY: Init Std Lean leanshared Lake libLake_shared lake lean LeanChecker leanchecker LeanIR
 
-ifeq "${USE_LAKE}" "ON"
+ifneq "${STAGE}" "0"
 
 # build in parallel
 Init:
@@ -60,33 +46,90 @@ Std Lean Lake Leanc LeanChecker LeanIR: Init
 
 else
 
-Init:
-	@mkdir -p "${LIB}/lean/Lean" "${LIB}/lean/Lake" "${LIB}/lean/Std"
-# Use `+` to use the Make jobserver with `leanmake` for parallelized builds
-# Build `.olean/.o`s of downstream libraries as well for better parallelism
-	+"${LEAN_BIN}/leanmake" objs lib lib.export PKG=Init $(LEANMAKE_OPTS) \
-	  EXTRA_SRC_ROOTS="Std Std.lean Lean Lean.lean LeanIR.lean"
-
-Std: Init
-	+"${LEAN_BIN}/leanmake" lib lib.export PKG=Std $(LEANMAKE_OPTS)
-
-Lean: Std
-	+"${LEAN_BIN}/leanmake" lib lib.export PKG=Lean $(LEANMAKE_OPTS)
-
-Leanc: Lean
-ifneq "${STAGE}" "0"
-	+"${LEAN_BIN}/leanmake" -C "${CMAKE_BINARY_DIR}/leanc" lib PKG=Leanc $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" OLEAN_OUT="$(OUTARC)"
+# --- Stage 0 has no Lake yet: compile the pre-generated C sources directly. ---
+# `update-stage0` snapshots the C sources under `stage0/stdlib/`; there are no
+# `.lean` files to elaborate, so this is plain C compilation and archiving.
+STDLIB_C := ${LEAN_SOURCE_DIR}/../stdlib
+OBJ_OUT  := ${LIB}/temp
+# `leanc.sh` reads the exported `LEAN_CC`; `-O3 -DNDEBUG` is the historical default.
+LEANC_COMPILE := $(LEANC_SH) -c -O3 -DNDEBUG ${LEANC_OPTS}
+
+# $(call c-objs,<pkg>): the `.o.export` files for package <pkg>, mirroring its `.c` layout.
+# `2> /dev/null`: ignore the find error when a package has no source directory.
+c-objs = $(patsubst %.c,$(OBJ_OUT)/%.o.export,$(shell cd $(STDLIB_C) && find $(1) $(1).c -name '*.c' 2> /dev/null))
+
+Init_OBJS        := $(call c-objs,Init)
+Std_OBJS         := $(call c-objs,Std)
+Lean_OBJS        := $(call c-objs,Lean)
+Lake_OBJS        := $(call c-objs,Lake)
+LeanChecker_OBJS := $(call c-objs,LeanChecker)
+LeanIR_OBJS      := $(call c-objs,LeanIR)
+
+# Every object is built with `-DLEAN_EXPORTING`: stage 0 links nothing that needs a
+# non-exported variant (the Windows symbol-limit `.o`), so there is a single compile
+# per source file.
+$(OBJ_OUT)/%.o.export: $(STDLIB_C)/%.c
+	@echo "[    ] Building $<"
+	@mkdir -p "$(@D)"
+	$(LEANC_COMPILE) -o $@ $< -DLEAN_EXPORTING
+
+# Keep the object files: the archive rules and the later link steps consume them,
+# so make must not treat them as deletable intermediates.
+.PRECIOUS: $(OBJ_OUT)/%.o.export
+
+${LIB}/lean $(OUTARC):
+	@mkdir -p "$@"
+
+# Archive `$^` into `$@`. On Windows the object list goes through a response file
+# (command-line length limit). `Init`/`Std`/`Lean`/`Lake` feed the shared libraries,
+# so their archives are named `.a.export` and — on Windows — "T"hin, letting the
+# `libleanshared` build manipulate them by path. `LeanChecker`/`LeanIR` are linked
+# statically into executables, so they get a plain archive.
+ifeq "${CMAKE_SYSTEM_NAME}" "Windows"
+define ar-shared
+@rm -f $@
+$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
+@${CMAKE_AR} rcsT $@ @$@.in
+@rm -f $@.in
+endef
+define ar-exe
+@rm -f $@
+$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
+@${CMAKE_AR} rcs $@ @$@.in
+@rm -f $@.in
+endef
+else
+define ar-shared
+@rm -f $@
+@${CMAKE_AR} rcs $@ $^
+endef
+define ar-exe
+@rm -f $@
+@${CMAKE_AR} rcs $@ $^
+endef
 endif
 
-Lake: Lean
-# lake is in its own subdirectory, so must adjust relative paths...
-	+"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export  PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean
-
-LeanChecker: Lake
-	+"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" TEMP_OUT="${LIB}/temp" OLEAN_OUT="$(OUTARC)"
-
-LeanIR: Lean
-	+"${LEAN_BIN}/leanmake" lib PKG=LeanIR $(LEANMAKE_OPTS) OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" LIB_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" OLEAN_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}"
+${LIB}/lean/libInit.a.export: $(Init_OBJS) | ${LIB}/lean
+	$(ar-shared)
+${LIB}/lean/libStd.a.export: $(Std_OBJS) | ${LIB}/lean
+	$(ar-shared)
+${LIB}/lean/libLean.a.export: $(Lean_OBJS) | ${LIB}/lean
+	$(ar-shared)
+${LIB}/lean/libLake.a.export: $(Lake_OBJS) | ${LIB}/lean
+	$(ar-shared)
+$(OUTARC)/libLeanChecker.a: $(LeanChecker_OBJS) | $(OUTARC)
+	$(ar-exe)
+$(OUTARC)/libLeanIR.a: $(LeanIR_OBJS) | $(OUTARC)
+	$(ar-exe)
+
+Init: ${LIB}/lean/libInit.a.export
+Std:  ${LIB}/lean/libStd.a.export
+Lean: ${LIB}/lean/libLean.a.export
+Lake: ${LIB}/lean/libLake.a.export $(OBJ_OUT)/LakeMain.o.export
+LeanChecker: $(OUTARC)/libLeanChecker.a
+LeanIR: $(OUTARC)/libLeanIR.a
+# `Leanc` has no Lean library to build at stage 0; its C sources are compiled in a later stage.
+Leanc:
 
 endif
 
@@ -96,7 +139,7 @@ ${LIB}/temp/empty.c:
 # the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt
 
 # Lake archive timestamps may be stale due to caching; use .trace files for rebuild decisions
-ifeq "${USE_LAKE}" "ON"
+ifneq "${STAGE}" "0"
 $(OUTLIB)/libInit_shared$(SO): ${LIB}/lean/libInit.a.export.trace ${LIB}/lean/libStd.a.export.trace
 $(OUTLIB)/libleanshared$(SO): ${LIB}/lean/libLean.a.export.trace
 $(OUTLIB)/libLake_shared$(SO): ${LIB}/lean/libLean.a.export.trace ${LIB}/lean/libLake.a.export.trace
@@ -156,10 +199,10 @@ else
 	$(LEANC_SH) -shared -o $(OUTLIB)/libleanshared_2$(SO) ${LIB}/temp/empty.c ${LEANSHARED_2_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
 ifeq "${CMAKE_SYSTEM_NAME}" "Darwin"
 	$(LEANC_SH) -shared -o $@ \
-	  ${LIB}/temp/Lean.*o.export -Wl,-force_load,${LIB}/temp/libleanshell.a -lInit -lStd -lLean -lleancpp ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
+	  ${LIB}/temp/Lean.*o.export -Wl,-force_load,${LIB}/temp/libleanshell.a ${LIB}/lean/libInit.a.export ${LIB}/lean/libStd.a.export ${LIB}/lean/libLean.a.export ${LIB}/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
 else
 	$(LEANC_SH) -shared -o $@ \
-	  -Wl,--whole-archive ${LIB}/temp/Lean.*o.export ${LIB}/temp/libleanshell.a -Wl,--no-whole-archive -Wl,--start-group -lInit -lStd -lLean -lleancpp -Wl,--end-group ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
+	  -Wl,--whole-archive ${LIB}/temp/Lean.*o.export ${LIB}/temp/libleanshell.a -Wl,--no-whole-archive -Wl,--start-group ${LIB}/lean/libInit.a.export ${LIB}/lean/libStd.a.export ${LIB}/lean/libLean.a.export ${LIB}/lean/libleancpp.a -Wl,--end-group ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
 endif
 endif
 ifeq "${STRIP_BINARIES}" "ON"
diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h
index e44444704908..c79ca3152fd0 100644
--- a/src/stdlib_flags.h
+++ b/src/stdlib_flags.h
@@ -24,7 +24,7 @@ options get_default_options() {
     opts = opts.update({"pp", "rawOnError"}, true);
 
     // Temporary, core-only flags for editing (i.e. must be part of stage0/bin/lean). Must be synced
-    // with `LEAN_EXTRA_MAKE_OPTS` build flags in src/CMakeLists.txt.
+    // with `LEAN_EXTRA_OPTS` build flags in src/CMakeLists.txt.
     opts = opts.update({"backward", "do", "legacy"}, false);
 #endif
     return opts;
diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt
index 6199a89b8c38..3c7de3f359a5 100644
--- a/stage0/src/CMakeLists.txt
+++ b/stage0/src/CMakeLists.txt
@@ -114,12 +114,10 @@ set(LEAN_MI_SECURE 0 CACHE STRING "Configure mimalloc memory safety mitigations
 
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
-option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
-option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
+option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds" OFF)
 
-set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
+set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake)")
 set(LEAN_EXTRA_LAKE_OPTS "" CACHE STRING "extra options to lake")
-set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
 # Temporary, core-only flags. Must be synced with stdlib_flags.h.
@@ -129,7 +127,6 @@ string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
 option(WFAIL "Fail build if warnings are emitted by Lean" ON)
 if(WFAIL MATCHES "ON")
   string(APPEND LEAN_EXTRA_LAKE_OPTS " --wfail")
-  string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
 endif()
 
 if(LAZY_RC MATCHES "ON")
@@ -618,7 +615,7 @@ if(USE_GITHASH)
     message(STATUS "git commit sha1: ${GIT_SHA1}")
   endif()
 else()
-  if(USE_LAKE AND STAGE EQUAL 0)
+  if(STAGE EQUAL 0)
     # we need to embed *some* hash for Lake to invalidate stage 1 on stage 0 changes
     execute_process(
       COMMAND git ls-tree HEAD "${CMAKE_CURRENT_SOURCE_DIR}/../../stage0" --object-only
@@ -658,30 +655,12 @@ else()
       endif()
     endif()
     message(STATUS "stage0 sha1: ${GIT_SHA1}")
-    # Now that we've prepared the information for the next stage, we can forget that we will use
-    # Lake in the future as we won't use it in this stage
-    set(USE_LAKE OFF)
   else()
     set(GIT_SHA1 "")
   endif()
 endif()
 configure_file("${LEAN_SOURCE_DIR}/githash.h.in" "${LEAN_BINARY_DIR}/githash.h")
 
-if(USE_LAKE AND STAGE EQUAL 0)
-  # Now that we've prepared the information for the next stage, we can forget that we will use
-  # Lake in the future as we won't use it in this stage
-  set(USE_LAKE OFF)
-endif()
-
-# Windows uses ";" as a path separator. We use `LEAN_PATH_SEPARATOR` on scripts such as lean.mk.in
-if(CMAKE_SYSTEM_NAME MATCHES "Windows")
-  set(LEAN_PATH_SEPARATOR ";")
-else()
-  set(LEAN_PATH_SEPARATOR ":")
-endif()
-
-# inherit genral options for lean.mk.in and stdlib.make.in
-string(APPEND LEAN_EXTRA_MAKE_OPTS " ${LEAN_EXTRA_OPTS}")
 
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
@@ -698,8 +677,6 @@ if(USE_MIMALLOC)
   )
 endif()
 install(DIRECTORY ${LEAN_BINARY_DIR}/include/ DESTINATION include)
-configure_file(${LEAN_SOURCE_DIR}/lean.mk.in ${LEAN_BINARY_DIR}/share/lean/lean.mk)
-install(DIRECTORY ${LEAN_BINARY_DIR}/share/ DESTINATION share)
 
 include_directories(${LEAN_SOURCE_DIR})
 include_directories(${CMAKE_BINARY_DIR}) # version.h etc., "private" headers
@@ -816,10 +793,7 @@ if(LEANTAR AND INSTALL_LEANTAR)
   add_dependencies(leancpp copy-leantar)
 endif()
 
-# MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
-string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
-
-# ...and Make doesn't like absolute Windows paths either
+# Make doesn't like absolute Windows paths
 # (also looks nicer in the build log)
 file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
@@ -837,12 +811,6 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   )
 endif()
 
-# Build the compiler using the bootstrapped C sources for stage0, and use
-# the LLVM build for stage1 and further.
-if(LLVM AND STAGE GREATER 0)
-  set(EXTRA_LEANMAKE_OPTS "LLVM=1")
-endif()
-
 set(
   STDLIBS
   Init
@@ -975,8 +943,6 @@ if(STAGE GREATER 0 AND NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   )
 endif()
 
-file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin)
-
 install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin)
 
 if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
@@ -1083,7 +1049,7 @@ else()
   set(CMAKE_BUILD_TYPE_TOML "Release")
 endif()
 
-if(USE_LAKE)
+if(STAGE GREATER 0)
   configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${CMAKE_BINARY_DIR}/lakefile.toml)
   # copy for editing
   if(STAGE EQUAL 1)
diff --git a/stage0/src/bin/leanmake b/stage0/src/bin/leanmake
deleted file mode 100755
index 7a04a26417fe..000000000000
--- a/stage0/src/bin/leanmake
+++ /dev/null
@@ -1,21 +0,0 @@
-#!/usr/bin/env bash
-# A simple wrapper around `make` and the `lean.mk` makefile
-# When called from a directory containing a `Makefile` file, calls `make` with
-# the directory containing `lean.mk` in its path so that you can use
-# `include lean.mk` in your code. Otherwise, run `lean.mk` directly.
-# Interesting targets:
-# * `leanmake PKG=Foo`  # compile package Foo into .olean files (in `build/Foo`, by default)
-# * `leanmake bin PKG=Foo`  # build the binary `build/bin/Foo`
-# * `leanmake lib PKG=Foo`  # build the library `build/lib/libFoo.a`
-# If there is exactly one .lean file in the current directory, you can omit `PKG`
-
-set -euo pipefail
-
-bindir=$(dirname $0)
-if [ -f Makefile ]; then
-    args=(-I "$bindir/../share/lean")
-else
-    args=(-f "$bindir/../share/lean/lean.mk")
-fi
-
-PATH="$bindir:$PATH" ${MAKE:-make} "${args[@]}" "$@"
diff --git a/stage0/src/lean.mk.in b/stage0/src/lean.mk.in
deleted file mode 100644
index 131a73a48abd..000000000000
--- a/stage0/src/lean.mk.in
+++ /dev/null
@@ -1,169 +0,0 @@
-# Copyright (c) 2018 Simon Hudon. All rights reserved.
-# Released under Apache 2.0 license as described in the file LICENSE.
-# Authors: Simon Hudon, Sebastian Ullrich, Leonardo de Moura
-
-# We compile all source files in $PKG/ as well as $PKG.lean. $PKG is also used for naming binary files.
-ifndef PKG
-  PKG = $(strip $(subst .lean,, $(wildcard *.lean)))
-  ifneq ($(words $(PKG)), 1)
-    $(error no unique .lean file found in current directory, please specify PKG)
-  endif
-endif
-
-LEAN = lean
-LEANC = leanc
-LEAN_AR = @CMAKE_AR@
-OUT = build
-OLEAN_OUT = $(OUT)
-TEMP_OUT = $(OUT)/temp
-C_OUT = $(TEMP_OUT)
-BC_OUT = $(TEMP_OUT)
-BIN_OUT = $(OUT)/bin
-LIB_OUT = $(OUT)/lib
-BIN_NAME = $(PKG)
-STATIC_LIB_NAME = lib$(PKG).a
-LEAN_OPTS += @LEAN_EXTRA_MAKE_OPTS@
-LEANC_OPTS = -O3 -DNDEBUG
-LINK_OPTS =
-
-# more FS entries to build SRCS from, for parallel build of .oleans (but not .os)
-EXTRA_SRC_ROOTS =
-
-# ignore error messages from missing parts, e.g. Leanc/
-SRCS = $(shell find $(PKG) $(PKG).lean $(EXTRA_SRC_ROOTS) -name '*.lean' 2> /dev/null)
-DEPS = $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.depend))
-export LEAN_PATH += @LEAN_PATH_SEPARATOR@$(OLEAN_OUT)
-OBJS = $(addprefix $(OLEAN_OUT)/, $(SRCS:.lean=.olean))
-ifdef C_ONLY
-# There are no .lean files in stage0/src/
-NAT_OBJS = $(patsubst %.c,$(TEMP_OUT)/%.o,$(shell cd $(C_OUT); find $(PKG) $(PKG).c -name '*.c' 2> /dev/null))
-ALL_NAT_OBJS = $(NAT_OBJS)
-else
-NAT_OBJS = $(patsubst %.lean,$(TEMP_OUT)/%.o,$(shell find $(PKG) $(PKG).lean -name '*.lean' 2> /dev/null))
-# include `EXTRA_SRC_ROOTS` when compiling individual `.o`s but not when building libraries
-ALL_NAT_OBJS = $(patsubst %.lean,$(TEMP_OUT)/%.o,$(SRCS))
-endif
-
-SHELL = /usr/bin/env bash -euo pipefail
-
-.PHONY: all bin lib depends clean
-# Disable all default make rules
-.SUFFIXES:
-
-objs: $(OBJS) $(ALL_NAT_OBJS)
-
-bin: $(BIN_OUT)/$(BIN_NAME)
-
-lib: $(LIB_OUT)/$(STATIC_LIB_NAME)
-lib.export: $(LIB_OUT)/$(STATIC_LIB_NAME).export
-
-depends: $(DEPS)
-
-$(OLEAN_OUT)/$(PKG) $(LIB_OUT) $(BIN_OUT):
-	@mkdir -p "$@"
-
-# Make sure the .olean output directory exists so that `lean --deps` knows where this package's
-# .olean files will be located even before any of them are actually built.
-$(TEMP_OUT)/%.depend: %.lean | $(OLEAN_OUT)/$(PKG)
-	@mkdir -p "$(TEMP_OUT)/$(*D)"
-# convert path separators and newlines on Windows
-	deps=`$(LEAN) --deps $<` || (echo "$(LEAN) --deps $< failed ($$?): $$deps"; exit 1); \
-  deps=`echo "$$deps" | tr '\\\\' / | tr -d '\\r'`; \
-  echo $(OLEAN_OUT)/$*.olean: $$deps > $@
-
-$(OLEAN_OUT)/%.olean: %.lean $(TEMP_OUT)/%.depend $(MORE_DEPS)
-ifdef CMAKE_LIKE_OUTPUT
-	@echo "[    ] Building $<"
-endif
-	@mkdir -p $(OLEAN_OUT)/$(*D)
-	LEAN_OPTS="$(LEAN_OPTS)"; \
-	[[ -z "$(LLVM)" ]] || LEAN_OPTS+=" --bc=$(TEMP_OUT)/$*.bc.tmp"; \
-	$(LEAN) $$LEAN_OPTS -o "$@" -i "$(OLEAN_OUT)/$*.ilean" --c="$(TEMP_OUT)/$*.c.tmp" "$<"
-# create the .c file atomically
-	@mv "$(TEMP_OUT)/$*.c.tmp" "$(C_OUT)/$*.c"
-ifdef LLVM
-	@mv "$(TEMP_OUT)/$*.bc.tmp" "$(BC_OUT)/$*.bc"
-endif
-
-$(OLEAN_OUT)/%.ilean: $(OLEAN_OUT)/%.olean
-	@
-
-ifndef C_ONLY
-$(C_OUT)/%.c: $(OLEAN_OUT)/%.olean
-	@
-
-$(BC_OUT)/%.bc: $(OLEAN_OUT)/%.olean
-	@
-endif
-
-ifdef LLVM
-$(TEMP_OUT)/%.o.export: $(BC_OUT)/%.bc
-else
-$(TEMP_OUT)/%.o.export: $(C_OUT)/%.c
-endif
-ifdef CMAKE_LIKE_OUTPUT
-	@echo "[    ] Building $<"
-endif
-	@mkdir -p "$(@D)"
-	$(LEANC) -c -o $@ $< $(LEANC_OPTS) -DLEAN_EXPORTING
-
-# On Windows, rebuild .o not intended for shared libraries
-# without dllexport because of symbol limit;
-# on other platforms, no point in bothering
-ifeq (@CMAKE_SYSTEM_NAME@, Windows)
-ifdef LLVM
-$(TEMP_OUT)/%.o: $(BC_OUT)/%.bc
-else
-$(TEMP_OUT)/%.o: $(C_OUT)/%.c
-endif
-ifdef CMAKE_LIKE_OUTPUT
-	@echo "[    ] Building $<"
-endif
-	@mkdir -p "$(@D)"
-	$(LEANC) -c -o $@ $< $(LEANC_OPTS)
-else
-$(TEMP_OUT)/%.o: $(TEMP_OUT)/%.o.export
-	ln -f $< $@
-endif
-
-$(BIN_OUT)/$(BIN_NAME): $(LIB_OUT)/$(STATIC_LIB_NAME).export | $(BIN_OUT)
-ifdef CMAKE_LIKE_OUTPUT
-	@echo "[    ] Linking $@"
-endif
-# on Windows, must remove binary before writing a new one (since the old one may be in use)
-	@rm -f $@
-	$(LEANC) -o "$@" $< $(LEANC_OPTS) $(LINK_OPTS)
-
-ifeq (@CMAKE_SYSTEM_NAME@, Windows)
-$(LIB_OUT)/$(STATIC_LIB_NAME): $(NAT_OBJS) | $(LIB_OUT)
-	@rm -f $@
-	$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
-	@$(LEAN_AR) rcs $@ @$@.in
-	@rm -f $@.in
-$(LIB_OUT)/$(STATIC_LIB_NAME).export: $(addsuffix .export,$(NAT_OBJS)) | $(LIB_OUT)
-	@rm -f $@
-	$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
-	# "T"hin archive seems necessary to preserve paths so that we can distinguish
-	# between object files with the same file name when manipulating the archive for
-	# `libleanshared_*`
-	@$(LEAN_AR) rcsT $@ @$@.in
-	@rm -f $@.in
-else
-$(LIB_OUT)/$(STATIC_LIB_NAME): $(NAT_OBJS) | $(LIB_OUT)
-	@rm -f $@
-# no response file support on macOS, but also no need for them
-	@$(LEAN_AR) rcs $@ $^
-$(LIB_OUT)/$(STATIC_LIB_NAME).export: $(LIB_OUT)/$(STATIC_LIB_NAME)
-	ln -f $< $@
-endif
-
-clean:
-	rm -rf $(OUT)
-
-.PRECIOUS: $(BC_OUT)/%.bc $(C_OUT)/%.c $(TEMP_OUT)/%.o $(TEMP_OUT)/%.o.export
-
-ifndef C_ONLY
-ifndef UNSAFE_ASSUME_OLD
-include $(DEPS)
-endif
-endif
diff --git a/stage0/src/stdlib.make.in b/stage0/src/stdlib.make.in
index 45feac318313..e09dd3c34626 100644
--- a/stage0/src/stdlib.make.in
+++ b/stage0/src/stdlib.make.in
@@ -4,9 +4,13 @@
 LEAN_BASH ?= /usr/bin/env bash
 SHELL := $(LEAN_BASH) -eo pipefail
 
+# This makefile uses only explicit and pattern rules; disable make's built-in
+# rules so a stray `.c` next to a `.o` cannot trigger an unintended C compile.
+MAKEFLAGS += -r
+
 # any absolute path to the stdlib breaks the Makefile
 export LEAN_PATH=
-ifeq "${USE_LAKE}" "ON"
+ifneq "${STAGE}" "0"
   export LEAN_CC=${CMAKE_C_COMPILER}
 else
   export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER}
@@ -28,29 +32,11 @@ define link-preamble
 @rm -f $@
 endef
 
-# MORE_DEPS: rebuild the stdlib whenever the compiler has changed
-LEANMAKE_OPTS=\
-	LEAN="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\
-	LEANC="${CMAKE_BINARY_DIR}/leanc.sh"\
-	OUT="${LIB}"\
-	LIB_OUT="${LIB}/lean"\
-	OLEAN_OUT="${LIB}/lean"\
-	BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
-	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS}"\
-	LEANC_OPTS+="${LEANC_OPTS}"\
-	LEAN_AR="${CMAKE_AR}"\
-	MORE_DEPS+="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\
-	${EXTRA_LEANMAKE_OPTS}\
-	CMAKE_LIKE_OUTPUT=1
-
-ifeq "${STAGE}" "0"
-  LEANMAKE_OPTS+=C_ONLY=1 C_OUT=${LEAN_SOURCE_DIR}/../stdlib/
-endif
-
-# These can be phony since the inner Makefile/Lake will have the correct dependencies and avoid rebuilds
+# `Init` etc. below are phony aliases; the real dependencies are tracked by Lake
+# (stage 1+) or by the archive rules (stage 0).
 .PHONY: Init Std Lean leanshared Lake libLake_shared lake lean LeanChecker leanchecker LeanIR
 
-ifeq "${USE_LAKE}" "ON"
+ifneq "${STAGE}" "0"
 
 # build in parallel
 Init:
@@ -60,33 +46,90 @@ Std Lean Lake Leanc LeanChecker LeanIR: Init
 
 else
 
-Init:
-	@mkdir -p "${LIB}/lean/Lean" "${LIB}/lean/Lake" "${LIB}/lean/Std"
-# Use `+` to use the Make jobserver with `leanmake` for parallelized builds
-# Build `.olean/.o`s of downstream libraries as well for better parallelism
-	+"${LEAN_BIN}/leanmake" objs lib lib.export PKG=Init $(LEANMAKE_OPTS) \
-	  EXTRA_SRC_ROOTS="Std Std.lean Lean Lean.lean LeanIR.lean"
-
-Std: Init
-	+"${LEAN_BIN}/leanmake" lib lib.export PKG=Std $(LEANMAKE_OPTS)
-
-Lean: Std
-	+"${LEAN_BIN}/leanmake" lib lib.export PKG=Lean $(LEANMAKE_OPTS)
-
-Leanc: Lean
-ifneq "${STAGE}" "0"
-	+"${LEAN_BIN}/leanmake" -C "${CMAKE_BINARY_DIR}/leanc" lib PKG=Leanc $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" OLEAN_OUT="$(OUTARC)"
+# --- Stage 0 has no Lake yet: compile the pre-generated C sources directly. ---
+# `update-stage0` snapshots the C sources under `stage0/stdlib/`; there are no
+# `.lean` files to elaborate, so this is plain C compilation and archiving.
+STDLIB_C := ${LEAN_SOURCE_DIR}/../stdlib
+OBJ_OUT  := ${LIB}/temp
+# `leanc.sh` reads the exported `LEAN_CC`; `-O3 -DNDEBUG` is the historical default.
+LEANC_COMPILE := $(LEANC_SH) -c -O3 -DNDEBUG ${LEANC_OPTS}
+
+# $(call c-objs,<pkg>): the `.o.export` files for package <pkg>, mirroring its `.c` layout.
+# `2> /dev/null`: ignore the find error when a package has no source directory.
+c-objs = $(patsubst %.c,$(OBJ_OUT)/%.o.export,$(shell cd $(STDLIB_C) && find $(1) $(1).c -name '*.c' 2> /dev/null))
+
+Init_OBJS        := $(call c-objs,Init)
+Std_OBJS         := $(call c-objs,Std)
+Lean_OBJS        := $(call c-objs,Lean)
+Lake_OBJS        := $(call c-objs,Lake)
+LeanChecker_OBJS := $(call c-objs,LeanChecker)
+LeanIR_OBJS      := $(call c-objs,LeanIR)
+
+# Every object is built with `-DLEAN_EXPORTING`: stage 0 links nothing that needs a
+# non-exported variant (the Windows symbol-limit `.o`), so there is a single compile
+# per source file.
+$(OBJ_OUT)/%.o.export: $(STDLIB_C)/%.c
+	@echo "[    ] Building $<"
+	@mkdir -p "$(@D)"
+	$(LEANC_COMPILE) -o $@ $< -DLEAN_EXPORTING
+
+# Keep the object files: the archive rules and the later link steps consume them,
+# so make must not treat them as deletable intermediates.
+.PRECIOUS: $(OBJ_OUT)/%.o.export
+
+${LIB}/lean $(OUTARC):
+	@mkdir -p "$@"
+
+# Archive `$^` into `$@`. On Windows the object list goes through a response file
+# (command-line length limit). `Init`/`Std`/`Lean`/`Lake` feed the shared libraries,
+# so their archives are named `.a.export` and — on Windows — "T"hin, letting the
+# `libleanshared` build manipulate them by path. `LeanChecker`/`LeanIR` are linked
+# statically into executables, so they get a plain archive.
+ifeq "${CMAKE_SYSTEM_NAME}" "Windows"
+define ar-shared
+@rm -f $@
+$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
+@${CMAKE_AR} rcsT $@ @$@.in
+@rm -f $@.in
+endef
+define ar-exe
+@rm -f $@
+$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
+@${CMAKE_AR} rcs $@ @$@.in
+@rm -f $@.in
+endef
+else
+define ar-shared
+@rm -f $@
+@${CMAKE_AR} rcs $@ $^
+endef
+define ar-exe
+@rm -f $@
+@${CMAKE_AR} rcs $@ $^
+endef
 endif
 
-Lake: Lean
-# lake is in its own subdirectory, so must adjust relative paths...
-	+"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export  PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean
-
-LeanChecker: Lake
-	+"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" TEMP_OUT="${LIB}/temp" OLEAN_OUT="$(OUTARC)"
-
-LeanIR: Lean
-	+"${LEAN_BIN}/leanmake" lib PKG=LeanIR $(LEANMAKE_OPTS) OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" LIB_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" OLEAN_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}"
+${LIB}/lean/libInit.a.export: $(Init_OBJS) | ${LIB}/lean
+	$(ar-shared)
+${LIB}/lean/libStd.a.export: $(Std_OBJS) | ${LIB}/lean
+	$(ar-shared)
+${LIB}/lean/libLean.a.export: $(Lean_OBJS) | ${LIB}/lean
+	$(ar-shared)
+${LIB}/lean/libLake.a.export: $(Lake_OBJS) | ${LIB}/lean
+	$(ar-shared)
+$(OUTARC)/libLeanChecker.a: $(LeanChecker_OBJS) | $(OUTARC)
+	$(ar-exe)
+$(OUTARC)/libLeanIR.a: $(LeanIR_OBJS) | $(OUTARC)
+	$(ar-exe)
+
+Init: ${LIB}/lean/libInit.a.export
+Std:  ${LIB}/lean/libStd.a.export
+Lean: ${LIB}/lean/libLean.a.export
+Lake: ${LIB}/lean/libLake.a.export $(OBJ_OUT)/LakeMain.o.export
+LeanChecker: $(OUTARC)/libLeanChecker.a
+LeanIR: $(OUTARC)/libLeanIR.a
+# `Leanc` has no Lean library to build at stage 0; its C sources are compiled in a later stage.
+Leanc:
 
 endif
 
@@ -96,7 +139,7 @@ ${LIB}/temp/empty.c:
 # the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt
 
 # Lake archive timestamps may be stale due to caching; use .trace files for rebuild decisions
-ifeq "${USE_LAKE}" "ON"
+ifneq "${STAGE}" "0"
 $(OUTLIB)/libInit_shared$(SO): ${LIB}/lean/libInit.a.export.trace ${LIB}/lean/libStd.a.export.trace
 $(OUTLIB)/libleanshared$(SO): ${LIB}/lean/libLean.a.export.trace
 $(OUTLIB)/libLake_shared$(SO): ${LIB}/lean/libLean.a.export.trace ${LIB}/lean/libLake.a.export.trace
@@ -156,10 +199,10 @@ else
 	$(LEANC_SH) -shared -o $(OUTLIB)/libleanshared_2$(SO) ${LIB}/temp/empty.c ${LEANSHARED_2_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
 ifeq "${CMAKE_SYSTEM_NAME}" "Darwin"
 	$(LEANC_SH) -shared -o $@ \
-	  ${LIB}/temp/Lean.*o.export -Wl,-force_load,${LIB}/temp/libleanshell.a -lInit -lStd -lLean -lleancpp ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
+	  ${LIB}/temp/Lean.*o.export -Wl,-force_load,${LIB}/temp/libleanshell.a ${LIB}/lean/libInit.a.export ${LIB}/lean/libStd.a.export ${LIB}/lean/libLean.a.export ${LIB}/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
 else
 	$(LEANC_SH) -shared -o $@ \
-	  -Wl,--whole-archive ${LIB}/temp/Lean.*o.export ${LIB}/temp/libleanshell.a -Wl,--no-whole-archive -Wl,--start-group -lInit -lStd -lLean -lleancpp -Wl,--end-group ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
+	  -Wl,--whole-archive ${LIB}/temp/Lean.*o.export ${LIB}/temp/libleanshell.a -Wl,--no-whole-archive -Wl,--start-group ${LIB}/lean/libInit.a.export ${LIB}/lean/libStd.a.export ${LIB}/lean/libLean.a.export ${LIB}/lean/libleancpp.a -Wl,--end-group ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
 endif
 endif
 ifeq "${STRIP_BINARIES}" "ON"
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index e44444704908..c79ca3152fd0 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -24,7 +24,7 @@ options get_default_options() {
     opts = opts.update({"pp", "rawOnError"}, true);
 
     // Temporary, core-only flags for editing (i.e. must be part of stage0/bin/lean). Must be synced
-    // with `LEAN_EXTRA_MAKE_OPTS` build flags in src/CMakeLists.txt.
+    // with `LEAN_EXTRA_OPTS` build flags in src/CMakeLists.txt.
     opts = opts.update({"backward", "do", "legacy"}, false);
 #endif
     return opts;
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index fd2dfa2ae3e7..d815a6f68c60 100644
--- a/tests/CMakeLists.txt
+++ b/tests/CMakeLists.txt
@@ -296,7 +296,6 @@ add_test_pile(misc_bench *.sh BENCH PART2)
 add_test_pile(server *.lean)
 add_test_pile(server_interactive *.lean)
 
-add_test_dir(../doc/examples/compiler)
 add_test_dir(bench/build BENCH PART1)
 add_test_dir(bench/mvcgen/sym BENCH PART2)
 add_test_dir(bench/size BENCH PART1)
diff --git a/tests/playground/webserver/README.md b/tests/playground/webserver/README.md
index 783a7c785900..883f18435063 100644
--- a/tests/playground/webserver/README.md
+++ b/tests/playground/webserver/README.md
@@ -1,9 +1,9 @@
 Example of a super-simple web server using custom syntax for registering routes and emitting HTML
 
-Compile with `leanmake bin` to get the `./build/bin/Webserver` executable listening on stdin and
-responding on stdout:
+Compile with `lean --c=Webserver.c Webserver.lean && leanc -o Webserver Webserver.c` to get the
+`./Webserver` executable listening on stdin and responding on stdout:
 ```bash
-$ echo "GET /greet/me HTTP/1.1" | ./build/bin/Webserver
+$ echo "GET /greet/me HTTP/1.1" | ./Webserver
 HTTP/1.1 200 OK
 Content-Type: text/html
 Content-Length: 19
@@ -12,5 +12,5 @@ Content-Length: 19
 ```
 Use with netcat to test in a browser at http://localhost:1234:
 ```bash
-bash -c 'coproc nc -lp 1234; ./build/bin/Webserver <&${COPROC[0]} >&${COPROC[1]}'
+bash -c 'coproc nc -lp 1234; ./Webserver <&${COPROC[0]} >&${COPROC[1]}'
 ```