From c5de2c3a2aa96c468e7583577141a93e359a9baf Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 May 2016 00:48:25 +0200 Subject: Fix bug #4722: Coq dies when encountering broken symbolic links. --- lib/system.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/system.ml b/lib/system.ml index 205a5506cb..b4b3882d33 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -35,7 +35,7 @@ let all_subdirs ~unix_path:root = Array.iter (fun f -> if ok_dirname f then let file = Filename.concat dir f in - if Sys.is_directory file then begin + if exists_dir file then begin let newrel = rel @ [f] in add file newrel; traverse file newrel -- cgit v1.2.3 From 123504209e35b98ac14956ec6950cb7cd8b0089b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 May 2016 18:10:34 +0200 Subject: Small optimization in evar resolution. Instead of rebuilding a whole set of evars just to make a typeclass filter, we use the source evarmap. --- pretyping/pretyping.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b33084a423..d6f8f0de5f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -184,8 +184,7 @@ type inference_flags = { } let frozen_holes (sigma, sigma') = - let fold evk _ accu = Evar.Set.add evk accu in - Evd.fold_undefined fold sigma Evar.Set.empty + (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma) let pending_holes (sigma, sigma') = let fold evk _ accu = @@ -194,7 +193,7 @@ let pending_holes (sigma, sigma') = Evd.fold_undefined fold sigma' Evar.Set.empty let apply_typeclasses env evdref frozen fail_evar = - let filter_frozen evk = Evar.Set.mem evk frozen in + let filter_frozen = frozen in evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk)) -- cgit v1.2.3 From 1c26b08983f903538992eb1b5605c6ebe29fd175 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 28 Apr 2016 21:17:23 +0200 Subject: More hints on how to fix compatibility issues. --- COMPATIBILITY | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/COMPATIBILITY b/COMPATIBILITY index eaeb2cba24..55b2d003f7 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -3,6 +3,43 @@ Potential sources of incompatibilities between Coq V8.4 and V8.5 (see also file CHANGES) +* List of typical changes to be done to adapt files from Coq 8.4 * +* to Coq 8.5 when not using compatibility option "-compat 8.4". * + +Symptom: "The reference omega was not found in the current environment". +Cause: "Require Omega" does not import the tactic "omega" any more +Possible solutions: +- use "Require Import OmegaTactic" (not compatible with 8.4) +- use "Require Import Omega" (compatible with 8.4) +- add definition "Ltac omega := Coq.omega.Omega.omega." + +Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective) +Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives +Possible solutions: +- use "dintuition" instead; it is stronger than "intuition" and works + uniformly on non standard connectives, such as n-ary conjunctions or disjunctions + (not compatible with 8.4) +- do the script differently + +Symptom: The constructor foo (in type bar) expects n arguments. +Cause: parameters must now be given in patterns +Possible solutions: +- use option "Set Asymmetric Patterns" (compatible with 8.4) +- add "_" for the parameters (not compatible with 8.4) +- turn the parameters into implicit arguments (compatible with 8.4) + +Symptom: "NPeano.Nat.foo" not existing anymore +Possible solutions: +- use "Nat.foo" instead + +Symptom: typing problems with proj1_sig or similar +Cause: coercion from sig to sigT and similar coercions have been + removed so as to make the initial state easier to understand for + beginners +Solution: change proj1_sig into projT1 and similarly (compatible with 8.4) + +* Other detailed changes * + Universe Polymorphism. - Refinement, unification and tactics are now aware of universes, -- cgit v1.2.3 From cdaf25c41414510f9ebc0eeea174ed3f3ce0b91b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 14 May 2016 20:16:53 +0200 Subject: Removing unexcepted activation of option "Regular Subst Tactic", since there is actually no change in default subst between 8.4 and 8.5. --- theories/Compat/Coq84.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index e46a556a98..aa4411704d 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -56,8 +56,6 @@ Tactic Notation "symmetry" := symmetry. Tactic Notation "split" := split. Tactic Notation "esplit" := esplit. -Global Set Regular Subst Tactic. - (** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *) Require Coq.Numbers.Natural.Peano.NPeano. -- cgit v1.2.3 From 9b2beca375e1b3fd8f1298ee13656124fe24e807 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 17:45:04 +0200 Subject: Fix bug #4737: cycle tactic doesn't like zero goals. --- proofs/proofview.ml | 11 ++++++----- test-suite/bugs/closed/4737.v | 9 +++++++++ 2 files changed, 15 insertions(+), 5 deletions(-) create mode 100644 test-suite/bugs/closed/4737.v diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6d7dcb9257..57ff777080 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -660,11 +660,12 @@ let with_shelf tac = (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) let goodmod p m = - let p' = p mod m in - (* if [n] is negative [n mod l] is negative of absolute value less - than [l], so [(n mod l)+l] is the representative of [n] in the - interval [[0,l-1]].*) - if p' < 0 then p'+m else p' + if m = 0 then 0 else + let p' = p mod m in + (* if [n] is negative [n mod l] is negative of absolute value less + than [l], so [(n mod l)+l] is the representative of [n] in the + interval [[0,l-1]].*) + if p' < 0 then p'+m else p' let cycle n = let open Proof in diff --git a/test-suite/bugs/closed/4737.v b/test-suite/bugs/closed/4737.v new file mode 100644 index 0000000000..84ed45e454 --- /dev/null +++ b/test-suite/bugs/closed/4737.v @@ -0,0 +1,9 @@ +Goal True. +Proof. +exact I; cycle 1. +Qed. + +Goal True. +Proof. +exact I; swap 1 2. +Qed. -- cgit v1.2.3 From d2f9a457d0bb2fd11ac7d5f6587174a79ca9c4b6 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 19 May 2016 15:18:26 +0200 Subject: Unicode.ascii_of_ident is now truly injective A non-ASCII char is now converted to _UUxxxx_ with xxxx being its unicode index in hexa. And any preexisting _UU substring in the ident is converted to _UUU. The switch from __Uxxxx_ to _UUxxxx_ is cosmetic, it just helps the extraction (less __ in names). But the other part of the patch (detection of preexisting _UU substrings) is critical to make ascii_of_ident truly injective and avoid the following kind of proof of False via native_compute : Definition α := 1. Definition __U03b1_ := 2. Lemma oups : False. Proof. assert (α = __U03b1_). { native_compute. reflexivity. } discriminate. Qed. Conflicts: lib/unicode.mli --- lib/unicode.ml | 30 ++++++++++++++++++++---------- lib/unicode.mli | 9 ++++++++- 2 files changed, 28 insertions(+), 11 deletions(-) diff --git a/lib/unicode.ml b/lib/unicode.ml index cfaa73cc11..0dc4238ee4 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -235,14 +235,24 @@ let is_basic_ascii s = !ok let ascii_of_ident s = - if is_basic_ascii s then s else - let i = ref 0 and out = ref "" in - begin try while true do + let len = String.length s in + let has_UU i = + i+2 < len && s.[i]='_' && s.[i+1]='U' && s.[i+2]='U' + in + let i = ref 0 in + while !i < len && Char.code s.[!i] < 128 && not (has_UU !i) do + incr i + done; + if !i = len then s else + let out = Buffer.create (2*len) in + Buffer.add_substring out s 0 !i; + while !i < len do let j, n = next_utf8 s !i in - out := - if n >= 128 - then Printf.sprintf "%s__U%04x_" !out n - else Printf.sprintf "%s%c" !out s.[!i]; - i := !i + j - done with End_of_input -> () end; - !out + if n >= 128 then + (Printf.bprintf out "_UU%04x_" n; i := !i + j) + else if has_UU !i then + (Buffer.add_string out "_UUU"; i := !i + 3) + else + (Buffer.add_char out s.[!i]; incr i) + done; + Buffer.contents out diff --git a/lib/unicode.mli b/lib/unicode.mli index 65e75a20d6..00211164fb 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -23,8 +23,15 @@ val ident_refutation : string -> (bool * string) option (** First char of a string, converted to lowercase *) val lowercase_first_char : string -> string -(** For extraction, turn a unicode string into an ascii-only one *) +(** Return [true] if all UTF-8 characters in the input string are just plain + ASCII characters. Returns [false] otherwise. *) val is_basic_ascii : string -> bool + +(** [ascii_of_ident s] maps UTF-8 string to a string composed solely from ASCII + characters. The non-ASCII characters are translated to ["_UUxxxx_"] where + {i xxxx} is the Unicode index of the character in hexadecimal (from four + to six hex digits). To avoid potential name clashes, any preexisting + substring ["_UU"] is turned into ["_UUU"]. *) val ascii_of_ident : string -> string (** Validate an UTF-8 string *) -- cgit v1.2.3 From 027c42c467da891803936155097879896dcd7ec7 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 19 May 2016 19:44:54 +0200 Subject: adding "user-contrib" directory to ".gitignore" --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 6d843661ff..3f9856916a 100644 --- a/.gitignore +++ b/.gitignore @@ -168,3 +168,4 @@ dev/myinclude /doc/refman/Reference-Manual.hoptind /doc/refman/Reference-Manual.optidx /doc/refman/Reference-Manual.optind +user-contrib -- cgit v1.2.3 From 830934afe66f1e6e9314a77a350c3df6c20e4584 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 19 May 2016 20:18:03 +0200 Subject: Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore) --- plugins/extraction/common.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index bb9e8e5f5b..f2e7c3ede1 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -17,8 +17,8 @@ open Table open Miniml open Mlutil -let string_of_id id = - let s = Names.Id.to_string id in +let ascii_of_id id = + let s = Id.to_string id in for i = 0 to String.length s - 2 do if s.[i] == '_' && s.[i+1] == '_' then warning_id s done; @@ -109,9 +109,9 @@ let pseudo_qualify = qualify "__" let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false -let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id)) +let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id)) let uppercase_id id = - let s = string_of_id id in + let s = ascii_of_id id in assert (not (String.is_empty s)); if s.[0] == '_' then Id.of_string ("Coq_"^s) else Id.of_string (String.capitalize s) @@ -331,7 +331,7 @@ let reset_renaming_tables flag = existing. *) let modular_rename k id = - let s = string_of_id id in + let s = ascii_of_id id in let prefix,is_ok = if upperkind k then "Coq_",is_upper else "coq_",is_lower in @@ -353,9 +353,9 @@ let modfstlev_rename = let coqset = get_prefixes id in let nextcoq = next_ident_away coqid coqset in add_prefixes id (nextcoq::coqset); - (string_of_id nextcoq)^"_"^(string_of_id id) + (Id.to_string nextcoq)^"_"^(ascii_of_id id) with Not_found -> - let s = string_of_id id in + let s = ascii_of_id id in if is_lower s || begins_with_CoqXX s then (add_prefixes id [coqid]; "Coq_"^s) else @@ -404,7 +404,7 @@ let ref_renaming_fun (k,r) = | [""] -> (* this happens only at toplevel of the monolithic case *) let globs = Id.Set.elements (get_global_ids ()) in let id = next_ident_away (kindcase_id k idg) globs in - string_of_id id + Id.to_string id | _ -> modular_rename k idg in add_global_ids (Id.of_string s); -- cgit v1.2.3 From 088b3161c93e46ec2d865fe71a206cee15acd30c Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 19 May 2016 20:37:23 +0200 Subject: native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore) --- kernel/nativecode.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 9d181b4763..2159a702c3 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1487,8 +1487,8 @@ let optimize_stk stk = (** Printing to ocaml **) (* Redefine a bunch of functions in module Names to generate names acceptable to OCaml. *) -let string_of_id s = Unicode.ascii_of_ident (string_of_id s) -let string_of_label l = Unicode.ascii_of_ident (string_of_label l) +let string_of_id s = Unicode.ascii_of_ident (Id.to_string s) +let string_of_label l = string_of_id (Label.to_id l) let string_of_dirpath = function | [] -> "_" @@ -1561,8 +1561,7 @@ let pp_gname fmt g = Format.fprintf fmt "%s" (string_of_gname g) let pp_lname fmt ln = - let s = Unicode.ascii_of_ident (string_of_name ln.lname) in - Format.fprintf fmt "x_%s_%i" s ln.luid + Format.fprintf fmt "x_%s_%i" (string_of_name ln.lname) ln.luid let pp_ldecls fmt ids = let len = Array.length ids in -- cgit v1.2.3