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
1c2ae888
Commit
1c2ae888
authored
Feb 11, 2020
by
Ralf Jung
Browse files
auto-detect timing job name
parent
f8393bfa
Changes
1
Hide whitespace changes
Inline
Side-by-side
buildjob
View file @
1c2ae888
...
...
@@ -16,10 +16,11 @@ set -eo pipefail
## Requires the $OPAM_UPDATE_SECRET variable to be set. This only happens if
## the current branch is $OPAM_PKG_BRANCH, or master if that variable is
## empty.
## - $TIMING_PROJECT, $TIMING_CONF, $TIMING_SECRET: If $TIMING_CONF is
## non-empty, submit timing information to coq-speed with the given project
## name and configuration string. The project names defaults to the
## repository name. Reqires the $TIMING_SECRET variable to be set.
## - $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.
## - $DOC_DIR, $DOC_BRANCH, $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 $DOC_BRANCH (defaults to master). Requires the
...
...
@@ -33,6 +34,7 @@ OCAML=${OCAML:-ocaml-base-compiler.4.07.1}
OPAM_PKG_BRANCH
=
${
OPAM_PKG_BRANCH
:-
master
}
DOC_BRANCH
=
${
DOC_BRANCH
:-
master
}
TIMING_PROJECT
=
${
TIMING_PROJECT
:-
$CI_PROJECT_NAME
}
TIMING_CONF
=
${
TIMING_CONF
:-
$CI_JOB_NAME
}
# Environment sanity checks
if
[[
-n
"
$VALIDATE
"
]]
;
then
...
...
@@ -55,7 +57,7 @@ status "[buildjob] Perfoming build"
time
make
--output-sync
--no-print-directory
-k
-j
$CPU_CORES
2>&1
# maybe submit timing information
if
[[
-n
"
$TIMING_CONF
"
]]
;
then
if
[[
"
$CI_RUNNER_DESCRIPTION
"
==
"coop-timing
"
]]
;
then
# collect all information into one file
status
"[buildjob] Build performance information"
find
-name
"*.v.perf"
-print0
| xargs
-0
cat
>
build-times.txt
...
...
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