The Coq mailing list

[Beta Ziliani <beta.ziliani AT gmail.com>]

On Feb 4, 2016 7:11 AM, "Ralf Jung" <post AT ralfj.de> wrote:
>
> Hi,
>
> > I asked this question because this would be very useful to have such an
> > option. If there is currently no way for batch compilation to print
> > warnings, then consider this as a feature request. Such a feature is
> > provided by compilers like gcc, ocamlc, etc. It helps maintaining and
> > improving developments. It is especially useful for big ones. Each new
> > release of Coq comes with new features but also with new warnings and
> > deprecated constructions. Instead of discovering that a development
> > breaks with a new release, printing warnings would enable users to
> > anticipate changes and improve their developments. Currently, in Coq,
> > warnings are discovered in interactive mode only. This makes impossible
> > to locate warnings in big developments spread other many files that are,
> > most of the time, run on batch mode only. So, would it be possible to
> > include such an option in the next 8.5pl1?
>
> I can second this, having warnings when running "make" would be helpful.
> However, there also would have to be some work on which warnings are
> printed. For example, when doing automation involving ssreflect's
> "case", one often gets annoying warnings like "nothing to inject", which
> are very hard to avoid in generic tactics. (Or maybe my ltac-foo is just
> lacking.)
>
> Other compilers typically allow choosing the set of printed warnings
> being configurable via "-Wflag". That would be helpful, and probably
> necessary, when enabling printing of warnings for batch compilation.
>

It's called "sed" :-P

> Kind regards,
> Ralf