Merge branch 'master' into 'master'

Change `buildjob` to accomodate external timing runners

See merge request !2

README.md

@@ -151,7 +151,7 @@ this.  The variable should *not* be protected because we do timing measurements
 on all branches, not just `master`!
 
 You also need to enable the `coop-timing` runner for your project. Again this
-needs to be done by an admit.
+needs to be done by an admin.
 
 Behind the scenes, the data is sent to our
 [custom webhook](https://gitlab.mpi-sws.org/iris/ci-timing-webhook), which runs

buildjob

@@ -19,8 +19,8 @@ set -eo pipefail
 ##   commit as a new package on opam when done.  Requires the
 ##   $OPAM_UPDATE_SECRET variable to be set.  This only happens if the current
 ##   branch is `master`.
-## - $TIMING_PROJECT, $TIMING_SECRET: When running on the `coop-timing` runner,
-##   submit timing information to coq-speed with the given project name.
+## - $TIMING_PROJECT, $TIMING_SECRET: When running on a runner with the `fp-timing`
+##   tag, submit timing information to coq-speed with the given project name.
 ##   $TIMING_PROJECT defaults to the repository name. Reqires the $TIMING_SECRET
 ##   variable to be set. The timing "branch" is determined by $CI_COMMIT_BRANCH
 ##   and the "config" by the job name, but that can be overwritten by setting
@@ -34,7 +34,16 @@ set -eo pipefail
 
 status "[buildjob] Using CI branch $(cd ci && git rev-parse --abbrev-ref HEAD) ($(cd ci && git rev-parse HEAD))"
 status "[buildjob] Pipeline source: $CI_PIPELINE_SOURCE; commit branch (empty for MRs): $CI_COMMIT_BRANCH"
-if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" && -n "$TIMING_AD_HOC_ID" ]]; then
+
+# Check if CI_RUNNER_TAGS contains "fp-timing". CI_RUNNER_TAGS is in JSON format:
+# a comma-separated list, each item in quotes, delimited by [ and ].
+if echo "${CI_RUNNER_TAGS:1:-1}" | tr , \n | grep '^"fp-timing"$' -q ; then
+    RUNNER_HAS_TIMING_TAG="true"
+else
+    RUNNER_HAS_TIMING_TAG="false"
+fi
+
+if [[ "$RUNNER_HAS_TIMING_TAG" == "true" && -n "$TIMING_AD_HOC_ID" ]]; then
     status "[buildjob] Ad-hoc timing run with ID $TIMING_AD_HOC_ID"
 fi
 
@@ -49,7 +58,7 @@ if [[ -n "$VALIDATE" ]]; then
     panic "[buildjob] Do not use the VALIDATE variable, it has been replaced by CI_COQCHK"
 fi
 
-# Parepare
+# Prepare
 . ci/prepare-opam.sh dune version 3.3.1 $OPAM_PINS # deliberately not quoted
 env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
 
@@ -57,7 +66,7 @@ if [[ -n "$MANGLE_NAMES" ]]; then
     status "[buildjob] Enabling name mangling"
     export COQEXTRAFLAGS="$COQEXTRAFLAGS -mangle-names _"
 fi
-if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" ]]; then
+if [[ "$RUNNER_HAS_TIMING_TAG" == "true" ]]; then
     export TIMECMD=$PWD/ci/perf
 fi
 # git-ignore CI-generated files (some projects look at `git status` in their CI)
@@ -82,15 +91,11 @@ if [[ -n "$DENY_WARNINGS" ]] && egrep -q "^Warning:" build-log.txt; then
 fi
 
 # maybe submit timing information
-if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" && -n "$CI_COMMIT_BRANCH" ]]; then
+if [[ "$RUNNER_HAS_TIMING_TAG" == "true" && -n "$CI_COMMIT_BRANCH" ]]; then
     # collect all information into one file
     status "[buildjob] Build performance information"
     find -name "*.v.perf" -print0 | xargs -0 cat > build-times.txt
     cat build-times.txt
-    # make sure we run on the timing machine
-    if [[ "$CI_RUNNER_TAGS" != "fp-timing" && "$CI_RUNNER_TAGS" != "[\"fp-timing\"]" ]]; then
-        panic "[buildjob] Timing jobs must be tagged with fp-timing to get the right runner (found CI_RUNNER_TAGS=$CI_RUNNER_TAGS)"
-    fi
     # check if we have the secret
     if [[ -z "$TIMING_SECRET" ]]; then
         panic "[buildjob] TIMING_SECRET variable is missing"

perf

@@ -3,6 +3,6 @@ set -e
 # Wrapper script to use perf as TIMECMD for the build.
 
 VFILE="${!#}"
-LC_ALL=C /usr/bin/time -o "$VFILE.time" -f "real: %e, user: %U, sys: %S, mem: %M kB" -- perf stat -o "$VFILE.counters" -x ';' -e instructions,cycles -- "$@"
+LC_ALL=C /usr/bin/time -o "$VFILE.time" -f "real: %e, user: %U, sys: %S, mem: %M kB" -- perf stat -o "$VFILE.counters" -x ';' -e instructions:u,cycles:u -- "$@"
 (echo "## $VFILE" && (cat "$VFILE.counters" | egrep -v '^(# .*)?$') && cat "$VFILE.time" && echo) > "$VFILE.perf"
 rm "$VFILE.counters" "$VFILE.time"