aboutsummaryrefslogtreecommitdiff
path: root/etc/ci/smithers.sh
blob: 643a667644d3babe434660cae73454f8a49927ff (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
#!/usr/bin/bash

set -ex

cd "$WORKSPACE"
export PATH="/opt/coq-$coq_version/bin${PATH:+:}$PATH"
. /opt/bashrc/bashrc
coqtop -v
echo | coqtop
export TARGETS="coq display bench test"
export TARGETS="coq non-specific nonautogenerated-specific nonautogenerated-specific-display" #  bench test" # bench and test don't work on smithers
rm -f BUILD.ok
((/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) && touch BUILD.ok) 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
/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
rm BUILD.ok