diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 0120f18bdb..bf69d6d5dd 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -410,7 +410,8 @@ jobs:
         run: |
           cd build
           ulimit -c unlimited # coredumps
-          make update-stage0 && make -j4
+          # clean rebuild in case of Makefile changes
+          make update-stage0 && rm -rf ./stage* && make -j4
         if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false'
       - name: CCache stats
         run: ccache -s
diff --git a/src/lean.mk.in b/src/lean.mk.in
index 9fd1cef9fd..d6ed3e021a 100644
--- a/src/lean.mk.in
+++ b/src/lean.mk.in
@@ -34,7 +34,12 @@ SRCS = $(shell find $(PKG) $(PKG).lean $(EXTRA_SRC_ROOTS) -name '*.lean' 2> /dev
 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/
+REL_OS = $(patsubst %.c,%.o,$(shell cd $(C_OUT); find $(PKG) $(PKG).c -name '*.c' 2> /dev/null))
+else
 REL_OS = $(patsubst %.lean,%.o,$(shell find $(PKG) $(PKG).lean -name '*.lean' 2> /dev/null))
+endif
 
 SHELL = /usr/bin/env bash -euo pipefail
 
diff --git a/stage0/src/lean.mk.in b/stage0/src/lean.mk.in
index 928c1e5d0a..d6ed3e021a 100644
--- a/stage0/src/lean.mk.in
+++ b/stage0/src/lean.mk.in
@@ -26,15 +26,19 @@ 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 -name '*.lean' 2> /dev/null)
+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/
 REL_OS = $(patsubst %.c,%.o,$(shell cd $(C_OUT); find $(PKG) $(PKG).c -name '*.c' 2> /dev/null))
 else
-REL_OS = $(SRCS:.lean=.o)
+REL_OS = $(patsubst %.lean,%.o,$(shell find $(PKG) $(PKG).lean -name '*.lean' 2> /dev/null))
 endif
 
 SHELL = /usr/bin/env bash -euo pipefail
@@ -43,7 +47,7 @@ SHELL = /usr/bin/env bash -euo pipefail
 # Disable all default make rules
 .SUFFIXES:
 
-all: $(OBJS)
+objs: $(OBJS)
 
 bin: $(BIN_OUT)/$(BIN_NAME)
 
@@ -61,20 +65,19 @@ $(TEMP_OUT)/%.depend: %.lean | $(OLEAN_OUT)/$(PKG)
 # 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)/$(<:.lean=.olean): $$deps > $@
+  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)
-ifndef LLVM
-	$(LEAN) $(LEAN_OPTS) -o "$@" -i "$(OLEAN_OUT)/$*.ilean" --c="$(TEMP_OUT)/$*.c.tmp" $<
+	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"
-else
-	$(LEAN) $(LEAN_OPTS) -o "$@" -i "$(OLEAN_OUT)/$*.ilean" --c="$(TEMP_OUT)/$*.c.tmp" --bc="$(TEMP_OUT)/$*.bc.tmp" $<
-	@mv "$(TEMP_OUT)/$*.c.tmp" "$(C_OUT)/$*.c"
+ifdef LLVM
 	@mv "$(TEMP_OUT)/$*.bc.tmp" "$(BC_OUT)/$*.bc"
 endif