diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6fa1e6ad21..f809d3e7b2 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -533,10 +533,11 @@ else()
 endif()
 install(FILES ${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a DESTINATION lib/lean)
 
+# 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")
+
 # make stdlib using previous stage
 if(PREV_STAGE)
-  # 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 "${PREV_STAGE}/bin")
   # ...and Make doesn't like absolute Windows paths either
   # (also looks nicer in the build log)
   file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
@@ -549,6 +550,7 @@ if(PREV_STAGE)
     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
     # for a parallelized nested build, but CMake doesn't let us do that.
+    # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make)
 
   add_library(Init STATIC IMPORTED)
diff --git a/src/lean.mk.in b/src/lean.mk.in
index 6a325adb0c..8f583855dc 100644
--- a/src/lean.mk.in
+++ b/src/lean.mk.in
@@ -10,6 +10,8 @@ ifndef PKG
   endif
 endif
 
+LEAN = lean
+LEANC = leanc
 OUT = build
 OLEAN_OUT = $(OUT)
 TEMP_OUT = $(OUT)/temp
@@ -47,14 +49,14 @@ $(TEMP_OUT)/%.depend: %.lean | $(OLEAN_OUT)/$(PKG)
 	@mkdir -p "$(TEMP_OUT)/$(*D)"
 # use separate assignment to ensure failure propagation
 # convert path separators and newlines on Windows
-	@deps=`lean --deps $< | tr '\\\\' / | tr -d '\\r'`; echo $(OLEAN_OUT)/$(<:.lean=.olean): $$deps > $@
+	@deps=`$(LEAN) --deps $< | tr '\\\\' / | tr -d '\\r'`; echo $(OLEAN_OUT)/$(<:.lean=.olean): $$deps > $@
 
 $(OLEAN_OUT)/%.olean: %.lean $(TEMP_OUT)/%.depend $(MORE_DEPS)
 ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Building $<"
 endif
 	@mkdir -p $(OLEAN_OUT)/$(*D)
-	lean $(LEAN_OPTS) -o "$@" --c="$(TEMP_OUT)/$*.c.tmp" $<
+	$(LEAN) $(LEAN_OPTS) -o "$@" --c="$(TEMP_OUT)/$*.c.tmp" $<
 # create the .c file atomically
 	mv "$(TEMP_OUT)/$*.c.tmp" "$(TEMP_OUT)/$*.c"
 # make sure the .olean file is newer than the .depend file to prevent infinite make cycles
@@ -71,7 +73,7 @@ endif
 ifdef PROFILE
 	\time -f "%U %S" leanc -c -o $@ $< $(LEANC_OPTS) 2>&1 > /dev/null | awk '{ printf "C compilation %fs\n", $$1 + $$2 }' > /dev/stderr
 else
-	leanc -c -o $@ $< $(LEANC_OPTS)
+	$(LEANC) -c -o $@ $< $(LEANC_OPTS)
 endif
 
 $(BIN_OUT)/$(BIN_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(BIN_OUT)
@@ -81,7 +83,7 @@ endif
 ifdef PROFILE
 	\time -f "%U %S" leanc -o "$@" -x none $^ $(LINK_OPTS) 2>&1 > /dev/null | awk '{ printf "C linking %fs\n", $$1 + $$2 }' > /dev/stderr
 else
-	leanc -o "$@" -x none $^ $(LINK_OPTS)
+	$(LEANC) -o "$@" -x none $^ $(LINK_OPTS)
 endif
 
 $(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(LIB_OUT)
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 59f6d88091..36f497f1e0 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -2,11 +2,12 @@ SHELL := /usr/bin/env bash -euo pipefail
 
 # MORE_DEPS: rebuild the stdlib whenever the compiler has changed
 LEANMAKE_OPTS+=\
+  LEAN="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
 	OUT="${LIB}"\
 	LIB_OUT="${LIB}/lean"\
 	OLEAN_OUT="${LIB}/lean"\
 	LEANC_OPTS="${LEANC_OPTS}"\
-	MORE_DEPS="${LEAN_BIN}/lean${CMAKE_EXECUTABLE_SUFFIX}"\
+	MORE_DEPS="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\
 	CMAKE_LIKE_OUTPUT=1
 
 stdlib: