The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

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.

Kind regards,
Ralf