[coq_makefile] Enforce warn_error for plugins.

The amount of dangerous warnings in plugins is out of hand, including
some very serious ones.

As Coq developers are maintaining plugins these days it makes sense to
require the contributions to follow the same coding discipline as in
the main tree, thus we require the set of warnings fatal warnings to
be the same in Coq and in plugins.

We don't mark deprecation as fatal as to allow time for migration.

Fixes #6974

9 files changed, 40 insertions, 5 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3c427793e2..b074427892 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -662,5 +662,5 @@ plugin:plugin-tutorial:
 plugin:ci-quickchick:
   extends: .ci-template-flambda
 
-plugin:ci-relation-algebra:
+plugin:ci-relation_algebra:
   extends: .ci-template
diff --git a/Makefile.ci b/Makefile.ci
index 000725b6b1..a244c17ef3 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -38,7 +38,7 @@ CI_TARGETS= \
     ci-mtac2 \
     ci-paramcoq \
     ci-quickchick \
-    ci-relation-algebra \
+    ci-relation_algebra \
     ci-sf \
     ci-simple-io \
     ci-stdlib2 \
diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md
index 01769aeddb..06b617d4c1 100644
--- a/dev/ci/README-users.md
+++ b/dev/ci/README-users.md
@@ -45,6 +45,26 @@ using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is
 to give merge permissions to someone from the Coq team as to help with
 these kind of merges.
 
+### OCaml and plugin-specific considerations
+
+Developments that link against Coq's OCaml API [most of them are known
+as "plugins"] do have some special requirements:
+
+- Coq's OCaml API is not stable. We hope to improve this in the future
+  but as of today you should expect to have to merge a fair amount of
+  "overlays", usually in the form of Pull Requests from Coq developers
+  in order to keep your plugin compatible with Coq master.
+
+  In order to alleviate the load, you can delegate the merging of such
+  compatibility pull requests to Coq developers themselves, by
+  granting access to the plugin repository or by using `bots` such as
+  [Bors](https://github.com/apps/bors) that allow for automatic
+  management of Pull Requests.
+
+- Plugins in the CI should compile with the OCaml flags that Coq
+  uses. In particular, warnings that are considered fatal by the Coq
+  developers _must_ be also fatal for plugin CI code.
+
 ### Add your development by submitting a pull request
 
 Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 0c89809ee9..4f5988c59c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -254,7 +254,7 @@
 : "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}"
 
 ########################################################################
-# relation-algebra
+# relation_algebra
 ########################################################################
 : "${relation_algebra_CI_REF:=master}"
 : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}"
diff --git a/dev/ci/ci-relation-algebra.sh b/dev/ci/ci-relation_algebra.sh
index 84bed5bdfe..84bed5bdfe 100755
--- a/dev/ci/ci-relation-algebra.sh
+++ b/dev/ci/ci-relation_algebra.sh
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 40c3c32e4f..4533a4dc01 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -20,6 +20,15 @@ General deprecation
   removed. Please, make sure your plugin is warning-free in 8.8 before
   trying to port it over 8.9.
 
+Warnings
+
+- Coq now builds plugins with `-warn-error` enabled by default. The
+  amount of dangerous warnings in plugin code was very high, so we now
+  require plugins in the CI to adhere to the Coq warning policy. We
+  _strongly_ recommend against disabling the default set of warnings.
+  If you have special needs, see the documentation of your build
+  system and/or OCaml for further help.
+
 Names
 
 - Kernel names no longer contain a section path. They now have only two
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 8346b72cb9..35231610fe 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -144,6 +144,10 @@ Here we describe only few of them.
 :CAMLFLAGS:
    can be used to specify additional flags to the |OCaml|
    compiler, like ``-bin-annot`` or ``-w``....
+:OCAMLWARN:
+   it contains a default of ``-warn-error +a-3``, useful to modify
+   this setting; beware this is not recommended for projects in
+   Coq's CI.
 :COQC, COQDEP, COQDOC:
    can be set in order to use alternative binaries
    (e.g. wrappers)
diff --git a/lib/envars.ml b/lib/envars.ml
index 0f4670688b..af8e45b137 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -178,6 +178,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs =
   fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
   fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
   fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags;
+  fprintf f "%sWARN=%s\n" prefix_var_name "-warn-error +a-3";
   fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name
     (if Coq_config.has_natdynlink then "true" else "false");
   fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs)
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 0236c549d5..48b797a3cd 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -38,6 +38,7 @@ DOCDIR            := $(COQMF_DOCDIR)
 OCAMLFIND         := $(COQMF_OCAMLFIND)
 CAMLFLAGS         := $(COQMF_CAMLFLAGS)
 HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
+OCAMLWARN         := $(COQMF_WARN)
 
 @CONF_FILE@: @PROJECT_FILE@
 	@COQ_MAKEFILE_INVOCATION@
@@ -190,9 +191,9 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@
 COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
 
 CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
-
 # ocamldoc fails with unknown argument otherwise
-CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+CAMLFLAGS+=$(OCAMLWARN)
 
 ifneq (,$(TIMING))
 TIMING_ARG=-time