From fb2ec54b60e62ab7cb00cccbc989b6ef8e40e25c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 14 Mar 2024 16:14:37 +0100
Subject: [PATCH] chore: build `Lean` `.o`s in parallel to rest of core (#3682)

Previously, we only did `Init/*.{o,olean}+Lean/*.olean` in parallel
---
 src/lean.mk.in     | 15 +++++++++------
 src/stdlib.make.in |  2 +-
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/lean.mk.in b/src/lean.mk.in
index 60fc1241a6..98084ffea8 100644
--- a/src/lean.mk.in
+++ b/src/lean.mk.in
@@ -36,9 +36,12 @@ 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))
+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
-REL_OS = $(patsubst %.lean,%.o,$(shell find $(PKG) $(PKG).lean -name '*.lean' 2> /dev/null))
+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
@@ -47,7 +50,7 @@ SHELL = /usr/bin/env bash -euo pipefail
 # Disable all default make rules
 .SUFFIXES:
 
-objs: $(OBJS)
+objs: $(OBJS) $(ALL_NAT_OBJS)
 
 bin: $(BIN_OUT)/$(BIN_NAME)
 
@@ -111,7 +114,7 @@ else
 	$(LEANC) -c -o $@ $< $(LEANC_OPTS)
 endif
 
-$(BIN_OUT)/$(BIN_NAME): $(addprefix $(TEMP_OUT)/,$(REL_OS)) | $(BIN_OUT)
+$(BIN_OUT)/$(BIN_NAME): $(NAT_OBJS) | $(BIN_OUT)
 ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Linking $@"
 endif
@@ -124,13 +127,13 @@ else
 endif
 
 ifeq (@CMAKE_SYSTEM_NAME@, Windows)
-$(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(REL_OS)) | $(LIB_OUT)
+$(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
 else
-$(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(REL_OS)) | $(LIB_OUT)
+$(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 $@ $^
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 2713af7886..ef98b4a368 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -35,7 +35,7 @@ endif
 Init:
 	@mkdir -p "${LIB}/lean/Lean" "${LIB}/lean/Lake"
 # Use `+` to use the Make jobserver with `leanmake` for parallelized builds
-# Build .oleans of downstream libraries as well for better parallelism
+# Build `.olean/.o`s of downstream libraries as well for better parallelism
 	+"${LEAN_BIN}/leanmake" objs lib PKG=Init $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING \
 	  EXTRA_SRC_ROOTS="Lean Lean.lean"