chore: speedcenter: benchmark actual, parallel stdlib build

src/lean.mk.in

@@ -68,13 +68,21 @@ ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Building $<"
 endif
 	@mkdir -p "$(@D)"
+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)
+endif
 
 $(BIN_OUT)/$(BIN_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(BIN_OUT)
 ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Linking $@"
 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)
+endif
 
 $(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(LIB_OUT)
 	@rm -f $@

src/stdlib.make.in

@@ -1,7 +1,7 @@
 SHELL := /usr/bin/env bash -euo pipefail
 
 # MORE_DEPS: rebuild the stdlib whenever the compiler has changed
-LEANMAKE_OPTS=\
+LEANMAKE_OPTS+=\
 	OUT="${LIB}"\
 	LIB_OUT="${LIB}/lean"\
 	OLEAN_OUT="${LIB}/lean"\

stage0/src/lean.mk.in

@@ -68,13 +68,21 @@ ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Building $<"
 endif
 	@mkdir -p "$(@D)"
+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)
+endif
 
 $(BIN_OUT)/$(BIN_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(BIN_OUT)
 ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Linking $@"
 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)
+endif
 
 $(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(LIB_OUT)
 	@rm -f $@

stage0/src/stdlib.make.in

@@ -1,7 +1,7 @@
 SHELL := /usr/bin/env bash -euo pipefail
 
 # MORE_DEPS: rebuild the stdlib whenever the compiler has changed
-LEANMAKE_OPTS=\
+LEANMAKE_OPTS+=\
 	OUT="${LIB}"\
 	LIB_OUT="${LIB}/lean"\
 	OLEAN_OUT="${LIB}/lean"\

tests/bench/speedcenter.exec.velcom.yaml

@@ -10,11 +10,19 @@
       rusage_properties: ['maxrss']
   run_config:
     <<: *time
-    cwd: ../../src
+    cwd: ../../build/release/stage0
     cmd: |
-      bash -c "find . -name '*.lean' -exec lean --stats -Dprofiler=true -Dprofiler.threshold=9999 {} \; 2>&1 | ../tests/bench/accumulate_profile.py"
-    max_runs: 3
+      find lib/lean ! -name libleancpp.a -delete
+      # for C profiling
+      #PROFILE=1 CCACHE_DISABLE=1
+      LEANMAKE_OPTS=LEAN_OPTS="--stats\ -Dprofiler=true\ -Dprofiler.threshold=9999" make -O -j5 make_stdlib 2>&1 > /dev/null | ../../../tests/bench/accumulate_profile.py
+    max_runs: 2
     parse_output: true
+  # Warmup. Somehow ccache doesn't reuse the cache from the original build? Weird.
+  build_config:
+    cmd: |
+      find lib/lean/ ! -name libleancpp.a -type f -delete
+      make -j5 make_stdlib
 - attributes:
     description: stdlib size
     tags: [deterministic, fast]

tests/bench/speedcenter.exec.yaml

@@ -9,11 +9,19 @@
       #  properties: ['cache-misses', 'wall-clock']
   run_config:
     <<: *time
-    cwd: ../../src
+    cwd: ../../build/release/stage0
     cmd: |
-      bash -c "find . -name '*.lean' -exec lean --stats -Dprofiler=true -Dprofiler.threshold=9999 {} \; 2>&1 | ../tests/bench/accumulate_profile.py"
-    max_runs: 3
+      find lib/lean ! -name libleancpp.a -delete
+      # for C profiling
+      #PROFILE=1 CCACHE_DISABLE=1
+      LEANMAKE_OPTS=LEAN_OPTS="--stats\ -Dprofiler=true\ -Dprofiler.threshold=9999" make -O -j5 make_stdlib 2>&1 > /dev/null | ../../../tests/bench/accumulate_profile.py
+    max_runs: 2
     parse_output: true
+  # Warmup. Somehow ccache doesn't reuse the cache from the original build? Weird.
+  build_config:
+    cmd: |
+      find lib/lean/ ! -name libleancpp.a -type f -delete
+      make -j5 make_stdlib
 - attributes:
     description: stdlib size
     tags: [deterministic, fast]