Stream: Coq users

Topic: What does the `Silent` coq flag do?


view this post on Zulip Ali Caglayan (Aug 09 2020 at 20:53):

There is a coq flag called Silent. But I can't seem to work out what it does. I have a .v file that prints something but setting Silent doesn't seem to change anything with coqc

view this post on Zulip Ali Caglayan (Aug 09 2020 at 20:56):

For example:

$ echo "Require Import Basics. Set Silent. Print Eq." > test.v
$ coqc test.v
Inductive comparison : Set :=
    Eq : comparison | Lt : comparison | Gt : comparison

What exactly was it supposed to do?

view this post on Zulip Théo Zimmermann (Aug 11 2020 at 15:16):

This line of code shows that -batch implies -quiet so there are good chances that this flag has no effect when used with coqc and is only useful to avoid printing goals when using coqtop.

view this post on Zulip Ali Caglayan (Aug 11 2020 at 18:21):

Thanks!


Last updated: Feb 09 2023 at 00:03 UTC