Stream: Coq devs & plugin devs

Topic: output-sync


view this post on Zulip Gaëtan Gilbert (Mar 07 2021 at 08:59):

Is output-sync in CI worth it? It's super spammy with "entering/leaving directory" messages for some reason.

view this post on Zulip Janno (Mar 07 2021 at 10:11):

I think one can avoid that with -s

view this post on Zulip Gaëtan Gilbert (Mar 07 2021 at 10:13):

I don't want -s though

view this post on Zulip Janno (Mar 07 2021 at 10:15):

Ah, I never bothered to see what other (useful) output it removes.

view this post on Zulip Janno (Mar 07 2021 at 10:16):

Does --no-print-directory help?

view this post on Zulip Gaëtan Gilbert (Mar 07 2021 at 10:18):

I want it to print directory, it helps emacs jump to error locations, but output-sync messes with it somehow

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2021 at 16:38):

Indeed for me output of CI is just unreadable, I'm a big fan of fully silent builds.

view this post on Zulip Michael Soegtrop (Mar 08 2021 at 09:53):

Silent build output is easier to read but it is less likely that you will find relevant information in it. I prefer to search a bit in a log over having to rerun CI with manipulated options. So I am a fan of verbose builds.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2021 at 13:05):

What is relevant information? I am interested only in warnings and errors, the rest I don't think it is relevant, and can be saved to _build/log as we do in the silent builds for further debugging if needed.

view this post on Zulip Gaëtan Gilbert (Mar 08 2021 at 13:17):

if something hangs we don't get _build/log

view this post on Zulip Michael Soegtrop (Mar 08 2021 at 14:33):

I have seen logs where I did see error messages, but it was quite hard to tell where they came from.

I don't say that one shouldn't try to organize logs in a reasonable way. My requirement for such an organized log would be that the relative frequency for having to restart CI cause of insufficient logs should be less than 1/100, better less than 1/1000. The shortest log which meets this requirement is what I really want. I guess we agree on this, we are just approaching this goal from different ends.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2021 at 16:21):

if something hangs we don't get _build/log

that's a bug on our CI as it should upload the _build/log in case of timeout; in any case running a build with --display=verbose is very easy if needed, but still the silent default is much much better, and in fact we already have filters to eliminate all the noise the CI does.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 08 2021 at 16:21):

I have seen many times people spending minutes to locate an error in a make -j 8 regular Coq build

view this post on Zulip Jason Gross (Mar 09 2021 at 13:48):

I think I added --output-sync because otherwise we occasionally get garbled lines and the pretty-timing table gets confused. (I can't recall whether the python script ever errors on garbled logs, it's possible that it does and should be made robust to such garbling)


Last updated: Oct 16 2021 at 01:03 UTC