Debugging CI issue with output redirect · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Debugging CI issue with output redirect

Jason Gross (Dec 16 2020 at 16:09):

But there's another fiat-parsers problem I'm hitting which is that some of the build fails on master on CI iff I redirect output to /dev/null (and succeeds locally on master and on CI on all other versions of Coq regardless of redirection)

Paolo Giarrusso (Dec 16 2020 at 20:32):

any chance your build uses coqtop?

Paolo Giarrusso (Dec 16 2020 at 20:33):

breaking with > /dev/null is more plausible with interactive programs that use TTY APIs (without checking isatty(3) first)

Jason Gross (Dec 20 2020 at 16:19):

Paolo Giarrusso said:

any chance your build uses coqtop?

The script is just

#!/bin/bash

set -x

FILE="conftest.ml"
MAKEFILE=""

function cleanup () {
    PREFILE="${FILE%.ml}"
    rm -f "$PREFILE.cmi" "$PREFILE.cmo" "$PREFILE.cmx" "$PREFILE.cmxs" "$PREFILE.ml.d" "$PREFILE.o" "$FILE" "$MAKEFILE" "$MAKEFILE.conf"
}

trap cleanup EXIT

cat > "$FILE" <<EOF
let test = $FUNCTION
EOF

cat "$FILE"

MAKEFILE="$(mktemp)"
(("${COQBIN}coq_makefile" "$FILE" -R . Top -o "$MAKEFILE" || "${COQBIN}coq_makefile" "$FILE" -R . Top > "$MAKEFILE")
     && make -f "$MAKEFILE" || exit 1)
exit 0

with some externally-set value of $FUNCTION. And note that it only hangs on redirect to /dev/null on the CI (both Travis and GitHub Actions, every single time, but only on Coq master), but not on either of the two local machines I tested, nor even on a VMWare Ubuntu VM that I tried out running the same Ubuntu version and same apt-get install'd Coq packages as the CI run used. I'm very puzzled.

Paolo Giarrusso (Dec 20 2020 at 21:26):

what about stdin / stderr? they’re likely bound to a terminal locally, but to a pipe or a file on Travis.

Paolo Giarrusso (Dec 20 2020 at 21:27):

That _shouldn’t_ make a difference, but it _could_.

Paolo Giarrusso (Dec 20 2020 at 21:34):

enough other differences are possible (in ulimit or surrounding code) that this might be worth a separate thread with links to the logs.

Paolo Giarrusso (Dec 20 2020 at 21:35):

and I’d hope neither coq_makefile nor mktemp break here, and that _other_ code behaves differently somehow.

Jason Gross (Dec 20 2020 at 23:25):

The commit that made things go from non-working to working was: https://github.com/JasonGross/coq-scripts/commit/dcc87199ca6fd0b87b76e3c28c849cfe96590e90 .

Paolo Giarrusso (Dec 21 2020 at 01:29):

~~Whoops, seems @Emilio Jesús Gallego Arias's message and my last one belong in the dune thread?~~

Paolo Giarrusso (Dec 21 2020 at 01:43):

@Jason Gross where's the callsite to test_exists_ml_function? and how do you redirect to devnull, > or &>?

Jason Gross (Dec 21 2020 at 01:46):

@Paolo Giarrusso The redirect is at the end of the test_exists_ml_function line, >$(TEST_EXISTS_ML_FUNCTION_OUTPUT) 2>$(TEST_EXISTS_ML_FUNCTION_OUTPUT) The call site is https://github.com/mit-plv/fiat/blob/18674cf854fc0bafb22c1b1a90f4ac99037f5a49/Makefile#L113

Paolo Giarrusso (Dec 21 2020 at 01:46):

the bug isn't obvious, and the produced 2>&2 might trigger dup2(2, 2) syscall — that's supposed to be a no-op — but at least this is more plausibly faulty