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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
#!/usr/bin/bash
# TODO:
#
# - Check if the branch already exists in the remote => checkout
# - Better error handling
# - Just checkout, don't build
# - Rebase functionality
#
set -x
set -e
set -o pipefail
# setup_contrib_git("_build_ci/fiat", "https://github.com/ejgallego/fiat-core.git")
setup_contrib_git() {
local _DIR=$1
local _GITURL=$2
( cd $_DIR
git checkout -b $OVERLAY_BRANCH || true # allow the branch to exist already
git remote add $DEVELOPER_NAME $_GITURL || true # allow the remote to exist already
if [ -d .git ]; then # TODO handle submodules
template_file=.git/OVERLAY_COMMIT_TEMPLATE
printf 'Adapt to rocq-prover/rocq#%s (short decription here)\n' "$PR_NUMBER" > "$template_file"
# don't override config if already set, maybe the user prefers something else
if ! git config get --local commit.template; then
git config set --local commit.template "$template_file"
fi
fi
)
}
if [ $# -lt 3 ]; then
echo "usage: $0 github_username pr_number contrib1 ... contribN"
exit 1
fi
set +x
. dev/ci/ci-basic-overlay.sh
set -x
DEVELOPER_NAME=$1
shift
PR_NUMBER=$1
shift
OVERLAY_BRANCH=$(git rev-parse --abbrev-ref HEAD)
OVERLAY_FILE=$(mktemp overlay-XXXX)
# Create the overlay file
> "$OVERLAY_FILE"
skipped_repos=
# We first try to build the contribs
while test $# -gt 0
do
_CONTRIB_NAME=$1
_CONTRIB_GITURL=${_CONTRIB_NAME}_CI_GITURL
_CONTRIB_GITURL=${!_CONTRIB_GITURL}
_CONTRIB_SUBMODULE_GITURL=${_CONTRIB_NAME}_CI_SUBMODULE_GITURL
_CONTRIB_SUBMODULE_GITURL=${!_CONTRIB_SUBMODULE_GITURL}
_CONTRIB_SUBMODULE_BRANCH=${_CONTRIB_NAME}_CI_SUBMODULE_BRANCH
_CONTRIB_SUBMODULE_BRANCH=${!_CONTRIB_SUBMODULE_BRANCH}
if [[ -n "${_CONTRIB_SUBMODULE_GITURL}" ]]; then
_CONTRIB_GITURL="${_CONTRIB_SUBMODULE_GITURL}"
fi
echo "Processing Contrib $_CONTRIB_NAME"
shift
# check _CONTRIB_GIT exists and it is of the from github...
_CONTRIB_DIR=_build_ci/$_CONTRIB_NAME
# extract the relevant part of the repository
if [[ $_CONTRIB_GITURL == https://github.com/*/* ]]; then
_CONTRIB_GITSUFFIX=${_CONTRIB_GITURL#https://github.com/*/}
_CONTRIB_GITURL="https://github.com/$DEVELOPER_NAME/$_CONTRIB_GITSUFFIX"
_CONTRIB_GITPUSHURL="git@github.com:$DEVELOPER_NAME/${_CONTRIB_GITSUFFIX}.git"
else
skipped_repos="$skipped_repos $_CONTRIB_NAME"
continue
fi
DOWNLOAD_ONLY=1 make ci-$_CONTRIB_NAME || true
setup_contrib_git $_CONTRIB_DIR $_CONTRIB_GITPUSHURL
echo "overlay ${_CONTRIB_NAME} $_CONTRIB_GITURL $OVERLAY_BRANCH $PR_NUMBER" >> $OVERLAY_FILE
if [ -n "${_CONTRIB_SUBMODULE_BRANCH}${_CONTRIB_SUBMODULE_GITURL}" ]; then
echo "# Make PRs against ${_CONTRIB_SUBMODULE_GITURL} base branch ${_CONTRIB_SUBMODULE_BRANCH}" >> $OVERLAY_FILE
fi
if [ $# -gt 0 ]; then echo "" >> $OVERLAY_FILE; fi
done
# Copy to overlays folder.
PR_NUMBER=$(printf '%05d' "$PR_NUMBER")
mv $OVERLAY_FILE dev/ci/user-overlays/$PR_NUMBER-$DEVELOPER_NAME-${OVERLAY_BRANCH///}.sh
if [ -n "$skipped_repos" ]; then
>&2 echo "Skipped non-github repos: $skipped_repos"
exit 1
fi
|
