blob: 637cd6c80dde3e99531ae87ca32a390c1fecd9d4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
#!/usr/bin/env bash
# vim: sw=2 et
set -euo pipefail
fail() {
echo "ERROR: $*" >&2
exit 1
}
GHC_ORIGIN="git@gitlab.haskell.org:ghc/ghc.git"
# Check that private key is available (Set on all GitLab protected branches).
if [ "$PERF_NOTE_KEY" = "" ]; then
echo "Not pushing performance git notes: PERF_NOTE_KEY is not set."
exit 0
fi
# TEST_ENV must be set.
if [ "$TEST_ENV" = "" ]; then
fail "Not pushing performance git notes: TEST_ENV must be set."
fi
# Setup ssh keys.
mkdir -p ~/.ssh
echo "ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAABAQC94vDmRcDXPTuZktLvMFXHD2X6H2GEdnP+7VO0QbwNje9jsPLpofQRHJKXG/9sm0a6NT9qXt9eccRNklP0AkW36LcNRni7ji8NxlrE9ASuXGqa4TTk83pOLFCzWmdcdVIxz3bxPfa/ECmyRmTxp3+mTW0eJrUEdVwprAieNoTH+ZLyDmq+IfAD5239ea+gAZzfCy5WcTbsSXOOJEAZKqqfzyog18agptzAWu/tCfzvyiGlkoQj+PE1MMEfnmWQC8d2bOhC6kQZZtPrGNhFU75JifYGT7y0e1EVa5bhqcZZ9cdGSli1S8T9MpSimVII6iZOFdho3+shbUX3ObagUl09 ben@ben-laptop" > ~/.ssh/perf_rsa.pub
echo $PERF_NOTE_KEY > ~/.ssh/perf_rsa
ssh-add ~/.ssh/perf_rsa
# Check that git notes don't already exist.
# This is a percausion as we reset refs/notes/perf and we want to avoid data loss.
# TODO CHANGE ME BEFORE MERGE
REF="perf_tmp"
if [ $(git notes --ref=$REF list | wc -l) -ne 0 ]
then
fail "Found an existing git note. Expected no git note."
fi
# Assert that the METRICS_FILE exists and can be read.
if [ "$METRICS_FILE" = "" ] || ! [ -r $METRICS_FILE ]
then
fail "Metrics file not found: $METRICS_FILE"
fi
# Reset the git notes and append the metrics file to the notes, then push and return the result.
# This is favoured over a git notes merge as it avoids potential data loss/duplication from the merge strategy.
function reset_append_note_push {
git fetch -f $GHC_ORIGIN refs/notes/$REF:refs/notes/$REF || true
echo "git notes --ref=$REF append -F $METRICS_FILE HEAD"
git notes --ref=$REF append -F $METRICS_FILE HEAD
git push $GHC_ORIGIN refs/notes/$REF
}
# Push the metrics file as a git note. This may fail if another task pushes a note first. In that case
# the latest note is fetched and appended.
MAX_RETRY=20
until reset_append_note_push || [ $MAX_RETRY -le 0 ]
do
((MAX_RETRY--))
echo ""
echo "Failed to push git notes. Fetching, appending, and retrying... $MAX_RETRY retries left."
done
|
