Stream: Coq devs & plugin devs

Topic: Debugging CI issue with output redirect


view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Dec 16 2020 at 20:32):

any chance your build uses coqtop?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 20 2020 at 21:27):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 .

view this post on Zulip 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?

view this post on Zulip 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 &>?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 01:47):

oh

view this post on Zulip Jason Gross (Dec 21 2020 at 01:47):

It works fine on 2>&2. It hangs on >/dev/null 2>/dev/null

view this post on Zulip Jason Gross (Dec 21 2020 at 01:48):

Failing build log: https://github.com/mit-plv/fiat/runs/1521926424?check_suite_focus=true
Failing build log (more verbose): https://github.com/mit-plv/fiat/runs/1527508546?check_suite_focus=true
Passing build log (more verbose): https://github.com/mit-plv/fiat/runs/1527645112?check_suite_focus=true
Passing build log (less verbose): https://github.com/mit-plv/fiat/runs/1528132237?check_suite_focus=true

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 02:00):

puzzling indeed. FWIW, you never tried > /dev/null without redirecting stderr?

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 02:00):

checking if TEST_EXISTS_ML_FUNCTION_OUTPUT is used elsewhere...

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 02:01):

seems not, at least according to github's semi-functioning search.

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 02:08):

Okay, no clue, sorry :-|

view this post on Zulip Emilio Jesús Gallego Arias (Dec 21 2020 at 10:38):

Oups, unfortunately I don't have admin here so I cannot move the messages :S

view this post on Zulip Théo Zimmermann (Dec 21 2020 at 18:18):

@Paolo Giarrusso Which Dune thread?

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 18:25):

@Théo Zimmermann https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/Generated.20files.20dependency

view this post on Zulip Notification Bot (Dec 21 2020 at 18:27):

This topic was moved by Théo Zimmermann to #Dune devs & users > Generated files dependency

view this post on Zulip Théo Zimmermann (Dec 21 2020 at 18:28):

Is it good now?

view this post on Zulip Paolo Giarrusso (Dec 21 2020 at 18:29):

looks good, thanks!


Last updated: Jun 04 2023 at 19:30 UTC