Skip to content
Snippets Groups Projects
Commit 8693ed7d authored by Ralf Jung's avatar Ralf Jung
Browse files

collect timing information using perf

parent 8ec855ae
No related branches found
No related tags found
No related merge requests found
...@@ -26,16 +26,16 @@ set -o pipefail ...@@ -26,16 +26,16 @@ set -o pipefail
. ci/prepare-opam.sh $OPAM_PINS # deliberately not quoted . ci/prepare-opam.sh $OPAM_PINS # deliberately not quoted
env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
# maybe set some coq flags
if [[ -n "$MANGLE_NAMES" ]]; then if [[ -n "$MANGLE_NAMES" ]]; then
export COQEXTRAFLAGS="$COQEXTRAFLAGS -mangle-names mangled_" export COQEXTRAFLAGS="$COQEXTRAFLAGS -mangle-names mangled_"
fi fi
if [[ -n "$TIMING_PROJECT" ]]; then
export TIMECMD=ci/perf
fi
# Build # Build
echo_color "$BOLDGREEN" "[buildjob] Perfoming build" echo_color "$BOLDGREEN" "[buildjob] Perfoming build"
time make --output-sync --no-print-directory -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt time make --output-sync --no-print-directory -k -j$CPU_CORES 2>&1
echo_color "$BOLDGREEN" "[buildjob] Build time summary"
cat build-log.txt | egrep "(real|user): [0-9]" | tee build-time.txt
# maybe check for axioms # maybe check for axioms
if [[ -z "$AXIOMS_IGNORE" ]]; then if [[ -z "$AXIOMS_IGNORE" ]]; then
...@@ -53,6 +53,9 @@ if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then ...@@ -53,6 +53,9 @@ if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then
echo_color "$BOLDRED" "[buildjob] TIMING_SECRET variable is missing" echo_color "$BOLDRED" "[buildjob] TIMING_SECRET variable is missing"
exit 1 exit 1
fi fi
# collect all information into one file
find -name "*.v.perf" -print0 | xargs -0 cat > build-times.txt
cat build-times.txt
# Submit to webhook endpoint # Submit to webhook endpoint
curl --fail -sS -X POST https://coq-speed.mpi-sws.org/webhook/build_times \ curl --fail -sS -X POST https://coq-speed.mpi-sws.org/webhook/build_times \
--user "$TIMING_SECRET" \ --user "$TIMING_SECRET" \
...@@ -61,7 +64,7 @@ if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then ...@@ -61,7 +64,7 @@ if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then
-H "X-Branch: $CI_COMMIT_REF_NAME" \ -H "X-Branch: $CI_COMMIT_REF_NAME" \
-H "X-Config: $TIMING_CONF" \ -H "X-Config: $TIMING_CONF" \
-H "X-Date: $(git show $CI_COMMIT_SHA -s --pretty=%cI)" \ -H "X-Date: $(git show $CI_COMMIT_SHA -s --pretty=%cI)" \
--data-binary @- < build-time.txt --data-binary @- < build-times.txt
fi fi
# maybe create opam package # maybe create opam package
......
perf 0 → 100755
#!/bin/bash
set -e
# Wrapper script to use perf as TIMECMD for the build.
VFILE="${!#}"
perf stat -o "$VFILE.perf.tmp" -x ';' -e instructions,cycles -- "$@"
(echo "## $VFILE" && (cat "$VFILE.perf.tmp" | egrep -v '^(# .*)?$') && echo) > "$VFILE.perf"
rm "$VFILE.perf.tmp"
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment