diff --git a/1-runs/run-2024-04-01---15-52-tcg40/run-lean-stage-bench-worker.sh b/1-runs/run-2024-04-01---15-52-tcg40/run-lean-stage-bench-worker.sh new file mode 100644 index 000000000000..fb8043042f02 --- /dev/null +++ b/1-runs/run-2024-04-01---15-52-tcg40/run-lean-stage-bench-worker.sh @@ -0,0 +1,81 @@ +#!/usr/bin/env bash +set -o xtrace +set -e + +COMMIT_TO_BENCH="2024-03-31---19-38---tcg40" + +# -------- + +EXPERIMENTDIR=$(pwd) +echo "pwd: $EXPERIMENTDIR" +DATE=$(date) +echo "date: $DATE" +MACHINE=$(uname -a) +echo "machine: $MACHINE" +echo "git status: $(git status --short)" +echo "git commit: $(git rev-parse HEAD)" +ROOT=$(git rev-parse --show-toplevel) +echo "root folder: $ROOT" +echo "out folder: $OUTFOLDER" + +if [ "$(uname -s)" = "Darwin" ]; then + TIME="gtime" +else + TIME="command time" +fi +echo "time: $TIME" +$TIME -v echo "time" + +rm *.txt -i || true +rm *.csv -i || true +rm -rf builds -I || true + + +COMMITS=("$COMMIT_TO_BENCH" "2024-borrowing-benching-baseline" ) +KINDS=("reuse" "noreuse") + +for tag in "${COMMITS[@]}"; do + git show --format="%H %ad" --date=short $tag -q +done + +# Ask if script should proceed +read -p "Do you want to proceed? (y/n) " -n 1 -r +echo # Move to a new line +if [[ $REPLY =~ ^[Yy]$ ]]; then + echo "Proceeding to run..." +else + echo "Run aborted." + exit 1 +fi + +mkdir -p $EXPERIMENTDIR/builds/ + +git clone --depth 1 git@github.com:opencompl/lean4.git --branch 2024-borrowing-benching-baseline $EXPERIMENTDIR/builds/baseline-src-code + +for i in {0..1}; do + echo "@@@ ${KINDS[i]} BUILD @@@" + curl -d "Started[${KINDS[i]}]. run:$EXPERIMENTDIR. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 + mkdir -p $EXPERIMENTDIR/builds/ + git clone --depth 1 git@github.com:opencompl/lean4.git --branch ${COMMITS[i]} $EXPERIMENTDIR/builds/${KINDS[i]} --reference /anfs/bigdisc/sb2743/24-borrowing/lean4.reference + mkdir -p $EXPERIMENTDIR/builds/${KINDS[i]}/build/release/ + cd $EXPERIMENTDIR/builds/${KINDS[i]}/build/release/ + # output log name from stage3 build. + CSVNAME="${KINDS[i]}.stage3.csv" + PROFILE_FILE=$EXPERIMENTDIR/$CSVNAME + + cmake ../../ \ + -DCCACHE=OFF \ + -DRUNTIME_STATS=ON \ + -DCMAKE_BUILD_TYPE=Release \ + -DLEAN_RESEARCH_COMPILER_PROFILE_CSV_PATH=$PROFILE_FILE + make update-stage0 + rm -rf ../../src/; cp -r $EXPERIMENTDIR/builds/baseline-src-code/src ../../ + git checkout -- ../../src/runtime ../../src/include/lean/lean.h ../../src/library/compiler/ir_interpreter.h + + make -j10 stage2 + rm $EXPERIMENTDIR/$CSVNAME || true + $TIME -v make -j10 stage3 2>&1 | tee "$EXPERIMENTDIR/time-${KINDS[i]}-stage3.txt" + cp "$EXPERIMENTDIR/$CSVNAME" "$EXPERIMENTDIR/${KINDS[i]}.stage3-compile.csv" + (cd $EXPERIMENTDIR/builds/${KINDS[i]}/build/release/stage3 && (ctest -E handleLocking -j32 --output-on-failure 2>&1 | tee "$EXPERIMENTDIR/ctest-${KINDS[i]}-stage3.txt")) || true + curl -d "Done[${KINDS[i]}]. run:$EXPERIMENTDIR. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 +done; diff --git a/1-runs/run-2024-04-01---15-52-tcg40/run-lean-stage-bench-wrapper.sh b/1-runs/run-2024-04-01---15-52-tcg40/run-lean-stage-bench-wrapper.sh new file mode 100755 index 000000000000..1649ba0d8833 --- /dev/null +++ b/1-runs/run-2024-04-01---15-52-tcg40/run-lean-stage-bench-wrapper.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +bash run-lean-stage-bench-worker.sh 2>&1 | tee log.txt + diff --git a/1-runs/run-2024-04-01---15-52-tcg40/run-stage3-recompile-worker.sh b/1-runs/run-2024-04-01---15-52-tcg40/run-stage3-recompile-worker.sh new file mode 100644 index 000000000000..06688be0a2eb --- /dev/null +++ b/1-runs/run-2024-04-01---15-52-tcg40/run-stage3-recompile-worker.sh @@ -0,0 +1,39 @@ +#!/usr/bin/env bash +set -o xtrace +set -e + +# -------- + +EXPERIMENTDIR=$(pwd) +echo "pwd: $EXPERIMENTDIR" +DATE=$(date) +echo "date: $DATE" +MACHINE=$(uname -a) +echo "machine: $MACHINE" +echo "git status: $(git status --short)" +echo "git commit: $(git rev-parse HEAD)" +ROOT=$(git rev-parse --show-toplevel) +echo "root folder: $ROOT" +echo "out folder: $OUTFOLDER" + +if [ "$(uname -s)" = "Darwin" ]; then + TIME="gtime" +else + TIME="command time" +fi +echo "time: $TIME" +$TIME -v echo "time" + +KINDS=("reuse" "noreuse") + +for i in {0..1}; do + curl -d "Start[stage3-recompile-${KINDS[i]}]. run:$EXPERIMENTDIR. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 + rm -rf $EXPERIMENTDIR/builds/${KINDS[i]}/build/release/ + mkdir -p $EXPERIMENTDIR/builds/${KINDS[i]}/build/release/ + cd $EXPERIMENTDIR/builds/${KINDS[i]}/build/release/ + make -j10 stage2 + CSVNAME="${KINDS[i]}.stage3.csv" + rm $EXPERIMENTDIR/$CSVNAME # cleanup old csv. + $TIME -v make -j10 stage3 2>&1 | tee $EXPERIMENTDIR/time-rebuild-stdlib-stage3-${KINDS[i]}.txt # make new CSV. + curl -d "Done[stage3-recompile-${KINDS[i]}]. run:$EXPERIMENTDIR. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 +done; diff --git a/1-runs/run-2024-04-01---15-52-tcg40/run-stage3-recompile-wrapper.sh b/1-runs/run-2024-04-01---15-52-tcg40/run-stage3-recompile-wrapper.sh new file mode 100755 index 000000000000..7e07b5002794 --- /dev/null +++ b/1-runs/run-2024-04-01---15-52-tcg40/run-stage3-recompile-wrapper.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +bash ./run-stage3-recompile-worker.sh 2>&1 | tee -a log.txt + diff --git a/1-runs/run-2024-04-01---15-52-tcg40/run-stdlib-recompile-worker.sh b/1-runs/run-2024-04-01---15-52-tcg40/run-stdlib-recompile-worker.sh new file mode 100644 index 000000000000..d35304ff22fd --- /dev/null +++ b/1-runs/run-2024-04-01---15-52-tcg40/run-stdlib-recompile-worker.sh @@ -0,0 +1,39 @@ +#!/usr/bin/env bash +set -o xtrace +set -e + +# -------- + +EXPERIMENTDIR=$(pwd) +echo "pwd: $EXPERIMENTDIR" +DATE=$(date) +echo "date: $DATE" +MACHINE=$(uname -a) +echo "machine: $MACHINE" +echo "git status: $(git status --short)" +echo "git commit: $(git rev-parse HEAD)" +ROOT=$(git rev-parse --show-toplevel) +echo "root folder: $ROOT" +echo "out folder: $OUTFOLDER" + +if [ "$(uname -s)" = "Darwin" ]; then + TIME="gtime" +else + TIME="command time" +fi +echo "time: $TIME" +$TIME -v echo "time" + +KINDS=("reuse" "noreuse") + +for i in {0..1}; do + curl -d "Start[stdlib-recompile-${KINDS[i]}]. run:$EXPERIMENTDIR. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 + touch $EXPERIMENTDIR/builds/${KINDS[i]}/src/Init/Prelude.lean # recompile stdlib. + + cd $EXPERIMENTDIR/builds/${KINDS[i]}/build/release/ + make -j10 stage2 + CSVNAME="${KINDS[i]}.stage3.csv" + rm $EXPERIMENTDIR/$CSVNAME + $TIME -v make -j10 stage3 2>&1 | tee $EXPERIMENTDIR/time-rebuild-stdlib-stage3-${KINDS[i]}.txt + curl -d "Done[stdlib-recompile-${KINDS[i]}]. run:$EXPERIMENTDIR. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 +done; diff --git a/1-runs/run-2024-04-01---15-52-tcg40/run-stdlib-recompile-wrapper.sh b/1-runs/run-2024-04-01---15-52-tcg40/run-stdlib-recompile-wrapper.sh new file mode 100755 index 000000000000..19bd7e886e3b --- /dev/null +++ b/1-runs/run-2024-04-01---15-52-tcg40/run-stdlib-recompile-wrapper.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +bash ./run-stdlib-recompile-worker.sh 2>&1 | tee -a log.txt + diff --git a/1-runs/run-2024-04-01---15-52-tcg40/speedcenter-worker.sh b/1-runs/run-2024-04-01---15-52-tcg40/speedcenter-worker.sh new file mode 100644 index 000000000000..e6047d93de13 --- /dev/null +++ b/1-runs/run-2024-04-01---15-52-tcg40/speedcenter-worker.sh @@ -0,0 +1,82 @@ +#!/usr/bin/env bash +set -o xtrace +set -e + +COMMIT_TO_BENCH="2024-03-31---19-38---tcg40" + +# -------- + +EXPERIMENTDIR=$(pwd) +echo "pwd: $EXPERIMENTDIR" +DATE=$(date) +echo "date: $DATE" +MACHINE=$(uname -a) +echo "machine: $MACHINE" +echo "git status: $(git status --short)" +echo "git commit: $(git rev-parse HEAD)" +ROOT=$(git rev-parse --show-toplevel) +echo "root folder: $ROOT" +echo "out folder: $OUTFOLDER" + +if [ "$(uname -s)" = "Darwin" ]; then + TIME="gtime" +else + TIME="command time" +fi +echo "time: $TIME" +$TIME -v echo "time" + +COMMITS=("2024-borrowing-benching-baseline" "$COMMIT_TO_BENCH") +KINDS=("noreuse" "reuse") + +run_benchmark_for_kind() { + # argument: kind + local kind="${KINDS[i]}" + local BENCHMARKS=("binarytrees.lean" + # binarytrees.st + "const_fold.lean" + "deriv.lean" + "liasolver.lean" + # parser.lean + # reduceMatch.lean + "qsort.lean" + "rbmap_checkpoint.lean" + "rbmap_fbip.lean" + "rbmap.lean" + "unionfind.lean") + # link lean tooolchain + # # https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/elan.20toolchain.20link.3A.20three.20hyphens.20becomes.20colon.3F/near/430447189 + # # Lean toolchain does not like having three dash, so for now, just name it based on KINDS. + LEAN_TOOLCHAIN="$kind" + # TODO: elan does not like '---' in folder name? + elan toolchain link "$LEAN_TOOLCHAIN" "$EXPERIMENTDIR/builds-speedcenter/$kind/build/release/stage2" + cd "$EXPERIMENTDIR/builds-speedcenter/$kind/tests/bench/" + elan override set "$LEAN_TOOLCHAIN" # set override for temci + mkdir -p "$EXPERIMENTDIR/outputs/" + for benchmark in "${BENCHMARKS[@]}"; do + RESEARCH_LEAN_RUNTIME_ALLOCATOR_LOG=./log.txt ./test_single.sh "${benchmark}" + # run benchmark, write result to CSV file. + while read -r line; do echo "$benchmark,$line"; done < log.txt >> "$EXPERIMENTDIR/outputs/benchmarks-allocator-log-$kind.csv" + done; +} + +for i in {0..1}; do + curl -d "Start[MICROBENCHMARK-RUNTIME-ALLOCATOR-LOG-${KINDS[i]}]. run:$EXPERIMENTDIR. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 + mkdir -p builds-speedcenter + # clone + git clone --depth 1 git@github.com:opencompl/lean4.git --branch "${COMMITS[i]}" "$EXPERIMENTDIR/builds-speedcenter/${KINDS[i]}" + # build + cd "$EXPERIMENTDIR/builds-speedcenter/${KINDS[i]}/build/release/" + # build stage2, with ccache, since we are only interested in benching the microbenchmarks + cmake ../../ \ + -DCCACHE=ON \ + -DRUNTIME_STATS=ON \ + -DCMAKE_BUILD_TYPE=Release + make -j20 stage2 + # run ctest to make sure our toolchain is legit. + cd "$EXPERIMENTDIR/builds-speedcenter/${KINDS[i]}/build/release/stage2" && \ + (ctest -E handleLocking -j32 --output-on-failure 2>&1 | tee "$EXPERIMENTDIR/outputs/ctest-speedcenter-${KINDS[i]}-stage2.txt") + run_benchmark_for_kind "${KINDS[i]}" + + curl -d "Done[MICROBENCHMARK-RUNTIME-ALLOCATOR-LOG-${KINDS[i]}]. run:$EXPERIMENTDIR. machine:$(uname -a)." ntfy.sh/xISSztEV8EoOchM2 +done; diff --git a/1-runs/run-2024-04-01---15-52-tcg40/speedcenter-wrapper.sh b/1-runs/run-2024-04-01---15-52-tcg40/speedcenter-wrapper.sh new file mode 100755 index 000000000000..01fd135e6ad4 --- /dev/null +++ b/1-runs/run-2024-04-01---15-52-tcg40/speedcenter-wrapper.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +bash ./speedcenter-worker.sh 2>&1 | tee log.txt +