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
.
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 -set
and -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 mltop.ml
Where is that file?
Nevermind, I found it in vernac
.
See also https://github.com/coq/coq/issues/12923
Last updated: Oct 13 2024 at 01:02 UTC