diff options
| -rwxr-xr-x | dev/tools/update-compat.py | 62 | ||||
| -rw-r--r-- | doc/changelog/03-notations/11090-master+refactoring-application-printing.rst | 1 | ||||
| -rw-r--r-- | doc/plugin_tutorial/README.md | 14 | ||||
| -rw-r--r-- | interp/constrextern.ml | 34 | ||||
| -rw-r--r-- | plugins/ssr/ssrbool.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_11161.v | 10 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 14 |
8 files changed, 97 insertions, 42 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 diff --git a/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst new file mode 100644 index 0000000000..5c3936073a --- /dev/null +++ b/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst @@ -0,0 +1 @@ +- Fixed #11033: regression in not printing coercions to which is also associated a notation (`#11090 <https://github.com/coq/coq/pull/11090>`_, by Hugo Herbelin). diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md index 6d142a9af8..e0cedb0487 100644 --- a/doc/plugin_tutorial/README.md +++ b/doc/plugin_tutorial/README.md @@ -3,13 +3,21 @@ How to write plugins in Coq # Working environment In addition to installing OCaml and Coq, it can help to install several tools for development. - - ## Merlin + + ## Tuareg and Merlin These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) ```shell opam install merlin # prints instructions for vim and emacs +opam install tuareg # syntax highlighting for OCaml +opam user-setup install # automatically configures editors for merlin +``` + + Adding this line to your .emacs helps Tuareg recognize the .mlg extension: + +```shell +(add-to-list 'auto-mode-alist '("\\.mlg$" . tuareg-mode) t) ``` ## This tutorial @@ -23,7 +31,7 @@ make # build # tuto0 : basics of project organization - package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` + package an mlg file in a plugin, organize a `Makefile`, `_CoqProject` - Example of syntax to add a new toplevel command - Example of function call to print a simple message - Example of function call to print a simple warning diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0c247e2660..c85f4f2cf7 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -721,15 +721,27 @@ let extern_possible_prim_token (custom,scopes) r = | None -> raise No_match | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) -let extern_possible extern r = - try Some (extern r) with No_match -> None - -let extern_optimal extern r r' = - let c = extern_possible extern r in - let c' = if r==r' then None else extern_possible extern r' in - match c,c' with - | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n - | _ -> raise No_match +let filter_fully_applied r l = + let nargs = match DAst.get r with + | GApp (f,args) -> List.length args + | _ -> assert false in + List.filter (fun (keyrule,pat,n as _rule) -> n = Some nargs) l + +let extern_optimal extern extern_fully_applied r r' = + if r==r' then + (* No coercion: we look for a notation for r or a partial application of it *) + extern r + else + (* A coercion is removed: we prefer in order: + - a notation w/o a delimiter for the expression w/o coercions (or a partial application of it), if any + - a notation for the fully-applied expression with coercions, if any + - a notation with a delimiter for the expression w/o coercions (or a partial applied of it), if any *) + try + let c' = extern r' in + match c' with + | { CAst.v = CDelimiters _} -> (try extern_fully_applied r with No_match -> c') + | _ -> c' + with No_match -> extern_fully_applied r (* Helper function for safe and optimal printing of primitive tokens *) (* such as those for Int63 *) @@ -798,13 +810,15 @@ let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal (extern_possible_prim_token scopes) r r' + let extern_fun = extern_possible_prim_token scopes in + extern_optimal extern_fun extern_fun r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_optimal (fun r -> extern_notation scopes vars r (uninterp_notations r)) + (fun r -> extern_notation scopes vars r (filter_fully_applied r (uninterp_notations r))) r r'' with No_match -> let loc = r'.CAst.loc in diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 376410658a..f6b192c226 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -290,7 +290,7 @@ Require Import ssreflect ssrfun. r -- a right-hand operation, as orb_andr : rightt_distributive orb andb. T or t -- boolean truth, as in andbT: right_id true andb. U -- predicate union, as in predU. - W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P. **) + W -- weakening, as in in1W : (forall x, P) -> {in D, forall x, P}. **) Set Implicit Arguments. diff --git a/test-suite/bugs/closed/bug_11161.v b/test-suite/bugs/closed/bug_11161.v new file mode 100644 index 0000000000..22a075e096 --- /dev/null +++ b/test-suite/bugs/closed/bug_11161.v @@ -0,0 +1,10 @@ +(* Ensure that evars are properly normalized in the instance path. + Problems with this can cause eg #11161. *) + +Class Foo (n:nat) := {x : bool}. + +Instance bar n : Foo n. Admitted. + +Instance bar' n : Foo n. split. abstract exact true. Qed. + +Instance bar'' n : Foo n. split. abstract exact true. Defined. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index ba4ac5a8f9..32120a9674 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -59,3 +59,5 @@ where |- Type] (pat, p0, p cannot be used) fun '{| |} => true : R -> bool +b = a + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4b9d0abd95..d3433949d1 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -140,3 +140,17 @@ Record R := { n : nat }. Check fun '{|n:=x|} => true. End EmptyRecordSyntax. + +Module L. + +(* Testing regression #11053 *) + +Section Test. +Variables (A B : Type) (a : A) (b : B). +Variable c : A -> B. +Coercion c : A >-> B. +Notation COERCION := (c). +Check b = a. +End Test. + +End L. |