Update update-compat.py and release-process.md

In response to review comments by Zimmi48

2 files changed, 84 insertions, 70 deletions

diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index e2ce3ecbd2..d05b6c8eef 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -1,76 +1,23 @@
 # Release process #
 
-## Anytime before the previous version is branched off master ##
-
-- [ ] Update the compatibility infrastructure, which consists of doing
-      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) with
-      the `--release` flag which sets up Coq to support three
-      `-compat` flag arguments).
-  + [ ] Delete the file `theories/Compat/CoqUU.v`, where U.U is four
-        versions prior to the new version X.X.  After this, there
-        should be exactly three `theories/Compat/CoqNN.v` files.
-  + [ ] Update
-        [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
-        with the deleted file.
-  + [ ] Remove any notations in the standard library which have `compat "U.U"`.
-  + [ ] 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).
-
-  + [ ] Remove the file
-        [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v).
-  + [ ] Update
-        [`test-suite/tools/update-compat/run.sh`](/test-suite/tools/update-compat/run.sh)
-        to ensure that it passes `--release` to the `update-compat.py`
-        script.
-  + [ ] Decide what to do about all test-suite files which mention
-        `-compat U.U` or `Coq.Comapt.CoqUU` (which is no longer valid,
-        since we only keep compatibility against the two previous
-        versions on releases)
-
 ## As soon as the previous version branched off master ##
 
 - [ ] Create a new issue to track the release process where you can copy-paste
   the present checklist.
-- [ ] Change the version name to the next major version and the magic numbers
-  (see [#7008](https://github.com/coq/coq/pull/7008/files)).
-- [ ] Update the compatibility infrastructure, which consists of doing
-      the following steps.  Note that all of these steps can be
-      performed automatically by
-      [`dev/tools/update-compat.py`](/dev/tools/update-compat.py).
-      Note that the `update-compat.py` script must be run twice: once
-      *before* branching with the `--release` flag (see above), and
-      again *after* branching with the `--master` flag (which sets up
-      Coq to support four `-compat` flag arguments), *in the same
-      commit* as the one that updates `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.
-  + [ ] Update
-        [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
-        with the added file.
-  + [ ] 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.  Re-create the file
-        [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v)
-        with its version numbers also bumped by 1 (file should have
-        been removed right before branching; see above).
-  + [ ] Update
-        [`test-suite/tools/update-compat/run.sh`](/test-suite/tools/update-compat/run.sh)
-        to ensure that it passes `--master` to the `update-compat.py`
-        script.
+- [ ] Change the version name to the next major version and the magic
+  numbers (see [#7008](https://github.com/coq/coq/pull/7008/files)).
+
+  Additionally, in the same commit, update the compatibility
+  infrastructure, which consists of invoking
+  [`dev/tools/update-compat.py`](../tools/update-compat.py) with the
+  `--master` flag.
+
+  Note that the `update-compat.py` script must be run twice: once
+  *immediately after* branching with the `--master` flag (which sets
+  up Coq to support four `-compat` flag arguments), *in the same
+  commit* as the one that updates `coq_version` in
+  [`configure.ml`](../../configure.ml), and once again later on before
+  the next branch point with the `--release` flag (see next section).
 - [ ] Put the corresponding alpha tag using `git tag -s`.
   The `VX.X+alpha` tag marks the first commit to be in `master` and not in the
   branch of the previous version.
@@ -79,6 +26,19 @@
   release date) and put this information in the milestone (using the
   description and due date fields).
 
+## Anytime after the previous version is branched off master ##
+
+- [ ] Update the compatibility infrastructure to the next release,
+  which consists of invoking
+  [`dev/tools/update-compat.py`](../tools/update-compat.py) with the
+  `--release` flag; this sets up Coq to support three `-compat` flag
+  arguments.  To ensure that CI passes, you will have to decide what
+  to do about all test-suite files which mention `-compat U.U` or
+  `Coq.Comapt.CoqUU` (which is no longer valid, since we only keep
+  compatibility against the two previous versions on releases), and
+  you may have to prepare overlays for projects using the
+  compatibility flags.
+
 ## About one month before the beta ##
 
 - [ ] Create the `X.X.0` milestone and set its due date.
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index 13bbf76198..bde00a2f0d 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -2,6 +2,60 @@
 from __future__ import with_statement
 import os, re, sys, subprocess
 
+# When passed `--release`, this script sets up Coq to support three
+# `-compat` flag arguments.  If executed manually, this would consist
+# of doing the following steps:
+#
+# - Delete the file `theories/Compat/CoqUU.v`, where U.U is four
+#   versions prior to the new version X.X.  After this, there
+#   should be exactly three `theories/Compat/CoqNN.v` files.
+# - Update
+#   [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
+#   with the deleted file.
+# - Remove any notations in the standard library which have `compat "U.U"`.
+# - 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).
+#
+# - Remove the file
+#   [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v).
+# - Update
+#   [`test-suite/tools/update-compat/run.sh`](/test-suite/tools/update-compat/run.sh)
+#   to ensure that it passes `--release` to the `update-compat.py`
+#   script.
+
+# When passed the `--master` flag, this script sets up Coq to support
+# four `-compat` flag arguments.  If executed manually, this would
+# consist of doing the following steps:
+#
+# - 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.
+# - Update
+#   [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
+#   with the added file.
+# - 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.  Re-create the file
+#   [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v)
+#   with its version numbers also bumped by 1 (file should have
+#   been removed before branching; see above).
+# - Update
+#   [`test-suite/tools/update-compat/run.sh`](/test-suite/tools/update-compat/run.sh)
+#   to ensure that it passes `--master` to the `update-compat.py`
+#   script.
+
+
+
 # Obtain the absolute path of the script being run.  By assuming that
 # the script lives in dev/tools/, and basing all calls on the path of
 # the script, rather than the current working directory, we can be
@@ -51,8 +105,8 @@ def maybe_git_add(local_path, suggest_add=True, **args):
 
 def maybe_git_rm(local_path, **args):
     if args['git_add']:
-        print("Running 'git rm --cached %s'..." % local_path)
-        retc = subprocess.call(['git', 'rm', '--cached', local_path], cwd=ROOT_PATH)
+        print("Running 'git rm %s'..." % local_path)
+        retc = subprocess.call(['git', 'rm', local_path], cwd=ROOT_PATH)
         if retc is not None and retc != 0:
             print('!!! Process returned code %d' % retc)
 
@@ -379,7 +433,7 @@ def parse_args(argv):
         'git_add': False,
     }
     if '--master' not in argv and '--release' not in argv:
-        print(r'''WARNING: You should pass either --release (right before branching)
+        print(r'''WARNING: You should pass either --release (sometime before branching)
   or --master (right after branching and updating the version number in version.ml)''')
         if '--assert-unchanged' not in args: break_or_continue()
     for arg in argv[1:]: