Stream: Dune devs & users

Topic: Muting output of coq during dune build


view this post on Zulip Ali Caglayan (Aug 14 2020 at 17:00):

Hi, does anybody know how to mute the output of coq during dune build? Specifically, if I built a file which has a Print statement in it, dune prints it. This can be annoying especially if the vernacular that is printing is really just checking something with Check.

view this post on Zulip Ali Caglayan (Aug 14 2020 at 17:01):

Also sometimes things are timed so the output gets littered with Finished transaction in 2.103 secs (1.994u,0.074s) (successful) etc.

view this post on Zulip Ali Caglayan (Aug 14 2020 at 17:02):

I guess I want dune to only print stderr from coq and not stdout

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 17:05):

coq_makefile behaves the same, no? But it’s true I don’t know a good fix with dune.

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 17:05):

With coq_makefile, I’ve reused code from Iris to support “tests” whose output gets compared with an expected output

view this post on Zulip Ali Caglayan (Aug 14 2020 at 19:30):

There isn't an argument for coqc that mutes stdout is there?

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 19:46):

hm, any change to use shell redirection, on coqc or even just on dune?

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 19:46):

meanwhile, let me check if coqc -quiet is what you want?

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 19:50):

unclear, but probably not. There are also the -set and -w options, but I don’t know if they support the knobs you want.

view this post on Zulip Paolo Giarrusso (Aug 14 2020 at 19:51):

but it’d make sense if dune kept stdout and stderr from underlying tools separate — and then dune build > /dev/null might do something (dunno how to only redirect stdout of subcommands).

view this post on Zulip Emilio Jesús Gallego Arias (Aug 27 2020 at 15:19):

It seems that quite a few people would like a flag like this, the file to tweak is mltop.ml

view this post on Zulip Ali Caglayan (Aug 27 2020 at 15:22):

Where is that file?

view this post on Zulip Ali Caglayan (Aug 27 2020 at 15:25):

Nevermind, I found it in vernac.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 27 2020 at 15:34):

See also https://github.com/coq/coq/issues/12923


Last updated: Mar 29 2024 at 08:39 UTC