The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

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?

Best regards,

Frédéric.

Le 03/02/2016 11:15, Frédéric Blanqui a écrit :
> Hello.
>
> Is there an option for batch compilation to print locations (file, 
> line number) of warnings?
>
> Frédéric.