Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Command line flags for warnings

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Command line flags for warnings


Chronological Thread 
  • 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 ;-)

And also feel free to open new issues for each warning that comes without a name and a category (because it predates the warning system and has not been adapted to it), like Erkki did for "Query commands should not be inserted into scripts.". These are bugs that we might want to solve.

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
>




Archive powered by MHonArc 2.6.18.

Top of Page