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
Also sometimes things are timed so the output gets littered with
Finished transaction in 2.103 secs (1.994u,0.074s) (successful) etc.
I guess I want dune to only print stderr from coq and not stdout
coq_makefile behaves the same, no? But it’s true I don’t know a good fix with dune.
With coq_makefile, I’ve reused code from Iris to support “tests” whose output gets compared with an expected output
There isn't an argument for coqc that mutes stdout is there?
hm, any change to use shell redirection, on coqc or even just on dune?
meanwhile, let me check if
coqc -quiet is what you want?
unclear, but probably not. There are also the
-w options, but I don’t know if they support the knobs you want.
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).
It seems that quite a few people would like a flag like this, the file to tweak is
Where is that file?
Nevermind, I found it in
See also https://github.com/coq/coq/issues/12923
Last updated: Oct 16 2021 at 07:02 UTC