Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
ci
Commits
8d9e688c
Commit
8d9e688c
authored
Jun 05, 2021
by
Ralf Jung
Browse files
add support for ad-hoc timing
parent
c3489f09
Changes
1
Hide whitespace changes
Inline
Side-by-side
buildjob
View file @
8d9e688c
...
...
@@ -19,11 +19,13 @@ 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_CONF, $TIMING_SECRET: When running on the
## `coop-timing` runner, submit timing information to coq-speed with the given
## project name and configuration string. $TIMING_PROJECT defaults to the
## repository name. $TIMING_CONF defaults to the job name. Reqires the
## $TIMING_SECRET variable to be set.
## - $TIMING_PROJECT, $TIMING_SECRET: When running on the `coop-timing` runner,
## 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
## $TIMING_AD_HOC_ID. In that case the branch will be set to `@hoc` and the
## configuration will be set to the $TIMING_AD_HOC_ID.
## - $DOC_DIR, $DOC_KEY, $DOC_OPTS: If $DOC_DIR is non-empty, run coqdoc and
## upload the results to the given directory. This only happens if the
## current branch is `master`. Requires the $DOC_KEY variable to be set to
...
...
@@ -36,7 +38,6 @@ status "[buildjob] Pipeline source: $CI_PIPELINE_SOURCE; commit branch (empty fo
OCAML
=
${
OCAML
:-
ocaml
-base-compiler.4.08.1
}
MAKE_TARGET
=
${
MAKE_TARGET
:-
all
}
TIMING_PROJECT
=
${
TIMING_PROJECT
:-
$CI_PROJECT_NAME
}
TIMING_CONF
=
${
TIMING_CONF
:-
$CI_JOB_NAME
}
# Environment sanity checks
if
[[
-n
"
$VALIDATE
"
]]
;
then
...
...
@@ -89,14 +90,21 @@ if [[ "$CI_RUNNER_DESCRIPTION" == "coop-timing" && -n "$CI_COMMIT_BRANCH" ]]; th
if
[[
-z
"
$TIMING_SECRET
"
]]
;
then
panic
"[buildjob] TIMING_SECRET variable is missing"
fi
# determine branch and config
TIMING_BRANCH
=
$CI_COMMIT_BRANCH
TIMING_CONFIG
=
$CI_JOB_NAME
if
[[
-n
"
$TIMING_AD_HOC_ID
"
]]
;
then
TIMING_BRANCH
=
"@hoc"
TIMING_CONFIG
=
$TIMING_AD_HOC_ID
fi
# Submit to webhook endpoint
status
"[buildjob] Submitting timing information to coq-speed (Project:
$TIMING_PROJECT
, Branch:
$CI_COMMIT_BRANCH
, Config:
$TIMING_CONF
)"
curl
--fail
-sS
-X
POST https://coq-speed.mpi-sws.org/webhook/build_times
\
--user
"
$TIMING_SECRET
"
\
-H
"X-Commit:
$CI_COMMIT_SHA
"
\
-H
"X-Project:
$TIMING_PROJECT
"
\
-H
"X-Branch:
$CI_COMMIT_BRANCH
"
\
-H
"X-Config:
$TIMING_CONF
"
\
-H
"X-Branch:
$TIMING_BRANCH
"
\
-H
"X-Config:
$TIMING_CONFIG
"
\
-H
"X-Commit:
$CI_COMMIT_SHA
"
\
-H
"X-Date:
$(
git show
$CI_COMMIT_SHA
-s
--pretty
=
%cI
)
"
\
--data-binary
@- < build-times.txt
fi
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment