Error fatally if update-compat.py gets no flag

c.f. https://github.com/coq/coq/pull/11032#issue-335944369

Also, change the default from python2 to python3 for update-compat while
we're at it, and update file unicode handling accordingly.
(Note that this file still works with both python2 and python3.)

1 files changed, 34 insertions, 28 deletions

diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index c7bb36b6d3..7312c2a5af 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -1,6 +1,8 @@
-#!/usr/bin/env python2
+#!/usr/bin/env python3
 from __future__ import with_statement
+from __future__ import print_function
 import os, re, sys, subprocess
+from io import open
 
 # When passed `--release`, this script sets up Coq to support three
 # `-compat` flag arguments.  If executed manually, this would consist
@@ -84,17 +86,25 @@ 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_file_lines(file_name):
+    with open(file_name, 'rb') as f:
+          lines = f.readlines()
+    return [line.decode('utf-8') for line in lines]
+
+def get_file(file_name):
+    return ''.join(get_file_lines(file_name))
+
 def get_header():
-    with open(HEADER_PATH, 'r') as f: return f.read()
+    return get_file(HEADER_PATH)
 
 HEADER = get_header()
 
-def break_or_continue():
-    msg = 'Press ENTER to continue, or Ctrl+C to break...'
-    try:
-        raw_input(msg)
-    except NameError: # we must be running python3
-        input(msg)
+def fatal_error(msg):
+    if hasattr(sys.stderr, 'buffer'):
+        sys.stderr.buffer.write(msg.encode("utf-8"))
+    else:
+        sys.stderr.write(msg.encode("utf-8"))
+    sys.exit(1)
 
 def maybe_git_add(local_path, suggest_add=True, **args):
     if args['git_add']:
@@ -114,11 +124,10 @@ def maybe_git_rm(local_path, **args):
 
 def get_version(cur_version=None):
     if cur_version is not None: return cur_version
-    with open(CONFIGURE_PATH, 'r') as f:
-        for line in f.readlines():
-            found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line)
-            if len(found) > 0:
-                return found[0]
+    for line in get_file_lines(CONFIGURE_PATH):
+        found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line)
+        if len(found) > 0:
+            return found[0]
     raise Exception("No line 'let coq_version = \"X.X' found in %s" % os.path.relpath(CONFIGURE_PATH, ROOT_PATH))
 
 def compat_name_to_version_name(compat_file_name):
@@ -132,8 +141,7 @@ def version_name_to_compat_name(v, ext='.v'):
 
 # returns (lines of compat files, lines of not compat files
 def get_doc_index_lines():
-    with open(DOC_INDEX_PATH, 'r') as f:
-        lines = f.readlines()
+    lines = get_file_lines(DOC_INDEX_PATH)
     return (tuple(line for line in lines if 'theories/Compat/Coq' in line),
             tuple(line for line in lines if 'theories/Compat/Coq' not in line))
 
@@ -183,7 +191,7 @@ def update_if_changed(contents, new_contents, path, exn_string='%s changed!', su
     if contents is None or contents != new_contents:
         if not assert_unchanged:
             print('Updating %s...' % os.path.relpath(path, ROOT_PATH))
-            with open(path, 'w') as f:
+            with open(path, 'w', encoding='utf-8') as f:
                 f.write(new_contents)
             maybe_git_add(os.path.relpath(path, ROOT_PATH), suggest_add=suggest_add, **args)
         else:
@@ -226,8 +234,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar
             update_file(contents, compat_path, exn_string='%s does not exist!', assert_unchanged=assert_unchanged, **args)
         else:
             # print('Checking %s...' % compat_file)
-            with open(compat_path, 'r') as f:
-                contents = f.read()
+            contents = get_file(compat_path)
             header = HEADER + (EXTRA_HEADER % v)
             if not contents.startswith(HEADER):
                 raise Exception("Invalid header in %s; does not match %s" % (compat_file, os.path.relpath(HEADER_PATH, ROOT_PATH)))
@@ -323,13 +330,13 @@ def check_no_old_versions(old_versions, new_versions, contents, relpath):
                 raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath))
 
 def update_flags_mli(old_versions, new_versions, **args):
-    with open(FLAGS_MLI_PATH, 'r') as f: contents = f.read()
+    contents = get_file(FLAGS_MLI_PATH)
     new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
     check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
     update_if_changed(contents, new_contents, FLAGS_MLI_PATH, **args)
 
 def update_flags_ml(old_versions, new_versions, **args):
-    with open(FLAGS_ML_PATH, 'r') as f: contents = f.read()
+    contents = get_file(FLAGS_ML_PATH)
     new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
     new_contents = update_version_compare(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
     new_contents = update_pr_version(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
@@ -337,13 +344,13 @@ def update_flags_ml(old_versions, new_versions, **args):
     update_if_changed(contents, new_contents, FLAGS_ML_PATH, **args)
 
 def update_coqargs_ml(old_versions, new_versions, **args):
-    with open(COQARGS_ML_PATH, 'r') as f: contents = f.read()
+    contents = get_file(COQARGS_ML_PATH)
     new_contents = update_add_compat_require(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
     check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
     update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args)
 
 def update_g_vernac(old_versions, new_versions, **args):
-    with open(G_VERNAC_PATH, 'r') as f: contents = f.read()
+    contents = get_file(G_VERNAC_PATH)
     new_contents = update_parse_compat_version(new_versions, contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH), **args)
     check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH))
     update_if_changed(contents, new_contents, G_VERNAC_PATH, **args)
@@ -361,7 +368,7 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES
         contents = None
         suggest_add = False
         if os.path.exists(path):
-            with open(path, 'r') as f: contents = f.read()
+            contents = get_file(path)
         else:
             suggest_add = True
         if '%s' in descr: descr = descr % v
@@ -376,7 +383,7 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES
         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()
+    contents = get_file(DOC_INDEX_PATH)
     firstline = '    theories/Compat/AdmitAxiom.v'
     new_contents = ''.join(DOC_INDEX_LINES)
     if firstline not in new_contents:
@@ -386,7 +393,7 @@ def update_doc_index(new_versions, **args):
     update_if_changed(contents, new_contents, DOC_INDEX_PATH, **args)
 
 def update_test_suite_run(**args):
-    with open(TEST_SUITE_RUN_PATH, 'r') as f: contents = f.read()
+    contents = get_file(TEST_SUITE_RUN_PATH)
     new_contents = r'''#!/usr/bin/env bash
 
 # allow running this script from any directory by basing things on where the script lives
@@ -410,7 +417,7 @@ def update_compat_notations(old_versions, new_versions, **args):
     for root, dirs, files in os.walk(os.path.join(ROOT_PATH, 'theories')):
         for fname in files:
             if not fname.endswith('.v'): continue
-            with open(os.path.join(root, fname), 'r') as f: contents = f.read()
+            contents = get_file(os.path.join(root, fname))
             new_contents = update_compat_notations_in(old_versions, new_versions, contents)
             update_if_changed(contents, new_contents, os.path.join(root, fname), **args)
 
@@ -435,9 +442,8 @@ 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 (sometime before branching)
+        fatal_error(r'''ERROR: 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:]:
         if arg == '--assert-unchanged':
             args['assert_unchanged'] = True