Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108#!/usr/bin/env bash
# Use this script to preserve the exit code of $CI_SCRIPT when piping# it to `tee $log_file`. We have a separate script, because# this only works in bash, which we don't require project-wide.
set -o pipefailset -x
CI_NAME="$1"CI_SCRIPT="scripts/ci-${CI_NAME}.sh"log_file="_build_ci/${CI_NAME}.log"
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"# assume this script is in dev/ci/, cd to the root Rocq directorycd "${DIR}/../.." || exit 1
mkdir -p _build_ci # needs to exist so we can write the log_file
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= fifi
# we don't want to block commands on user interactionexport 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 "$log_file" else script --quiet --flush --return -c "bash '${DIR}/${CI_SCRIPT}'" /dev/null 2>&1 | tee "$log_file" fielse if [ "$COQ_CI_COLOR" = 1 ]; then >&2 echo 'script command not available, colors will be hidden' fi bash "${DIR}/${CI_SCRIPT}" 2>&1 | tee "$log_file"ficode=$?
printf "\n%s exit code: %s\n" "$CI_NAME" "$code" >> "$log_file"
# the test suite already prints a timing tableif [ "$CI_NAME" != stdlib_test ]; then echo 'Aggregating timing log...' echo tools/make-one-time-file.py --real "$log_file"fi
# don't print error summary for coq_tools as it gets spammy, and hides jason_msg# see eg https://gitlab.inria.fr/coq/coq/-/jobs/6292796if [ "$CI" ] && ! [ $code = 0 ] && [ "$CI_NAME" != coq_tools ]; 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 < "$log_file" 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
fiexit $code