Update update-compat.py script

It now removes the outdated `CompatOldOldFlag.v` file on `--release`,
and it now correctly updates `bug_9166.v` which seems to specifically be
about the compat flag behavior.

Additionally, it inserts an "autogenerated" notice at top of the two bug
files, and makes them read-only.

1 files changed, 36 insertions, 2 deletions

diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index bde00a2f0d..ff9b32fe78 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -74,6 +74,7 @@ COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
 G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg')
 DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
 BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v')
+BUG_9166_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_9166.v')
 TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
 TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
                          for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
@@ -81,6 +82,9 @@ TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-
 # sanity check that we are where we think we are
 assert(os.path.normpath(os.path.realpath(SCRIPT_PATH)) == os.path.normpath(os.path.realpath(os.path.join(ROOT_PATH, 'dev', 'tools'))))
 assert(os.path.exists(CONFIGURE_PATH))
+BUG_HEADER = r"""(* DO NOT MODIFY THIS FILE DIRECTLY *)
+(* It is autogenerated by %s. *)
+""" % os.path.relpath(os.path.realpath(__file__), ROOT_PATH)
 
 def get_header():
     with open(HEADER_PATH, 'r') as f: return f.read()
@@ -190,6 +194,15 @@ def update_if_changed(contents, new_contents, path, exn_string='%s changed!', su
                 print_diff(contents, new_contents)
             raise Exception(exn_string % os.path.relpath(path, ROOT_PATH))
 
+def remove_if_exists(path, exn_string='%s exists when it should not!', assert_unchanged=False, **args):
+    if os.path.exists(path):
+        if not assert_unchanged:
+            print('Removing %s...' % os.path.relpath(path, ROOT_PATH))
+            os.remove(path)
+            maybe_git_rm(os.path.relpath(path, ROOT_PATH), **args)
+        else:
+            raise Exception(exn_string % os.path.relpath(path, ROOT_PATH))
+
 def update_file(new_contents, path, **args):
     update_if_changed(None, new_contents, path, **args)
 
@@ -343,7 +356,7 @@ def update_flags(old_versions, new_versions, **args):
     update_coqargs_ml(old_versions, new_versions, **args)
     update_g_vernac(old_versions, new_versions, **args)
 
-def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, **args):
+def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, test_suite_outdated_paths=tuple(), **args):
     assert(len(new_versions) == len(test_suite_paths))
     assert(len(new_versions) == len(test_suite_descriptions))
     for i, (v, path, descr) in enumerate(zip(new_versions, test_suite_paths, test_suite_descriptions)):
@@ -361,6 +374,8 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES
         lines.append('')
         new_contents = '\n'.join(lines)
         update_if_changed(contents, new_contents, path, suggest_add=suggest_add, **args)
+    for path in test_suite_outdated_paths:
+        remove_if_exists(path, assert_unchanged=assert_unchanged, **args)
 
 def update_doc_index(new_versions, **args):
     with open(DOC_INDEX_PATH, 'r') as f: contents = f.read()
@@ -391,12 +406,29 @@ def update_bug_4789(new_versions, **args):
     # currently-supported compat version, which should never be the
     # current version
     with open(BUG_4798_PATH, 'r') as f: contents = f.read()
-    new_contents = r"""Check match 2 with 0 => 0 | S n => n end.
+    new_contents = BUG_HEADER + r"""Check match 2 with 0 => 0 | S n => n end.
 Notation "|" := 1 (compat "%s").
 Check match 2 with 0 => 0 | S n => n end. (* fails *)
 """ % new_versions[0]
     update_if_changed(contents, new_contents, BUG_4798_PATH, **args)
 
+def update_bug_9166(new_versions, **args):
+    # we always update this compat notation to oldest
+    # currently-supported compat version, which should never be the
+    # current version
+    with open(BUG_9166_PATH, 'r') as f: contents = f.read()
+    new_contents = BUG_HEADER + r"""Set Warnings "+deprecated".
+
+Notation bar := option (compat "%s").
+
+Definition foo (x: nat) : nat :=
+  match x with
+  | 0 => 0
+  | S bar => bar
+  end.
+""" % new_versions[0]
+    update_if_changed(contents, new_contents, BUG_9166_PATH, **args)
+
 def update_compat_notations_in(old_versions, new_versions, contents):
     for v in old_versions:
         if v not in new_versions:
@@ -469,6 +501,7 @@ if __name__ == '__main__':
     new_versions = get_new_versions(known_versions, **args)
     assert(len(TEST_SUITE_PATHS) >= args['number_of_compat_versions'])
     args['test_suite_paths'] = tuple(TEST_SUITE_PATHS[-args['number_of_compat_versions']:])
+    args['test_suite_outdated_paths'] = tuple(TEST_SUITE_PATHS[:-args['number_of_compat_versions']])
     args['test_suite_descriptions'] = tuple(TEST_SUITE_DESCRIPTIONS[-args['number_of_compat_versions']:])
     update_compat_files(known_versions, new_versions, **args)
     update_flags(known_versions, new_versions, **args)
@@ -476,5 +509,6 @@ if __name__ == '__main__':
     update_test_suite_run(**args)
     update_doc_index(new_versions, **args)
     update_bug_4789(new_versions, **args)
+    update_bug_9166(new_versions, **args)
     update_compat_notations(known_versions, new_versions, **args)
     display_git_grep(known_versions, new_versions)