From 015903f055e5daae5a22d60d5f38fc20b31ea7a1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 21 Aug 2020 16:03:37 +0200 Subject: [PATCH] chore: speedcenter: benchmark actual, parallel stdlib build --- src/lean.mk.in | 8 ++++++++ src/stdlib.make.in | 2 +- stage0/src/lean.mk.in | 8 ++++++++ stage0/src/stdlib.make.in | 2 +- tests/bench/speedcenter.exec.velcom.yaml | 14 +++++++++++--- tests/bench/speedcenter.exec.yaml | 14 +++++++++++--- 6 files changed, 40 insertions(+), 8 deletions(-) diff --git a/src/lean.mk.in b/src/lean.mk.in index e8052f2cee..6a325adb0c 100644 --- a/src/lean.mk.in +++ b/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 $@ diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 94be64e950..0b225665c5 100644 --- a/src/stdlib.make.in +++ b/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"\ diff --git a/stage0/src/lean.mk.in b/stage0/src/lean.mk.in index e8052f2cee..6a325adb0c 100644 --- a/stage0/src/lean.mk.in +++ b/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 $@ diff --git a/stage0/src/stdlib.make.in b/stage0/src/stdlib.make.in index 94be64e950..0b225665c5 100644 --- a/stage0/src/stdlib.make.in +++ b/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"\ diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 1757f63fcf..4748bc4f7d 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/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] diff --git a/tests/bench/speedcenter.exec.yaml b/tests/bench/speedcenter.exec.yaml index 70a479c950..297ceceefb 100644 --- a/tests/bench/speedcenter.exec.yaml +++ b/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]