M .github/CODEOWNERS => .github/CODEOWNERS +0 -3
@@ 279,9 279,6 @@
/dev/tools/ @coq/dev-tools-maintainers
-/dev/tools/update-compat.py @coq/compat-maintainers
-/test-suite/tools/update-compat/ @coq/compat-maintainers
-
########## Dune ##########
/.ocamlinit @coq/build-maintainers
M boot/usage.ml => boot/usage.ml +5 -3
@@ 31,10 31,12 @@ let print_usage_common co command =
\n -coqlib dir set the coq standard library directory\
\n -exclude-dir f exclude subdirectories named f for option -R\
\n\
-\n -boot don't bind the `Coq.` prefix to the default -coqlib dir\
-\n -noinit don't load Coq.Init.Prelude on start \
+\n -boot don't bind the `Stdlib.` prefix to the default -coqlib dir\
+\n -noinit don't load Stdlib.Init.Prelude on start\
\n -nois (idem)\
-\n -compat X.Y provides compatibility support for Coq version X.Y\
+\n -compat X.Y same as -compat-from Stdlib CoqXY\
+\n -compat-from root lib same as -require-import-from root lib, except that\
+\n a non existing file only produces a warning\
\n\
\n -load-vernac-source f load Coq file f.v (Load \"f\".)\
\n -l f (idem)\
A dev/ci/user-overlays/19370-proux01-improve-compat.sh => dev/ci/user-overlays/19370-proux01-improve-compat.sh +1 -0
@@ 0,0 1,1 @@
+overlay serapi https://github.com/proux01/coq-serapi coq_19370 19370
M dev/doc/release-process.md => dev/doc/release-process.md +0 -3
@@ 10,11 10,8 @@
- [ ] Create both the upcoming final release (`X.X.0`) and the following major release (`Y.Y+rc1`) milestones if they do not already exist.
- [ ] Send an announcement of the upcoming branching date on Coqdev + the Coq development category on Discourse (coqdev@inria.fr + coq+coq-development@discoursemail.com) and ask people to remove from the `X.X+rc1` milestone any feature and clean up PRs that they already know won't be ready on time.
-- [ ] In a PR on `master`, call [`dev/tools/update-compat.py`](../tools/update-compat.py) with the `--release` flag; this sets up Coq to support three `-compat` flag arguments including the upcoming one (instead of four). To ensure that CI passes, you will have to decide what to do about all test-suite files that mention `-compat U.U` or `Coq.Compat.CoqUU` (which is no longer valid, since we only keep compatibility against the two previous versions), and you may have to ping maintainers of projects that are still relying on the old compatibility flag so that they fix this.
- [ ] Make sure that this change is merged in time for the branching date.
- [ ] Prepare a PR on `master` (not yet to be merged) changing the version name to the next major version and both magic numbers in [`tools/configure/configure.ml`](../../tools/configure/configure.ml). For example, for `8.5`, the version name will be `8.5+alpha` while the magic numbers will end with `80490`.
- 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 in preparation of the release with the `--release` flag (see earlier in this section) and once on the branching date with the `--master` flag to mark the start of the next version.
This PR should be opened before the branching date to have time to deal with CI issues, but should not be merged until branching.
## On the branching date ##
D dev/tools/update-compat.py => dev/tools/update-compat.py +0 -399
@@ 1,399 0,0 @@
-#!/usr/bin/env python3
-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
-# 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 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).
-# - 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 Stdlib.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 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),
-# 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
-# robust to users who choose to run the script from any location.
-SCRIPT_PATH = os.path.dirname(os.path.realpath(__file__))
-ROOT_PATH = os.path.realpath(os.path.join(SCRIPT_PATH, '..', '..'))
-CONFIGURE_PATH = os.path.join(ROOT_PATH, 'tools/configure/configure.ml')
-HEADER_PATH = os.path.join(ROOT_PATH, 'dev', 'header.ml')
-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'
-COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'sysinit', 'coqargs.ml')
-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)
- for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
-TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-minus-one', '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_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():
- return get_file(HEADER_PATH)
-
-HEADER = get_header()
-
-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']:
- print("Running 'git add %s'..." % local_path)
- retc = subprocess.call(['git', 'add', local_path], cwd=ROOT_PATH)
- if retc is not None and retc != 0:
- print('!!! Process returned code %d' % retc)
- elif suggest_add:
- print(r"!!! Don't forget to 'git add %s'!" % local_path)
-
-def maybe_git_rm(local_path, **args):
- if args['git_add']:
- 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)
-
-def get_version(cur_version=None):
- if cur_version is not None: return cur_version
- 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):
- assert(compat_file_name.startswith('Coq') and compat_file_name.endswith('.v'))
- v = compat_file_name[len('Coq'):][:-len('.v')]
- assert(len(v) == 2 or (len(v) >= 2 and v[0] in ('8', '9'))) # we'll have to change this scheme when we hit Coq 10.*
- return '%s.%s' % (v[0], v[1:])
-
-def version_name_to_compat_name(v, ext='.v'):
- return 'Coq%s%s%s' % tuple(v.split('.') + [ext])
-
-# returns (lines of compat files, lines of not compat files
-def get_doc_index_lines():
- 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))
-
-COMPAT_INDEX_LINES, DOC_INDEX_LINES = get_doc_index_lines()
-
-def version_to_int_pair(v):
- return tuple(map(int, v.split('.')))
-
-def get_known_versions():
- # We could either get the files from the doc index, or from the
- # directory list. We assume that the doc index is more
- # representative. If we wanted to use the directory list, we
- # would do:
- # compat_files = os.listdir(os.path.join(ROOT_PATH, 'theories', 'Compat'))
- compat_files = re.findall(r'Coq[^\.]+\.v', '\n'.join(COMPAT_INDEX_LINES))
- return tuple(sorted((compat_name_to_version_name(i) for i in compat_files if i.startswith('Coq') and i.endswith('.v')), key=version_to_int_pair))
-
-def get_new_versions(known_versions, **args):
- if args['cur_version'] in known_versions:
- assert(known_versions[-1] == args['cur_version'])
- known_versions = known_versions[:-1]
- assert(len(known_versions) >= args['number_of_old_versions'])
- return tuple(list(known_versions[-args['number_of_old_versions']:]) + [args['cur_version']])
-
-def print_diff(olds, news, numch=30):
- for ch in range(min(len(olds), len(news))):
- if olds[ch] != news[ch]:
- print('Character %d differs:\nOld: %s\nNew: %s' % (ch, repr(olds[ch:][:numch]), repr(news[ch:][numch])))
- return
- ch = min(len(olds), len(news))
- assert(len(olds) != len(news))
- print('Strings are different lengths:\nOld tail: %s\nNew tail: %s' % (repr(olds[ch:]), repr(news[ch:])))
-
-def update_shebang_to_match(contents, new_contents, path):
- contents_lines = contents.split('\n')
- new_contents_lines = new_contents.split('\n')
- if not (contents_lines[0].startswith('#!/') and contents_lines[0].endswith('bash')):
- raise Exception('Unrecognized #! line in existing %s: %s' % (os.path.relpath(path, ROOT_PATH), repr(contents_lines[0])))
- if not (new_contents_lines[0].startswith('#!/') and new_contents_lines[0].endswith('bash')):
- raise Exception('Unrecognized #! line in new %s: %s' % (os.path.relpath(path, ROOT_PATH), repr(new_contents_lines[0])))
- new_contents_lines[0] = contents_lines[0]
- return '\n'.join(new_contents_lines)
-
-def update_if_changed(contents, new_contents, path, exn_string='%s changed!', suggest_add=False, pass_through_shebang=False, assert_unchanged=False, **args):
- if contents is not None and pass_through_shebang:
- new_contents = update_shebang_to_match(contents, new_contents, path)
- 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', encoding='utf-8') as f:
- f.write(new_contents)
- maybe_git_add(os.path.relpath(path, ROOT_PATH), suggest_add=suggest_add, **args)
- else:
- if contents is not None:
- print('Unexpected change:\nOld contents:\n%s\n\nNew contents:\n%s\n' % (contents, new_contents))
- 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)
-
-def update_compat_files(old_versions, new_versions, assert_unchanged=False, **args):
- for v in old_versions:
- if v not in new_versions:
- compat_file = os.path.join('theories', 'Compat', version_name_to_compat_name(v))
- if not assert_unchanged:
- print('Removing %s...' % compat_file)
- compat_path = os.path.join(ROOT_PATH, compat_file)
- os.rename(compat_path, compat_path + '.bak')
- maybe_git_rm(compat_file, **args)
- else:
- raise Exception('%s exists!' % compat_file)
- for v, next_v in zip(new_versions, list(new_versions[1:]) + [None]):
- compat_file = os.path.join('theories', 'Compat', version_name_to_compat_name(v))
- compat_path = os.path.join(ROOT_PATH, compat_file)
- if not os.path.exists(compat_path):
- print('Creating %s...' % compat_file)
- contents = HEADER + (EXTRA_HEADER % v)
- if next_v is not None:
- contents += '\nRequire Export Stdlib.Compat.%s.\n' % version_name_to_compat_name(next_v, ext='')
- update_file(contents, compat_path, exn_string='%s does not exist!', assert_unchanged=assert_unchanged, **args)
- else:
- # print('Checking %s...' % compat_file)
- 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)))
- if not contents.startswith(header):
- raise Exception("Invalid header in %s; missing line %s" % (compat_file, EXTRA_HEADER.strip('\n') % v))
- if next_v is not None:
- line = 'Require Export Stdlib.Compat.%s.' % version_name_to_compat_name(next_v, ext='')
- if ('\n%s\n' % line) not in contents:
- if not contents.startswith(header + '\n'):
- contents = contents.replace(header, header + '\n')
- 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_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 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\.]*" -> "Stdlib.Compat.Coq[0-9]*"$', cur_line) is not None:
- line_count += 1
- else:
- 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, ['"Stdlib.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 get_compat_file in %s' % relpath)
- return new_contents
-
-def update_coqargs_ml(old_versions, new_versions, **args):
- 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_flags(old_versions, new_versions, **args):
- update_coqargs_ml(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))
- assert(len(new_versions) == len(test_suite_descriptions))
- for i, (v, path, descr) in enumerate(zip(new_versions, test_suite_paths, test_suite_descriptions)):
- contents = None
- suggest_add = False
- if os.path.exists(path):
- contents = get_file(path)
- else:
- suggest_add = True
- if '%s' in descr: descr = descr % v
- lines = ['(* -*- coq-prog-args: ("-compat" "%s") -*- *)' % v,
- '(** Check that the %s compatibility flag actually requires the relevant modules. *)' % descr]
- for imp_v in reversed(new_versions[i:]):
- lines.append('Import Stdlib.Compat.%s.' % version_name_to_compat_name(imp_v, ext=''))
- 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):
- contents = get_file(DOC_INDEX_PATH)
- firstline = ' theories/Compat/AdmitAxiom.v'
- new_contents = ''.join(DOC_INDEX_LINES)
- if firstline not in new_contents:
- raise Exception("Could not find line '%s' in %s" % (firstline, os.path.relpath(DOC_INDEX_PATH, ROOT_PATH)))
- extra_lines = [' theories/Compat/%s' % version_name_to_compat_name(v) for v in new_versions]
- new_contents = new_contents.replace(firstline, '\n'.join([firstline] + extra_lines))
- update_if_changed(contents, new_contents, DOC_INDEX_PATH, **args)
-
-def update_test_suite_run(**args):
- 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
-SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"
-
-# we assume that the script lives in test-suite/tools/update-compat/,
-# and that update-compat.py lives in dev/tools/
-cd "${SCRIPT_DIR}/../../.."
-dev/tools/update-compat.py --assert-unchanged %s || exit $?
-''' % ' '.join([('--master' if args['master'] else ''), ('--release' if args['release'] else '')]).strip()
- update_if_changed(contents, new_contents, TEST_SUITE_RUN_PATH, pass_through_shebang=True, **args)
-
-def update_compat_notations_in(old_versions, new_versions, contents):
- for v in old_versions:
- if v not in new_versions:
- reg = re.compile(r'^[ \t]*(?:Notation|Infix)[^\n]*?compat "%s"[^\n]*?\n' % v, flags=re.MULTILINE)
- contents = re.sub(r'^[ \t]*(?:Notation|Infix)[^\n]*?compat "%s"[^\n]*?\n' % v, '', contents, flags=re.MULTILINE)
- return contents
-
-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
- 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)
-
-def display_git_grep(old_versions, new_versions):
- Vs = ['V%s_%s' % tuple(v.split('.')) for v in old_versions if v not in new_versions]
- compat_vs = ['compat "%s"' % v for v in old_versions if v not in new_versions]
- all_options = tuple(Vs + compat_vs)
- options = (['"-compat" "%s"' % v for v in old_versions if v not in new_versions] +
- [version_name_to_compat_name(v, ext='') for v in old_versions if v not in new_versions])
- if len(options) > 0 or len(all_options) > 0:
- print('To discover what files require manual updating, run:')
- if len(options) > 0: print("git grep -- '%s' test-suite/" % r'\|'.join(options))
- if len(all_options) > 0: print("git grep -- '%s'" % r'\|'.join(all_options))
-
-def parse_args(argv):
- args = {
- 'assert_unchanged': False,
- 'cur_version': None,
- 'number_of_old_versions': None,
- 'master': False,
- 'release': False,
- 'git_add': False,
- }
- if '--master' not in argv and '--release' not in argv:
- 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)''')
- for arg in argv[1:]:
- if arg == '--assert-unchanged':
- args['assert_unchanged'] = True
- elif arg == '--git-add':
- args['git_add'] = True
- elif arg == '--master':
- args['master'] = True
- if args['number_of_old_versions'] is None: args['number_of_old_versions'] = MASTER_NUMBER_OF_OLD_VERSIONS
- elif arg == '--release':
- args['release'] = True
- if args['number_of_old_versions'] is None: args['number_of_old_versions'] = RELEASE_NUMBER_OF_OLD_VERSIONS
- elif arg.startswith('--cur-version='):
- args['cur_version'] = arg[len('--cur-version='):]
- assert(len(args['cur_version'].split('.')) == 2)
- assert(all(map(str.isdigit, args['cur_version'].split('.'))))
- elif arg.startswith('--number-of-old-versions='):
- args['number_of_old_versions'] = int(arg[len('--number-of-old-versions='):])
- else:
- print('USAGE: %s [--assert-unchanged] [--cur-version=NN.NN] [--number-of-old-versions=NN] [--git-add]' % argv[0])
- print('')
- print('ERROR: Unrecognized argument: %s' % arg)
- sys.exit(1)
- if args['number_of_old_versions'] is None: args['number_of_old_versions'] = DEFAULT_NUMBER_OF_OLD_VERSIONS
- return args
-
-if __name__ == '__main__':
- args = parse_args(sys.argv)
- args['cur_version'] = get_version(args['cur_version'])
- args['number_of_compat_versions'] = args['number_of_old_versions'] + 1
- known_versions = get_known_versions()
- 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)
- update_test_suite(new_versions, **args)
- update_test_suite_run(**args)
- update_doc_index(new_versions, **args)
- update_compat_notations(known_versions, new_versions, **args)
- display_git_grep(known_versions, new_versions)
A doc/changelog/09-cli-tools/19370-compat-from.rst => doc/changelog/09-cli-tools/19370-compat-from.rst +12 -0
@@ 0,0 1,12 @@
+- **Added:**
+ :ref:`command line option <command-line-options>` ``-compat-from``
+ to enable writing compatibility files for libraries similarly to the
+ ``-compat`` option for Coq
+ (`#19370 <https://github.com/coq/coq/pull/19370>`_,
+ by Pierre Roux).
+- **Added:**
+ The ``-compat`` :ref:`command line option <command-line-options>`
+ now silences deprecation warnings that were introduced since the
+ given version
+ (`#19370 <https://github.com/coq/coq/pull/19370>`_,
+ by Pierre Roux).
A doc/changelog/09-cli-tools/19370-compat-warning.rst => doc/changelog/09-cli-tools/19370-compat-warning.rst +7 -0
@@ 0,0 1,7 @@
+- **Changed:**
+ The ``-compat`` :ref:`command line option <command-line-options>`
+ now raises a warning rather than an error when the compatibility file
+ doesn't exist. This enables easier use of the compat mechanism with
+ versions where the compatibility file doesn't exist yet
+ (`#19370 <https://github.com/coq/coq/pull/19370>`_,
+ by Pierre Roux).
M doc/sphinx/practical-tools/coq-commands.rst => doc/sphinx/practical-tools/coq-commands.rst +7 -5
@@ 419,11 419,13 @@ and ``coqtop``, unless stated otherwise:
*string* must be :n:`"@setting_name"`.
See the :ref:`note above <interleave-command-line>` regarding the order
of command-line options.
-:-compat *version*: Load a file that sets a few options to maintain
- partial backward-compatibility with a previous version. This is
- equivalent to :cmd:`Require Import` `Stdlib.Compat.CoqXXX` with `XXX`
- one of the last three released versions (including the current
- version). Note that the :ref:`explanations above
+:-compat *version*: same as ``-compat-from Stdlib Coq<version>``
+:-compat-from *root* *library*: Loads a file that sets a few options to maintain
+ partial backward-compatibility with a previous version. This is
+ equivalent to ``-require-import-from <root> <library>``
+ except that a non existing file only produces a warning (so that the option can
+ be uniformly used on older versions that didn't offer the compat file yet).
+ Note that the :ref:`explanations above
<interleave-command-line>` regarding the order of command-line
options apply, and this could be relevant if you are resetting some
of the compatibility options.
M doc/stdlib/index-list.html.template => doc/stdlib/index-list.html.template +0 -1
@@ 705,7 705,6 @@ through the <tt>Require Import</tt> command.</p>
theories/Compat/Coq818.v
theories/Compat/Coq819.v
theories/Compat/Coq820.v
- theories/Compat/Coq90.v
user-contrib/Ltac2/Compat/Coq818.v
user-contrib/Ltac2/Compat/Coq819.v
</dd>
M lib/deprecation.ml => lib/deprecation.ml +3 -0
@@ 94,5 94,8 @@ module Version = struct
let v8_19 = get_generic_cat "8.19"
let v8_20 = get_generic_cat "8.20"
let v9_0 = get_generic_cat "9.0"
+ (* When adding a new version here, please also add
+ #[export] Set Warnings "-deprecated-since-X.Y".
+ in theories/Compat/CoqX{Y-1}.v *)
end
M stm/asyncTaskQueue.ml => stm/asyncTaskQueue.ml +1 -1
@@ 135,7 135,7 @@ module Make(T : Task) () = struct
| "-async-proofs-worker-priority" | "-worker-id") :: _ :: tl ->
set_slave_opt tl
(* Options to discard: 2 arguments *)
- | ( "-rifrom" | "-refrom" | "-rfrom"
+ | ( "-compat-from" | "-rifrom" | "-refrom" | "-rfrom"
| "-require-import-from" | "-require-export-from") :: _ :: _ :: tl ->
set_slave_opt tl
(* We need to pass some options with one argument *)
M sysinit/coqargs.ml => sysinit/coqargs.ml +9 -26
@@ 40,7 40,7 @@ type option_command =
| OptionUnset
| OptionAppend of string
-type require_injection = { lib: string; prefix: string option; export: Lib.export_flag option; }
+type require_injection = { lib: string; prefix: string option; export: Lib.export_flag option; allow_failure: bool }
type injection_command =
| OptionInjection of (Goptions.option_name * option_command)
@@ 167,8 167,8 @@ let add_vo_include opts unix_path coq_path implicit =
{ opts with pre = { opts.pre with vo_includes = {
unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }}
-let add_vo_require opts d p export =
- { opts with pre = { opts.pre with injections = RequireInjection {lib=d; prefix=p; export} :: opts.pre.injections }}
+let add_vo_require opts d ?(allow_failure=false) p export =
+ { opts with pre = { opts.pre with injections = RequireInjection {lib=d; prefix=p; export; allow_failure} :: opts.pre.injections }}
let add_load_vernacular opts verb s =
{ opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
@@ 230,26 230,6 @@ let set_option = let open Goptions in function
| opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
| opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v
-let get_compat_file = function
- | "9.0" -> "Stdlib.Compat.Coq90"
- | "8.20" -> "Stdlib.Compat.Coq820"
- | "8.19" -> "Stdlib.Compat.Coq819"
- | "8.18" -> "Stdlib.Compat.Coq818"
- | ("8.17" | "8.16" | "8.15" | "8.14" | "8.13" | "8.12" | "8.11" | "8.10" | "8.9" | "8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
- CErrors.user_err
- Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
- | s ->
- CErrors.user_err
- Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
-
-(* Workaround for the OCaml parser using regex in update-compat.py *)
-let get_compat_files v =
- let coq_compat = get_compat_file v in
- match v with
- | "8.19" -> coq_compat :: ["Ltac2.Compat.Coq819"]
- | "8.18" | "8.17" -> coq_compat :: ["Ltac2.Compat.Coq818"]
- | _ -> [coq_compat]
-
let to_opt_key = Str.(split (regexp " +"))
let parse_option_set opt =
@@ 314,8 294,8 @@ let parse_args ~usage ~init arglist : t * string list =
}}
|"-compat" ->
- get_compat_files (next ()) |>
- List.fold_left (fun oval lib -> add_vo_require oval lib None (Some Lib.Import)) oval
+ let xy = String.(concat "" ("Coq" :: split_on_char '.' (next ()))) in
+ add_vo_require oval xy ~allow_failure:true (Some "Stdlib") (Some Lib.Import)
|"-exclude-dir" ->
System.exclude_directory (next ()); oval
@@ 347,6 327,9 @@ let parse_args ~usage ~init arglist : t * string list =
|"-require-from"|"-rfrom" ->
let from = next () in add_vo_require oval (next ()) (Some from) None
+ |"-compat-from" ->
+ let from = next () in add_vo_require oval (next ()) ~allow_failure:true (Some from) (Some Lib.Import)
+
|"-require-import-from" | "-rifrom" ->
let from = next () in add_vo_require oval (next ()) (Some from) (Some Lib.Import)
@@ 468,7 451,7 @@ let parse_args ~usage ~init args =
(******************************************************************************)
(* prelude_data == From Coq Require Import Prelude. *)
-let prelude_data = RequireInjection { lib = "Prelude"; prefix = Some "Stdlib"; export = Some Lib.Import; }
+let prelude_data = RequireInjection { lib = "Prelude"; prefix = Some "Stdlib"; export = Some Lib.Import; allow_failure = false }
let injection_commands opts =
if opts.pre.load_init then prelude_data :: opts.pre.injections else opts.pre.injections
M sysinit/coqargs.mli => sysinit/coqargs.mli +1 -1
@@ 20,7 20,7 @@ type option_command =
| OptionUnset
| OptionAppend of string
-type require_injection = { lib: string; prefix: string option; export: Lib.export_flag option; }
+type require_injection = { lib: string; prefix: string option; export: Lib.export_flag option; allow_failure: bool }
(** Parameters follow [Library], that is to say, [lib,prefix,export]
means require library [lib] from optional [prefix] and import or
export if [export] is [Some Lib.Import]/[Some Lib.Export]. *)
M sysinit/coqinit.ml => sysinit/coqinit.ml +14 -3
@@ 182,11 182,22 @@ let init_runtime opts =
| Coqargs.Run ->
injection_commands opts
-let require_file ~intern ~prefix ~lib ~export =
+let warn_require_not_found =
+ CWarnings.create ~name:"compatibility-module-not-found"
+ ~category:CWarnings.CoreCategories.filesystem
+ Pp.(fun (prefix, lib) ->
+ strbrk "Did not find compatibility module " ++ Libnames.pr_qualid lib ++
+ pr_opt (fun prefix -> str "with prefix " ++ Libnames.pr_qualid prefix)
+ prefix ++ str ".")
+
+let require_file ~intern ~prefix ~lib ~export ~allow_failure =
let mp = Libnames.qualid_of_string lib in
let mfrom = Option.map Libnames.qualid_of_string prefix in
let exp = Option.map (fun e -> e, None) export in
- Flags.silently (Vernacentries.vernac_require ~intern mfrom exp) [mp,Vernacexpr.ImportAll]
+ try
+ Flags.silently (Vernacentries.vernac_require ~intern mfrom exp) [mp,Vernacexpr.ImportAll]
+ with (Synterp.UnmappedLibrary _ | Synterp.NotFoundLibrary _) when allow_failure ->
+ warn_require_not_found (mfrom, mp)
let warn_no_native_compiler =
CWarnings.create_in Nativeconv.w_native_disabled
@@ 201,7 212,7 @@ let warn_deprecated_native_compiler =
files ahead of time, use the coqnative binary instead.")
let handle_injection ~intern = let open Coqargs in function
- | RequireInjection {lib;prefix;export} -> require_file ~intern ~lib ~prefix ~export
+ | RequireInjection {lib;prefix;export;allow_failure} -> require_file ~intern ~lib ~prefix ~export ~allow_failure
| OptionInjection o -> set_option o
| WarnNoNative s -> warn_no_native_compiler s
| WarnNativeDeprecated -> warn_deprecated_native_compiler ()
M test-suite/dune => test-suite/dune +0 -5
@@ 21,11 21,6 @@
; when TIMED is set, used to print the timing table
../tools/make-one-time-file.py
../tools/TimeFileMaker.py
- ; Stuff for the compat script test
- ../dev/header.ml
- ../dev/tools/update-compat.py
- ../doc/stdlib/index-list.html.template
- ../sysinit/coqargs.ml
; For the changelog test
../config/coq_config.py
(source_tree doc/changelog)
A test-suite/output/compat_not_found.out => test-suite/output/compat_not_found.out +3 -0
@@ 0,0 1,3 @@
+While loading initial state:
+Warning: Did not find compatibility module tutu with prefix Tata.
+[compatibility-module-not-found,filesystem,default]
A test-suite/output/compat_not_found.v => test-suite/output/compat_not_found.v +5 -0
@@ 0,0 1,5 @@
+(* -*- coq-prog-args: ("-compat-from" "Tata" "tutu"); -*- *)
+(* From Tata Require tutu. would fail but -compat-from only issues a warning
+ and the file compiles fine. *)
+Goal True.
+Proof. exact I. Qed.
D test-suite/success/CompatCurrentFlag.v => test-suite/success/CompatCurrentFlag.v +0 -3
@@ 1,3 0,0 @@
-(* -*- coq-prog-args: ("-compat" "9.0") -*- *)
-(** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Stdlib.Compat.Coq90.
D test-suite/success/CompatOldFlag.v => test-suite/success/CompatOldFlag.v +0 -5
@@ 1,5 0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.19") -*- *)
-(** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
-Import Stdlib.Compat.Coq90.
-Import Stdlib.Compat.Coq820.
-Import Stdlib.Compat.Coq819.
D test-suite/success/CompatOldOldFlag.v => test-suite/success/CompatOldOldFlag.v +0 -6
@@ 1,6 0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.18") -*- *)
-(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
-Import Stdlib.Compat.Coq90.
-Import Stdlib.Compat.Coq820.
-Import Stdlib.Compat.Coq819.
-Import Stdlib.Compat.Coq818.
D test-suite/success/CompatPreviousFlag.v => test-suite/success/CompatPreviousFlag.v +0 -4
@@ 1,4 0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.20") -*- *)
-(** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
-Import Stdlib.Compat.Coq90.
-Import Stdlib.Compat.Coq820.
A test-suite/success/compat.v => test-suite/success/compat.v +7 -0
@@ 0,0 1,7 @@
+(* -*- coq-prog-args: ("-compat-from" "TestSuite" "admit"); -*- *)
+(* Check that TestSuite.admit was required *)
+Goal False.
+Proof. exact TestSuite.admit.proof_admitted. Qed.
+(* and also imported *)
+Goal False.
+Proof. exact proof_admitted. Qed.
D test-suite/tools/update-compat/run.sh => test-suite/tools/update-compat/run.sh +0 -9
@@ 1,9 0,0 @@
-#!/usr/bin/env bash
-
-# allow running this script from any directory by basing things on where the script lives
-SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"
-
-# we assume that the script lives in test-suite/tools/update-compat/,
-# and that update-compat.py lives in dev/tools/
-cd "${SCRIPT_DIR}/../../.."
-dev/tools/update-compat.py --assert-unchanged --master || exit $?
M theories/Compat/Coq818.v => theories/Compat/Coq818.v +2 -0
@@ 12,6 12,8 @@
Require Export Stdlib.Compat.Coq819.
+#[export] Set Warnings "-deprecated-since-8.19".
+
(* Restore broken behavior of [zify] reported in COQBUG(https://github.com/coq/coq/issues/17936) *)
From Stdlib Require Import Arith BinInt BinNat Znat Nnat PreOmega.
M theories/Compat/Coq819.v => theories/Compat/Coq819.v +2 -0
@@ 11,3 11,5 @@
(** Compatibility file for making Coq act similar to Coq v8.19 *)
Require Export Stdlib.Compat.Coq820.
+
+#[export] Set Warnings "-deprecated-since-8.20".
M theories/Compat/Coq820.v => theories/Compat/Coq820.v +1 -1
@@ 10,4 10,4 @@
(** Compatibility file for making Coq act similar to Coq v8.20 *)
-Require Export Stdlib.Compat.Coq90.
+#[export] Set Warnings "-deprecated-since-8.21".
D theories/Compat/Coq90.v => theories/Compat/Coq90.v +0 -11
@@ 1,11 0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * Copyright INRIA, CNRS and contributors *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** Compatibility file for making Coq act similar to Coq v9.0 *)
A theories/Compat/README.md => theories/Compat/README.md +9 -0
@@ 0,0 1,9 @@
+Files in this directory are intended to be loaded with the `-compat`
+command line option, in order to provide compatibility features to
+mimick some behaviors of older versions. For instance, this can
+disable warnings introduced in later versions.
+
+When adding a file in this directory, please name it `CoqXY.v` and
+prepend `From Stdlib Require Export CoqXY.` to the previous file.
+When removing the last remaining content of some file, please also
+remove the file altogether.