diff options
Diffstat (limited to 'dev/tools/update-compat.py')
| -rwxr-xr-x | dev/tools/update-compat.py | 165 |
1 files changed, 42 insertions, 123 deletions
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index c7bb36b6d3..ddb0362186 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 @@ -13,10 +15,8 @@ import os, re, sys, subprocess # [`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). +# - Update the function `get_compat_file` in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) +# by bumping all the version numbers by one. # # - Remove the file # [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v). @@ -36,10 +36,8 @@ import os, re, sys, subprocess # - 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 function `get_compat_file` in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) +# by bumping all the version numbers by one. # - Update the files # [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v), # [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v), @@ -68,10 +66,7 @@ DEFAULT_NUMBER_OF_OLD_VERSIONS = 2 RELEASE_NUMBER_OF_OLD_VERSIONS = 2 MASTER_NUMBER_OF_OLD_VERSIONS = 3 EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n' -FLAGS_MLI_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.mli') -FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml') 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') 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) @@ -84,17 +79,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 +117,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 +134,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 +184,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 +227,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))) @@ -241,118 +241,38 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar contents = contents.replace(header, '%s\n%s' % (header, line)) update_file(contents, compat_path, exn_string=('Compat file %%s is missing line %s' % line), assert_unchanged=assert_unchanged, **args) -def update_compat_versions_type_line(new_versions, contents, relpath): - compat_version_string = ' | '.join(['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']) - new_compat_line = 'type compat_version = %s' % compat_version_string - new_contents = re.sub(r'^type compat_version = .*$', new_compat_line, contents, flags=re.MULTILINE) - if new_compat_line not in new_contents: - raise Exception("Could not find 'type compat_version =' in %s" % relpath) - return new_contents - -def update_version_compare(new_versions, contents, relpath): - first_line = 'let version_compare v1 v2 = match v1, v2 with' - new_lines = [first_line] - for v in new_versions[:-1]: - V = 'V%s_%s' % tuple(v.split('.')) - new_lines.append(' | %s, %s -> 0' % (V, V)) - new_lines.append(' | %s, _ -> -1' % V) - new_lines.append(' | _, %s -> 1' % V) - new_lines.append(' | Current, Current -> 0') - new_lines = '\n'.join(new_lines) - new_contents = re.sub(first_line + '.*' + 'Current, Current -> 0', new_lines, contents, flags=re.DOTALL|re.MULTILINE) - if new_lines not in new_contents: - raise Exception('Could not find version_compare in %s' % relpath) - return new_contents - -def update_pr_version(new_versions, contents, relpath): - first_line = 'let pr_version = function' - new_lines = [first_line] - for v in new_versions[:-1]: - V = 'V%s_%s' % tuple(v.split('.')) - new_lines.append(' | %s -> "%s"' % (V, v)) - new_lines.append(' | Current -> "current"') - new_lines = '\n'.join(new_lines) - new_contents = re.sub(first_line + '.*' + 'Current -> "current"', new_lines, contents, flags=re.DOTALL|re.MULTILINE) - if new_lines not in new_contents: - raise Exception('Could not find pr_version in %s' % relpath) - return new_contents - -def update_add_compat_require(new_versions, contents, relpath): - first_line = 'let add_compat_require opts v =' - new_lines = [first_line, ' match v with'] - for v in new_versions[:-1]: - V = 'V%s_%s' % tuple(v.split('.')) - new_lines.append(' | Flags.%s -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % (V, version_name_to_compat_name(v, ext=''))) - new_lines.append(' | Flags.Current -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % version_name_to_compat_name(new_versions[-1], ext='')) - new_lines = '\n'.join(new_lines) - new_contents = re.sub(first_line + '.*' + 'Flags.Current -> add_vo_require opts "Coq.Compat.[^"]+" None .Some false.', new_lines, contents, flags=re.DOTALL|re.MULTILINE) - if new_lines not in new_contents: - raise Exception('Could not find add_compat_require in %s' % relpath) - return new_contents - -def update_parse_compat_version(new_versions, contents, relpath, **args): +def update_get_compat_file(new_versions, contents, relpath): line_count = 3 # 1 for the first line, 1 for the invalid flags, and 1 for Current - first_line = 'let parse_compat_version = let open Flags in function' + first_line = 'let get_compat_file = function' split_contents = contents[contents.index(first_line):].split('\n') while True: cur_line = split_contents[:line_count][-1] if re.match(r'^ \| \([0-9 "\.\|]*\) as s ->$', cur_line) is not None: break - elif re.match(r'^ \| "[0-9\.]*" -> V[0-9_]*$', cur_line) is not None: + elif re.match(r'^ \| "[0-9\.]*" -> "Coq.Compat.Coq[0-9]*"$', cur_line) is not None: line_count += 1 else: - raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line))) + raise Exception('Could not recognize line %d of get_compat_file in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line))) old_function_lines = split_contents[:line_count] all_versions = re.findall(r'"([0-9\.]+)"', ''.join(old_function_lines)) invalid_versions = tuple(i for i in all_versions if i not in new_versions) new_function_lines = [first_line] - for v, V in reversed(list(zip(new_versions, ['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']))): + for v, V in reversed(list(zip(new_versions, ['"Coq.Compat.Coq%s%s"' % tuple(v.split('.')) for v in new_versions]))): new_function_lines.append(' | "%s" -> %s' % (v, V)) new_function_lines.append(' | (%s) as s ->' % ' | '.join('"%s"' % v for v in invalid_versions)) new_lines = '\n'.join(new_function_lines) new_contents = contents.replace('\n'.join(old_function_lines), new_lines) if new_lines not in new_contents: - raise Exception('Could not find parse_compat_version in %s' % relpath) + raise Exception('Could not find get_compat_file in %s' % relpath) return new_contents -def check_no_old_versions(old_versions, new_versions, contents, relpath): - for v in old_versions: - if v not in new_versions: - V = 'V%s_%s' % tuple(v.split('.')) - if V in contents: - 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() - 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() - 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)) - check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) - 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() - 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)) + contents = get_file(COQARGS_ML_PATH) + new_contents = update_get_compat_file(new_versions, 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() - 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) - def update_flags(old_versions, new_versions, **args): - update_flags_mli(old_versions, new_versions, **args) - update_flags_ml(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, test_suite_outdated_paths=tuple(), **args): assert(len(new_versions) == len(test_suite_paths)) @@ -361,7 +281,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 +296,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 +306,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 +330,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 +355,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 |