Compile Coq will all warnings as errors.

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4671
From: @ejgallego
Reported version: trunk
CC: coq-bugs-redist@lists.gforge.inria.fr

[coqbot]

Comment author: @ejgallego

This is a tracker bug for the goal of compiling a warning-free Coq.

OCAML default set of warnings is.

-w +a-4-6-7-9-27-29-32..39-41-42-44-45-48-50

The easy way to enable all warnings is:

make CAMLFLAGS="-rectypes -w @ 1..49"

Enabling all of them is not realistic now, but we can start looking into the many warnings generated.

[coqbot]

Comment author: @ejgallego

Created attachment 698
Full warning log for trunk.

Attached file: coq-warn.log.bz2 (application/x-bzip, 116747 bytes)
Description: Full warning log for trunk.

[coqbot]

Comment author: @ejgallego

Adding this snippet to the .merlin file is of great help with cleaning up some of these warnings:

FLG -rectypes -w +1..49

[coqbot]

Comment author: @ejgallego

Implemented by Gaetan Gilbert in d8d56df