From a4bde2c1504c3fa3efe74586798d5d6f372b40d9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 31 Aug 2018 19:51:50 -0400
Subject: Update dev/doc/release-process: compat+automate

As requested in
https://github.com/coq/coq/issues/8311#issuecomment-415976318
the release process describes the steps to take.

All automatable steps are taken by the new script
dev/tools/update-compat.py

I've tried to make the script relatively easy to update if functions get
renamed or moved, but since it's doing unstructured source manipulation,
it is sort-of fragile.

We could plausibly add a file to the test-suite to ensure that we catch
script-breakage early, but this would require dropping compatibility
support much earlier in the development cycle (the compatibility changes
would have to come right when the new version is branched, rather than
shortly before the beta release).
---
 dev/doc/release-process.md | 30 +++++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

(limited to 'dev/doc')

diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 1821a181f1..7765d4b05c 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -57,7 +57,35 @@
 ## Before the beta release date ##
 
 - [ ] Ensure the Credits chapter has been updated.
-- [ ] Ensure an empty `CompatXX.v` file has been created.
+- [ ] Ensure the compatibility infrastructure has been updated, which consists
+      of the following steps.  Note that all but the final step can be
+      performed automatically by
+      [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so long as
+      you have already updated `coq_version` in
+      [`configure.ml`](/configure.ml).
+  + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header
+        from [`dev/header.ml`](/dev/header.ml)
+  + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of
+        `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X.
+  + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions
+        prior to X.X.
+  + [ ] Update
+        [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
+        with the deleted/added files.
+  + [ ] Remove any notations in the standard library which have `compat "W.W"`.
+  + [ ] Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by
+        bumping all the version numbers by one, and update the interpretations
+        of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and
+        [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg).
+  + [ ] Update the files
+        [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v),
+        [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v),
+        and
+        [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v)
+        by bumping all version numbers by 1.
+  + [ ] Decide what to do about all test-suite files which mention `-compat
+        W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only
+        keep compatibility against the two previous versions)
 - [ ] Ensure that an appropriate version of the plugins we will distribute with
   Coq has been tagged.
 - [ ] Have some people test the recently auto-generated Windows and MacOS
-- 
cgit v1.2.3