@@ -11,6 +11,7 @@ if [[ -n "$GITHUB_RUN_ID" ]]; then
1111 LOCAL_REPO_PATH=/local/repos
1212 mkdir -p " $LOCAL_REPO_PATH "
1313 LAST_UPDATE_FILE=" $LOCAL_REPO_PATH /last-update"
14+ UPDATE_LOCK_FILE=" $LOCAL_REPO_PATH /.update.lock"
1415
1516 WORKFLOW_LOG_DIR=" /artifacts/workflow-logs/${GITHUB_RUN_ID} "
1617 NINJA_LOG_FILE=" ${WORKFLOW_LOG_DIR} /ninja-${BUILD_ARCH} ,${CROSS_ARCH} ,${BUILD_DIST} ,${BUILD_TYPE} .log"
@@ -23,35 +24,55 @@ if [[ -n "$GITHUB_RUN_ID" ]]; then
2324 echo " $( python3 - <<< ' from datetime import datetime; print(datetime.now().isoformat())' ) $event " >> " $BUILD_LOG_FILE "
2425 }
2526
26- if [[ " $BUILD_TYPE " != " *-static-*" ]]; then
27- if [ -f " $LAST_UPDATE_FILE " ] && [ $( find " $LAST_UPDATE_FILE " -mmin -180) ]; then
28- echo " Skipping git repo update because it already ran in the last three hours."
29- else
30- echo " Running git repo update."
31-
32- log " begin:repo-update"
33-
34- for repo in " fmtlib/fmt" \
35- " google/googletest" \
36- " ericniebler/range-v3" \
37- " greg7mdp/parallel-hashmap" ; do
38- reponame=$( basename " $repo " )
39- cd " $LOCAL_REPO_PATH "
40- if [ -d " $reponame " ]; then
41- cd " $reponame "
42- time git fetch
43- else
44- time git clone " https://github.com/$repo .git"
45- fi
46- done
47-
48- log " end:repo-update"
49-
50- touch " $LAST_UPDATE_FILE "
27+ retry () {
28+ local attempt=1 max=5 delay=15
29+ while true ; do
30+ if " $@ " ; then return 0; fi
31+ if [ " $attempt " -ge " $max " ]; then
32+ echo " '$* ' still failing after $attempt attempts, giving up." >&2
33+ return 1
34+ fi
35+ echo " '$* ' failed (attempt $attempt /$max ), retrying in ${delay} s..." >&2
36+ sleep " $delay "
37+ attempt=$(( attempt + 1 ))
38+ delay=$(( delay * 2 ))
39+ done
40+ }
41+
42+ REPO_LIST=(
43+ google/googletest
44+ greg7mdp/parallel-hashmap
45+ # fmtlib/fmt
46+ # ericniebler/range-v3
47+ )
48+
49+ (
50+ flock -w 900 9 || { echo " Timed out waiting for repo lock." >&2 ; exit 1; }
51+
52+ if [ -f " $LAST_UPDATE_FILE " ] && [ -n " $( find " $LAST_UPDATE_FILE " -mmin -180) " ]; then
53+ echo " Skipping git repo update because it already ran in the last three hours."
54+ exit 0
5155 fi
5256
53- export DWARFS_LOCAL_REPO_PATH=" $LOCAL_REPO_PATH "
54- fi
57+ echo " Running git repo update."
58+ log " begin:repo-update"
59+
60+ for repo in " ${REPO_LIST[@]} " ; do
61+ reponame=$( basename " $repo " )
62+ if [ -d " $LOCAL_REPO_PATH /$reponame /.git" ]; then
63+ time retry git -C " $LOCAL_REPO_PATH /$reponame " fetch --prune
64+ else
65+ rm -rf " $LOCAL_REPO_PATH /$reponame .tmp" " $LOCAL_REPO_PATH /$reponame "
66+ time retry git clone " https://github.com/$repo .git" " $LOCAL_REPO_PATH /$reponame .tmp"
67+ mv " $LOCAL_REPO_PATH /$reponame .tmp" " $LOCAL_REPO_PATH /$reponame "
68+ fi
69+ done
70+
71+ log " end:repo-update"
72+ touch " $LAST_UPDATE_FILE "
73+ ) 9> " $UPDATE_LOCK_FILE "
74+
75+ export DWARFS_LOCAL_REPO_PATH=" $LOCAL_REPO_PATH "
5576
5677 if [[ " -$BUILD_TYPE -" == * -debug-* ]] && [[ " -$BUILD_TYPE -" != * -coverage-* ]] &&
5778 [[ " -$BUILD_TYPE -" != * -[at]san-* ]] && [[ " -$BUILD_TYPE -" != * -ubsan-* ]]; then
0 commit comments