coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo.zimmi AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Command line flags for warnings
- Date: Thu, 9 Nov 2017 11:08:31 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f180.google.com
- Ironport-phdr: 9a23:q9ocbheSVHYfsbZV2j6IgEDZlGMj4u6mDksu8pMizoh2WeGdxc2zZh7h7PlgxGXEQZ/co6odzbGJ4+a9ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpRZbIBj0NBJ0K+LpAcaSyp3vj6Hhs6HUNi5PnXKWZa54ZEG9qhyUvc0Li6NjLLwww13HuC0bVf5RwDZUJdOUqCT948K95ptq9SIY7+4h+skGQ6T/eqUQQrlRDTBgOGcwsp64/SLfRBeCsyNPGl4dlQBFVk2ctEn3
Hi Christian,
Feel free to submit a pull request improving the way the manual explains this ;-)Best,
Théo
2017-11-08 11:31 GMT+01:00 Christian Doczkal <christian.doczkal AT ens-lyon.fr>:
Hello,
That was indeed very helpful. Maybe the manual could be improved to more
clearly state the connection between the printed messages and the
command-line switches.
Somewhat related, there are other warnings (e.g., "Warning: Noting to
inject.") that predate the current warning system and seem to be
unaffected by any warning switches. Is there a way to turn the
aforementioned waring off or into an error?
Best,
Christian
Is there also a way for turning "Warning: Nothing to Inject" into a
On 11/05/2017 12:16 PM, Théo Zimmermann wrote:
> Hi,
>
> Section 6.9.3 (https://coq.inria.fr/distrib/current/refman/vernacular.html#SetWarnings) also says "Adding - in front of a warning or category disables it, adding + makes it an error. It is possible to use the special categories all and default, the latter containing the warnings enabled by default."
>
> The warnings names and categories are displayed whenever you see such a warning (I ignore if there is a command to display all warning names or categories).
> E.g. if you type "Variable A : Prop." in an empty buffer, you will see:
> "A is declared as a local axiom [local-declaration,scope]"
> The warning name is local-declaration and the category is scope.
>
> Thus if you relaunch CoqIDE (or coqtop through Proof-General) with option -w "-local-declaration", you won't see any warning for the same buffer.
> And if you use option -w "+local-declaration", you will see an error instead.
>
> Théo
>
> Le sam. 4 nov. 2017 à 23:27, Erkki Luuk <erkkil AT gmail.com <mailto:erkkil AT gmail.com>> a écrit :
>
> Hi
>
> Where do I find the command line flags for warning names and categories? The manual just says:
>
> -w (all|none|w1,…,wn)
>
> Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section 6.9.3).
>
> https://coq.inria.fr/distrib/current/refman/commands.html#hevea_default978
>
> Erkki
>
- [Coq-Club] Command line flags for warnings, Erkki Luuk, 11/04/2017
- Re: [Coq-Club] Command line flags for warnings, Théo Zimmermann, 11/05/2017
- Re: [Coq-Club] Command line flags for warnings, Erkki Luuk, 11/07/2017
- Re: [Coq-Club] Command line flags for warnings, Christian Doczkal, 11/08/2017
- Re: [Coq-Club] Command line flags for warnings, Théo Zimmermann, 11/09/2017
- Re: [Coq-Club] Command line flags for warnings, Théo Zimmermann, 11/05/2017
Archive powered by MHonArc 2.6.18.