feat: add code to run run-2024-04-01---15-52-tcg40

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 [email protected]: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 [email protected]: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;

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
+

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;

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
+

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;

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
+

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 [email protected]: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;

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
+