Commits (4)
......@@ -26,17 +26,16 @@ set -o pipefail
. ci/prepare-opam.sh $OPAM_PINS # deliberately not quoted
env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
# maybe set some coq flags
if [[ -n "$MANGLE_NAMES" ]]; then
export COQEXTRAFLAGS="$COQEXTRAFLAGS -mangle-names mangled_"
fi
if [[ -n "$TIMING_PROJECT" ]]; then
export TIMECMD=ci/perf
fi
# Build
BUILD_TARGET=${BUILD_TARGET:-all}
echo_color "$BOLDGREEN" "[buildjob] Perfoming build (target: $BUILD_TARGET)"
time make $BUILD_TARGET --output-sync --no-print-directory -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt
echo_color "$BOLDGREEN" "[buildjob] Build time summary"
cat build-log.txt | egrep "(real|user): [0-9]" | tee build-time.txt
echo_color "$BOLDGREEN" "[buildjob] Perfoming build"
time make --output-sync --no-print-directory -k -j$CPU_CORES 2>&1
# maybe check for axioms
if [[ -z "$AXIOMS_IGNORE" ]]; then
......@@ -48,8 +47,12 @@ fi
# maybe submit timing information
if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then
echo_color "$BOLDGREEN" "[buildjob] Submitting timing information to coq-speed"
# collect all information into one file
echo_color "$BOLDGREEN" "[buildjob] Build performance information"
find -name "*.v.perf" -print0 | xargs -0 cat > build-times.txt
cat build-times.txt
# check if we have the secret
echo_color "$BOLDGREEN" "[buildjob] Submitting timing information to coq-speed"
if [[ -z "$TIMING_SECRET" ]]; then
echo_color "$BOLDRED" "[buildjob] TIMING_SECRET variable is missing"
exit 1
......@@ -62,7 +65,7 @@ if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then
-H "X-Branch: $CI_COMMIT_REF_NAME" \
-H "X-Config: $TIMING_CONF" \
-H "X-Date: $(git show $CI_COMMIT_SHA -s --pretty=%cI)" \
--data-binary @- < build-time.txt
--data-binary @- < build-times.txt
fi
# maybe create opam package
......
#!/bin/bash
set -e
# Wrapper script to use perf as TIMECMD for the build.
VFILE="${!#}"
LC_ALL=C /usr/bin/time -o "$VFILE.time" -f "real: %e, user: %U, sys: %S, mem: %M kB" -- perf stat -o "$VFILE.counters" -x ';' -e instructions,cycles -- "$@"
(echo "## $VFILE" && (cat "$VFILE.counters" | egrep -v '^(# .*)?$') && cat "$VFILE.time" && echo) > "$VFILE.perf"
rm "$VFILE.counters" "$VFILE.time"