[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

4 files changed, 30 insertions, 1 deletions

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