1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
#!/usr/bin/bash
# Use this script to preserve the exit code of $CI_SCRIPT when piping
# it to `tee time-of-build.log`. We have a separate script, because
# this only works in bash, which we don't require project-wide.
set -o pipefail
set -x
CI_NAME="$1"
CI_SCRIPT="scripts/ci-${CI_NAME}.sh"
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
# assume this script is in dev/ci/, cd to the root Rocq directory
cd "${DIR}/../.." || exit 1
export TIMED=1
# if COQ_CI_COLOR is set (from the environment) keep it intact (even when it's the empty string)'
if ! [ "${COQ_CI_COLOR+1}" ]; then
# NB: in CI TERM is unset in the environment
# when TERM is unset, bash sets it to "dumb" as a bash variable (not exported?)
if { [ -t 1 ] && ! [ "$TERM" = dumb ]; } || [ "$CI" ]
then COQ_CI_COLOR=1
else COQ_CI_COLOR=
fi
fi
# we don't want to block commands on user interaction
export GIT_PAGER=
if [ "$COQ_CI_COLOR" = 1 ] && command -v script > /dev/null; then
# prevent piping from disabling auto colors / enable auto colors in CI
if [ "$CI" ]; then
export TERM=xterm-color
fi
# on some macos systems OSTYPE is just "darwin", on others it's followed by version info
if [[ "$OSTYPE" =~ ^darwin ]]; then
script -q /dev/null bash "${DIR}/${CI_SCRIPT}" 2>&1 | tee "$CI_NAME.log"
else
script --quiet --flush --return -c "bash '${DIR}/${CI_SCRIPT}'" /dev/null 2>&1 | tee "$CI_NAME.log"
fi
else
if [ "$COQ_CI_COLOR" = 1 ]; then
>&2 echo 'script command not available, colors will be hidden'
fi
bash "${DIR}/${CI_SCRIPT}" 2>&1 | tee "$CI_NAME.log"
fi
code=$?
printf "\n%s exit code: %s\n" "$CI_NAME" "$code" >> "$CI_NAME.log"
# the test suite already prints a timing table
if [ "$CI_NAME" != stdlib_test ]; then
echo 'Aggregating timing log...'
echo
tools/make-one-time-file.py --real "$CI_NAME.log"
fi
if [ "$CI" ] && ! [ $code = 0 ]; then
set +x
escape_re=$(printf '\033%s' '\[[0-9;]+m')
# File ".*
file_re="($escape_re)?"'File ".*\n'
# OCaml: error message may contain some code extracts starting with the line number,
# followed by a line containing "^^^" to point at the columns (possibly colored)
codeline_re='([0-9].*\n)*'
carets_re="((($escape_re)|[ ^])*\n)?"
# Error messages may be multiline, but it's hard to find the end
# heuristic: if the line ends with ":" or ",", also print the next
# (typically if the start of the message got moved to the next line,
# the first line is just "Error:",
# also note that OCaml colors just "Error" but Rocq colors the whole "Error:")
error_re="($escape_re)?Error(.*[:,]($escape_re)?\n)*.*\n"
# for some reason when testing with colors on
# I also got carriage returns in my output which confused grep, so remove them
# -P: perl-like
# -z: multiline using \0 chars (which is why we have to tr to cleanup the output)
# -o: print only matched (otherwise it prints the whole file due to -z)
# || true: if no error is matched by this pattern, we still want to use the error code from the build
< "$CI_NAME.log" tr -d "$(printf '\r')" \
| grep -Pzo "$file_re$codeline_re$carets_re$error_re" \
| tr -d '\0' > errors \
|| true
if [ -s errors ]; then {
echo
echo "Error list (may be incomplete):"
echo
cat errors
} >&2
fi
rm errors
fi
exit $code
|
