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)
any chance your build uses coqtop
?
breaking with > /dev/null
is more plausible with interactive programs that use TTY APIs (without checking isatty(3)
first)
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.
what about stdin / stderr? they’re likely bound to a terminal locally, but to a pipe or a file on Travis.
That _shouldn’t_ make a difference, but it _could_.
enough other differences are possible (in ulimit or surrounding code) that this might be worth a separate thread with links to the logs.
and I’d hope neither coq_makefile nor mktemp break here, and that _other_ code behaves differently somehow.
The commit that made things go from non-working to working was: https://github.com/JasonGross/coq-scripts/commit/dcc87199ca6fd0b87b76e3c28c849cfe96590e90 .
Whoops, seems @Emilio Jesús Gallego Arias's message and my last one belong in the dune thread?
@Jason Gross where's the callsite to test_exists_ml_function
? and how do you redirect to devnull, >
or &>
?
@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
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
oh
It works fine on 2>&2
. It hangs on >/dev/null 2>/dev/null
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
puzzling indeed. FWIW, you never tried > /dev/null
without redirecting stderr?
checking if TEST_EXISTS_ML_FUNCTION_OUTPUT is used elsewhere...
seems not, at least according to github's semi-functioning search.
Okay, no clue, sorry :-|
Oups, unfortunately I don't have admin here so I cannot move the messages :S
@Paolo Giarrusso Which Dune thread?
@Théo Zimmermann https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/Generated.20files.20dependency
This topic was moved by Théo Zimmermann to #Dune devs & users > Generated files dependency
Is it good now?
looks good, thanks!
Last updated: Jun 04 2023 at 19:30 UTC