diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/profiling.txt | 6 | ||||
| -rw-r--r-- | dev/doc/versions-history.tex | 2 | ||||
| -rwxr-xr-x | dev/tools/update-compat.py | 38 |
3 files changed, 40 insertions, 6 deletions
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 29e87df6b8..8455d13377 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -10,7 +10,7 @@ In Coq source folder: opam switch 4.05.0+trunk+fp ./configure -local -debug make -perf record -g bin/coqtop -compile file.v +perf record -g bin/coqc file.v perf report -g fractal,callee --no-children To profile only part of a file, first load it using @@ -96,7 +96,7 @@ https://github.com/mshinwell/opam-repo-dev ### For memory dump: -CAMLRUNPARAM=T,mj bin/coqtop -compile file.v +CAMLRUNPARAM=T,mj bin/coqc file.v In another terminal: @@ -112,7 +112,7 @@ number of objects and third is the place where the objects where allocated. ### For complete memory graph: -CAMLRUNPARAM=T,gr bin/coqtop -compile file.v +CAMLRUNPARAM=T,gr bin/coqc file.v In another terminal: diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 8f9c3171da..1c4913d201 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -271,7 +271,7 @@ Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \ & & \feature{kernel-centric} architecture \\ & & more care for outside readers\\ & & (indentation, ocaml warning protection)\\ -Coq V7.0beta& released 27 December 2000 & \feature{${\cal L}_{\mathit{tac}}$} \\ +Coq V7.0beta& released 27 December 2000 & \feature{${\mathcal{L}}_{\mathit{tac}}$} \\ Coq V7.0beta2& released 2 February 2001\\ Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\ 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) |