diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-10 19:23:13 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-10 19:23:13 -0400 |
| commit | 9279ff69732ca873758365518de8105c250ecd23 (patch) | |
| tree | 8b3a8847569c3787e230140ff338929aec1d875b /etc | |
| parent | 21f2c1bafa10e0375acf0cd7b89930e006770c74 (diff) | |
Add etc/ci/smithers.sh for smithers testing
Diffstat (limited to 'etc')
| -rwxr-xr-x | etc/ci/smithers.sh | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/etc/ci/smithers.sh b/etc/ci/smithers.sh new file mode 100755 index 000000000..9109251b2 --- /dev/null +++ b/etc/ci/smithers.sh @@ -0,0 +1,11 @@ +#!/usr/bin/bash + +set -exo pipefail + +cd "$WORKSPACE" +export PATH="/opt/coq-$coq_version/bin${PATH:+:}$PATH" +. /opt/bashrc/bashrc +export TARGETS="coq display bench test" +(/opt/timeout/default-timeout make -j$(nproc) TIMED=1 PROFILE=1 $TARGETS || make STDTIME='/opt/timeout/time-default-timeout-coq -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"' TIMED=1 PROFILE=1 $TARGETS) 2>&1 | tee time-of-build.log +python ./etc/coq-scripts/timing/make-one-time-file.py time-of-build.log time-of-build-pretty.log +cat time-of-build-pretty.log |