From 2b47c0d1b492424c39477f9d4ec262e4d093be92 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 20 Nov 2015 20:17:35 +0100 Subject: Univs: fix type_of_global_in_context not returning instantiated universe contexts. --- library/global.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/global.ml b/library/global.ml index 6002382c1f..4cffd6b7e3 100644 --- a/library/global.ml +++ b/library/global.ml @@ -198,13 +198,13 @@ let type_of_global_in_context env r = | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = - if mib.mind_polymorphic then mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes else Univ.UContext.empty in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = - if mib.mind_polymorphic then mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes else Univ.UContext.empty in let inst = Univ.UContext.instance univs in -- cgit v1.2.3 From 8d93301045c45ec48c85ecae2dfb3609e5e4695f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 20 Nov 2015 20:18:11 +0100 Subject: Univs: generation of induction schemes should not generated useless instances for each of the inductive in the same block but reuse the original universe context shared by all of them. Also do not force schemes to become universe polymorphic. --- toplevel/indschemes.ml | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index f16e6e3f3f..00197bd668 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -128,7 +128,7 @@ let define id internal ctx c t = { const_entry_body = c; const_entry_secctx = None; const_entry_type = t; - const_entry_polymorphic = true; + const_entry_polymorphic = Flags.is_universe_polymorphism (); const_entry_universes = snd (Evd.universe_context ctx); const_entry_opaque = false; const_entry_inline_code = false; @@ -360,12 +360,21 @@ requested let do_mutual_induction_scheme lnamedepindsort = let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort and env0 = Global.env() in - let sigma, lrecspec = + let sigma, lrecspec, _ = List.fold_right - (fun (_,dep,ind,sort) (evd, l) -> - let evd, indu = Evd.fresh_inductive_instance env0 evd ind in - (evd, (indu,dep,interp_elimination_sort sort) :: l)) - lnamedepindsort (Evd.from_env env0,[]) + (fun (_,dep,ind,sort) (evd, l, inst) -> + let evd, indu, inst = + match inst with + | None -> + let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in + let ctxs = Univ.ContextSet.of_context ctx in + let evd = Evd.from_ctx (Evd.evar_universe_context_of ctxs) in + let u = Univ.UContext.instance ctx in + evd, (ind,u), Some u + | Some ui -> evd, (ind, ui), inst + in + (evd, (indu,dep,interp_elimination_sort sort) :: l, inst)) + lnamedepindsort (Evd.from_env env0,[],None) in let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = -- cgit v1.2.3 From e583a79b5a0298fd08f34305cc876d5117913e95 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 21 Nov 2015 00:23:12 +0100 Subject: Fixing kernel bug in typing match with let-ins in the arity. Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in 8.5beta2 and 8.5beta3 from a Coq file because typing done while compiling "match" would serve as a protection. However exploitable by calling the kernel directly, e.g. from a plugin (but a plugin can anyway do what it wants by bypassing kernel type abstraction). Fixing similar error in pretyping. --- kernel/reduction.ml | 2 +- pretyping/reductionops.ml | 2 +- test-suite/success/Case22.v | 24 ++++++++++++++++++++++++ 3 files changed, 26 insertions(+), 2 deletions(-) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 892557ac6c..939eeef5d5 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -136,7 +136,7 @@ let betazeta_appvect n c v = if Int.equal n 0 then applist (substl env t, stack) else match kind_of_term t, stack with Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack + | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | _ -> anomaly (Pp.str "Not enough lambda/let's") in stacklam n [] c (Array.to_list v) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 156c9a2772..bdd9ed81cf 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1651,7 +1651,7 @@ let betazetaevar_applist sigma n c l = if Int.equal n 0 then applist (substl env t, stack) else match kind_of_term t, stack with | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack + | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | Evar ev, _ -> (match safe_evar_value sigma ev with | Some body -> stacklam n env body stack diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v index ce9050d421..8c8f02eccf 100644 --- a/test-suite/success/Case22.v +++ b/test-suite/success/Case22.v @@ -17,3 +17,27 @@ Definition foo (x : I') : bool := match x with C' => true end. + +(* Bug found in november 2015: was wrongly failing in 8.5beta2 and 8.5beta3 *) + +Inductive I2 (A:Type) : let B:=A in forall C, let D:=(C*B)%type in Type := + E2 : I2 A nat. + +Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with + E2 _ => (0,0,(0,0)) + end. + +(* This used to succeed in 8.3, 8.4 and 8.5beta1 *) + +Inductive IND : forall X:Type, let Y:=X in Type := + C : IND True. + +Definition F (x:IND True) (A:Type) := + (* This failed in 8.5beta2 though it should have been accepted *) + match x in IND Y Z return Z with + C => I + end. + +Theorem paradox : False. + (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *) +Fail Proof (F C False). -- cgit v1.2.3 From af954522789043202d9c300a0bb37cbaf4958d60 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Nov 2015 17:17:49 +0100 Subject: Fixing a bug of adjust_subst_to_rel_context. --- pretyping/termops.ml | 2 +- test-suite/success/Case22.v | 18 +++++++++++++++--- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 5a55d47fd1..ebd9d939aa 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -930,7 +930,7 @@ let adjust_subst_to_rel_context sign l = match sign, l with | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args' | (_,Some c,_)::sign', args' -> - aux (substl (List.rev subst) c :: subst) sign' args' + aux (substl subst c :: subst) sign' args' | [], [] -> List.rev subst | _ -> anomaly (Pp.str "Instance and signature do not match") in aux [] (List.rev sign) l diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v index 8c8f02eccf..f88051f8f5 100644 --- a/test-suite/success/Case22.v +++ b/test-suite/success/Case22.v @@ -30,14 +30,26 @@ Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with (* This used to succeed in 8.3, 8.4 and 8.5beta1 *) Inductive IND : forall X:Type, let Y:=X in Type := - C : IND True. + CONSTR : IND True. Definition F (x:IND True) (A:Type) := (* This failed in 8.5beta2 though it should have been accepted *) - match x in IND Y Z return Z with - C => I + match x in IND X Y return Y with + CONSTR => Logic.I end. Theorem paradox : False. (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *) Fail Proof (F C False). + +(* Another bug found in November 2015 (a substitution was wrongly + reversed at pretyping level) *) + +Inductive Ind (A:Type) : + let X:=A in forall Y:Type, let Z:=(X*Y)%type in Type := + Constr : Ind A nat. + +Check fun x:Ind bool nat => + match x in Ind _ X Y Z return Z with + | Constr _ => (true,0) + end. -- cgit v1.2.3 From c4e2cf027b3fade4f9c2806e6061e1294a99e540 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Nov 2015 21:17:59 +0100 Subject: Fixing a vm_compute bug in the presence of let-ins among the parameters of an inductive type. --- pretyping/vnorm.ml | 9 +++++---- test-suite/success/Case22.v | 8 ++++++++ 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c4c85a62ed..be772a6677 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -59,11 +59,12 @@ let type_constructor mind mib u typ params = let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in - let nparams = Array.length params in - if Int.equal nparams 0 then ctyp + let ndecls = Context.rel_context_length mib.mind_params_ctxt in + if Int.equal ndecls 0 then ctyp else - let _,ctyp = decompose_prod_n nparams ctyp in - substl (Array.rev_to_list params) ctyp + let _,ctyp = decompose_prod_n_assum ndecls ctyp in + substl (List.rev (Termops.adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params))) + ctyp diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v index f88051f8f5..3c696502cd 100644 --- a/test-suite/success/Case22.v +++ b/test-suite/success/Case22.v @@ -53,3 +53,11 @@ Check fun x:Ind bool nat => match x in Ind _ X Y Z return Z with | Constr _ => (true,0) end. + +(* A vm_compute bug (the type of constructors was not supposed to + contain local definitions before proper parameters) *) + +Inductive Ind2 (b:=1) (c:nat) : Type := + Constr2 : Ind2 c. + +Eval vm_compute in Constr2 2. -- cgit v1.2.3 From 6b3112d3b6e401a4c177447dd3651820897f711f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 23 Nov 2015 08:14:27 +0100 Subject: Fix output of universe arcs. (Fix bug #4422) --- kernel/univ.ml | 4 ++-- toplevel/vernacentries.ml | 13 +++++-------- 2 files changed, 7 insertions(+), 10 deletions(-) diff --git a/kernel/univ.ml b/kernel/univ.ml index 6c2316988e..dc0a4b43c0 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -2030,8 +2030,8 @@ let dump_universes output g = let dump_arc u = function | Canonical {univ=u; lt=lt; le=le} -> let u_str = Level.to_string u in - List.iter (fun v -> output Lt (Level.to_string v) u_str) lt; - List.iter (fun v -> output Le (Level.to_string v) u_str) le + List.iter (fun v -> output Lt u_str (Level.to_string v)) lt; + List.iter (fun v -> output Le u_str (Level.to_string v)) le | Equiv v -> output Eq (Level.to_string u) (Level.to_string v) in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b6a1a53fa8..177c3fb0ab 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -355,11 +355,6 @@ let dump_universes_gen g s = close (); iraise reraise -let dump_universes sorted s = - let g = Global.universes () in - let g = if sorted then Univ.sort_universes g else g in - dump_universes_gen g s - (*********************) (* "Locate" commands *) @@ -1623,15 +1618,17 @@ let vernac_print = function | PrintCoercionPaths (cls,clt) -> msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) - | PrintUniverses (b, None) -> + | PrintUniverses (b, dst) -> let univ = Global.universes () in let univ = if b then Univ.sort_universes univ else univ in let pr_remaining = if Global.is_joined_environment () then mt () else str"There may remain asynchronous universe constraints" in - msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) - | PrintUniverses (b, Some s) -> dump_universes b s + begin match dst with + | None -> msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) + | Some s -> dump_universes_gen univ s + end | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s) -- cgit v1.2.3 From 3e4a4fbb1e0f00aff08664321d916167166dbab3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 23 Nov 2015 15:57:54 +0100 Subject: Fix generation of equality schemes on polymorphic equality types. --- tactics/eqschemes.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index b2603315d5..d08c7615a9 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -176,7 +176,7 @@ let build_sym_scheme env ind = name_context env ((Name varH,None,applied_ind)::realsign) in let ci = make_case_info (Global.env()) ind RegularStyle in let c = - (my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign_ind (mkCase (ci, my_it_mkLambda_or_LetIn_name @@ -395,7 +395,7 @@ let build_l2r_rew_scheme dep env ind kind = applied_sym_C 3, [|mkVar varHC|]) in let c = - (my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign (mkNamedLambda varP (my_it_mkProd_or_LetIn (if dep then realsign_ind_P else realsign_P) s) @@ -485,7 +485,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = mkApp (mkVar varP,Array.append (rel_vect 3 nrealargs) (if dep then [|cstr (3*nrealargs+4) 3|] else [||])) in let c = - (my_it_mkLambda_or_LetIn mib.mind_params_ctxt + (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign (mkNamedLambda varH applied_ind (mkCase (ci, @@ -782,5 +782,6 @@ let build_congr env (eq,refl,ctx) ind = let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> - (* May fail if equality is not defined *) - build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants) + (* May fail if equality is not defined *) + build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, + Safe_typing.empty_private_constants) -- cgit v1.2.3 From 1467c22548453cd07ceba0029e37c8bbdfd039ea Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 23 Nov 2015 17:51:16 +0100 Subject: Fixing an old typo in Retyping, found by Matej. --- pretyping/retyping.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index fb55265526..a169a4577e 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -158,8 +158,7 @@ let retype ?(polyprop=true) sigma = and sort_family_of env t = match kind_of_term t with | Cast (c,_, s) when isSort s -> family_of_sort (destSort s) - | Sort (Prop c) -> InType - | Sort (Type u) -> InType + | Sort s -> family_of_sort s | Prod (name,t,c2) -> let s2 = sort_family_of (push_rel (name,None,t) env) c2 in if not (is_impredicative_set env) && -- cgit v1.2.3 From 2d32a2c5606286c85fd35c7ace167b4d4e108ced Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 24 Nov 2015 15:48:28 +0100 Subject: Univs: carry on universe substitution when defining obligations of non-polymorphic definitions, original universes might be substituted later on due to constraints. --- toplevel/obligations.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 311c61f894..e091d825cd 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -823,7 +823,9 @@ let obligation_hook prg obl num auto ctx' _ gr = if not (pi2 prg.prg_kind) (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) - Evd.evar_universe_context (Evd.from_env (Global.env ())) + let evd = Evd.from_env (Global.env ()) in + let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in + Evd.evar_universe_context ctx' else ctx' in let prg = { prg with prg_ctx = ctx' } in @@ -899,8 +901,10 @@ and solve_obligation_by_tac prg obls i tac = let def, obl' = declare_obligation !prg obl t ty uctx in obls.(i) <- obl'; if def && not (pi2 !prg.prg_kind) then ( - (* Declare the term constraints with the first obligation only *) - let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in + (* Declare the term constraints with the first obligation only *) + let evd = Evd.from_env (Global.env ()) in + let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in + let ctx' = Evd.evar_universe_context evd in prg := {!prg with prg_ctx = ctx'}); true else false -- cgit v1.2.3 From 901a9b29adf507370732aeafbfea6718c1842f1b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 25 Nov 2015 12:09:27 +0100 Subject: Checking lablgtk version in configure. Fix bug #4423. --- configure.ml | 41 ++++++++++++++++++++++++++++++++--------- 1 file changed, 32 insertions(+), 9 deletions(-) diff --git a/configure.ml b/configure.ml index 51033c3d01..500796f5d1 100644 --- a/configure.ml +++ b/configure.ml @@ -719,10 +719,18 @@ let operating_system, osdeplibs = (** * lablgtk2 and CoqIDE *) +type source = Manual | OCamlFind | Stdlib + +let get_source = function +| Manual -> "manually provided" +| OCamlFind -> "via ocamlfind" +| Stdlib -> "in OCaml library" + (** Is some location a suitable LablGtk2 installation ? *) -let check_lablgtkdir ?(fatal=false) msg dir = +let check_lablgtkdir ?(fatal=false) src dir = let yell msg = if fatal then die msg else (printf "%s\n" msg; false) in + let msg = get_source src in if not (dir_exists dir) then yell (sprintf "No such directory '%s' (%s)." dir msg) else if not (Sys.file_exists (dir/"gSourceView2.cmi")) then @@ -736,11 +744,11 @@ let check_lablgtkdir ?(fatal=false) msg dir = let get_lablgtkdir () = match !Prefs.lablgtkdir with | Some dir -> - let msg = "manually provided" in + let msg = Manual in if check_lablgtkdir ~fatal:true msg dir then dir, msg - else "", "" + else "", msg | None -> - let msg = "via ocamlfind" in + let msg = OCamlFind in let d1,_ = tryrun "ocamlfind" ["query";"lablgtk2.sourceview2"] in if d1 <> "" && check_lablgtkdir msg d1 then d1, msg else @@ -748,10 +756,25 @@ let get_lablgtkdir () = let d2,_ = tryrun "ocamlfind" ["query";"lablgtk2"] in if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg else - let msg = "in OCaml library" in + let msg = Stdlib in let d3 = camllib^"/lablgtk2" in if check_lablgtkdir msg d3 then d3, msg - else "", "" + else "", msg + +(** Detect and/or verify the Lablgtk2 version *) + +let check_lablgtk_version src dir = match src with +| Manual | Stdlib -> + let test = sprintf "grep -q -w convert_with_fallback %S/glib.mli" dir in + let ans = Sys.command test = 0 in + printf "Warning: could not check the version of lablgtk2.\n"; + (ans, "an unknown version") +| OCamlFind -> + let v, _ = tryrun "ocamlfind" ["query"; "-format"; "%v"; "lablgtk2"] in + try + let vi = List.map s2i (numeric_prefix_list v) in + ([2; 16] <= vi, v) + with _ -> (false, v) let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native" @@ -775,9 +798,9 @@ let check_coqide () = if !Prefs.coqide = Some No then set_ide No "CoqIde manually disabled"; let dir, via = get_lablgtkdir () in if dir = "" then set_ide No "LablGtk2 not found"; - let found = sprintf "LablGtk2 found (%s)" via in - let test = sprintf "grep -q -w convert_with_fallback %S/glib.mli" dir in - if Sys.command test <> 0 then set_ide No (found^" but too old"); + let found = sprintf "LablGtk2 found (%s)" (get_source via) in + let (ok, version) = check_lablgtk_version via dir in + if not ok then set_ide No (found^", but too old (required >= 2.16, found " ^ version ^ ")"); (* We're now sure to produce at least one kind of coqide *) lablgtkdir := shorten_camllib dir; if !Prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested"); -- cgit v1.2.3 From 6f9cc3aca5bb0e5684268a7283796a9272ed5f9d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 25 Nov 2015 15:58:03 +0100 Subject: Advertising that CoqIDE requires lablgtk >= 2.16 --- INSTALL.ide | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/INSTALL.ide b/INSTALL.ide index 6e41b2d051..b651e77db4 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -39,7 +39,7 @@ COMPILATION REQUIREMENTS install GTK+ 2.x, should you need to force it for one reason or another.) - The OCaml bindings for GTK+ 2.x, lablgtk2 with support for gtksourceview2. - You need at least version 2.14.2. + You need at least version 2.16. Your distribution may contain precompiled packages. For example, for Debian, run -- cgit v1.2.3 From e92aeed3abcf7d42045deb9fb3a450d3527eadc9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Nov 2015 17:33:24 +0100 Subject: Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej). This was not a typo (was correctly taking the family type of the type). --- pretyping/retyping.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a169a4577e..fb55265526 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -158,7 +158,8 @@ let retype ?(polyprop=true) sigma = and sort_family_of env t = match kind_of_term t with | Cast (c,_, s) when isSort s -> family_of_sort (destSort s) - | Sort s -> family_of_sort s + | Sort (Prop c) -> InType + | Sort (Type u) -> InType | Prod (name,t,c2) -> let s2 = sort_family_of (push_rel (name,None,t) env) c2 in if not (is_impredicative_set env) && -- cgit v1.2.3 From ef8718a7fd3bcd960d954093d8c636525e6cc492 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 25 Nov 2015 17:56:41 +0100 Subject: Heuristic to check the version of lablgtk2 in configure.ml. When not using ocamlfind, we use a grep-based heuristic to check that lablgtk2 is recent enough. This is an extension of an already-used heuristic. --- configure.ml | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/configure.ml b/configure.ml index 500796f5d1..3a55fb5707 100644 --- a/configure.ml +++ b/configure.ml @@ -765,9 +765,18 @@ let get_lablgtkdir () = let check_lablgtk_version src dir = match src with | Manual | Stdlib -> - let test = sprintf "grep -q -w convert_with_fallback %S/glib.mli" dir in - let ans = Sys.command test = 0 in - printf "Warning: could not check the version of lablgtk2.\n"; + let test accu f = + if accu then + let test = sprintf "grep -q -w %s %S/glib.mli" f dir in + Sys.command test = 0 + else false + in + let heuristics = [ + "convert_with_fallback"; + "wrap_poll_func"; (** Introduced in lablgtk 2.16 *) + ] in + let ans = List.fold_left test true heuristics in + if ans then printf "Warning: could not check the version of lablgtk2.\n"; (ans, "an unknown version") | OCamlFind -> let v, _ = tryrun "ocamlfind" ["query"; "-format"; "%v"; "lablgtk2"] in @@ -798,8 +807,8 @@ let check_coqide () = if !Prefs.coqide = Some No then set_ide No "CoqIde manually disabled"; let dir, via = get_lablgtkdir () in if dir = "" then set_ide No "LablGtk2 not found"; - let found = sprintf "LablGtk2 found (%s)" (get_source via) in let (ok, version) = check_lablgtk_version via dir in + let found = sprintf "LablGtk2 found (%s, %s)" (get_source via) version in if not ok then set_ide No (found^", but too old (required >= 2.16, found " ^ version ^ ")"); (* We're now sure to produce at least one kind of coqide *) lablgtkdir := shorten_camllib dir; -- cgit v1.2.3 From 3940441dffdfc3a8f968760c249f6a2e8a1e0912 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 22 Sep 2015 09:05:44 +0200 Subject: Generalizing the patch to bug #2554 on fixing path looking with correct case on MacOS X whose file system is case-insensitive but case-preserving (HFS+ configured in case-insensitive mode). Generalized it to any case-preserving case-insensitive file system, which makes it applicable to Windows with NTFS used in case-insensitive mode but also to Linux when mounting a case-insensitive file system. Removed the blow-up of the patch, improved the core of the patch by checking whether the case is correct only for the suffix part of the file to be found (not for the part which corresponds to the path in which where to look), and finally used a cache so that the effect of the patch is not observable. Note that the cache is implemented in a way not synchronous with backtracking what implies e.g. that a file compiled in the middle of an interactive session would not be found until Coq is restarted, even by backtracking before the corresponding Require. For history see commits b712864e9cf499f1298c1aca1ad8a8b17e145079, 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606 69941d4e195650bf59285b897c14d6287defea0f e7043eec55085f4101bfb126d8829de6f6086c5a. as well as https://coq.inria.fr/bugs/show_bug.cgi?id=2554 discussion on coq-club "8.5 and MathClasses" (May 2015) discussion on coqdev "Coq awfully slow on MacOS X" (Sep 2015) --- lib/envars.ml | 5 ++++- lib/system.ml | 50 +++++++++++++++++++++++++++++++++++++++++++++++++- lib/system.mli | 2 ++ 3 files changed, 55 insertions(+), 2 deletions(-) diff --git a/lib/envars.ml b/lib/envars.ml index b0eed8386b..2b8af917fa 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -39,6 +39,8 @@ let path_to_list p = let user_path () = path_to_list (Sys.getenv "PATH") (* may raise Not_found *) +(* Finding a name in path using the equality provided by the file system *) +(* whether it is case-sensitive or case-insensitive *) let rec which l f = match l with | [] -> @@ -99,7 +101,8 @@ let _ = (** [check_file_else ~dir ~file oth] checks if [file] exists in the installation directory [dir] given relatively to [coqroot]. If this Coq is only locally built, then [file] must be in [coqroot]. - If the check fails, then [oth ()] is evaluated. *) + If the check fails, then [oth ()] is evaluated. + Using file system equality seems well enough for this heuristic *) let check_file_else ~dir ~file oth = let path = if Coq_config.local then coqroot else coqroot / dir in if Sys.file_exists (path / file) then path else oth () diff --git a/lib/system.ml b/lib/system.ml index ddc56956c5..02d5e963ff 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -53,6 +53,49 @@ let all_subdirs ~unix_path:root = if exists_dir root then traverse root []; List.rev !l +(* Caching directory contents for efficient syntactic equality of file + names even on case-preserving but case-insensitive file systems *) + +module StrMod = struct + type t = string + let compare = compare +end + +module StrMap = Map.Make(StrMod) +module StrSet = Set.Make(StrMod) + +let dirmap = ref StrMap.empty + +let make_dir_table dir = + let b = ref StrSet.empty in + let a = Unix.opendir dir in + (try + while true do + let s = Unix.readdir a in + if s.[0] != '.' then b := StrSet.add s !b + done + with + | End_of_file -> ()); + Unix.closedir a; !b + +let exists_in_dir_respecting_case dir bf = + let contents = + try StrMap.find dir !dirmap with Not_found -> + let contents = make_dir_table dir in + dirmap := StrMap.add dir contents !dirmap; + contents in + StrSet.mem bf contents + +let file_exists_respecting_case path f = + (* This function ensures that a file with expected lowercase/uppercase + is the correct one, even on case-insensitive file systems *) + let rec aux f = + let bf = Filename.basename f in + let df = Filename.dirname f in + (String.equal df "." || aux df) + && exists_in_dir_respecting_case (Filename.concat path df) bf + in Sys.file_exists (Filename.concat path f) && aux f + let rec search paths test = match paths with | [] -> [] @@ -77,7 +120,7 @@ let where_in_path ?(warn=true) path filename = in check_and_warn (search path (fun lpe -> let f = Filename.concat lpe filename in - if Sys.file_exists f then [lpe,f] else [])) + if file_exists_respecting_case lpe filename then [lpe,f] else [])) let where_in_path_rex path rex = search path (fun lpe -> @@ -93,6 +136,8 @@ let where_in_path_rex path rex = let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then + (* the name is considered to be a physical name and we use the file + system rules (e.g. possible case-insensitivity) to find it *) if Sys.file_exists filename then let root = Filename.dirname filename in root, filename @@ -100,6 +145,9 @@ let find_file_in_path ?(warn=true) paths filename = errorlabstrm "System.find_file_in_path" (hov 0 (str "Can't find file" ++ spc () ++ str filename)) else + (* the name is considered to be the transcription as a relative + physical name of a logical name, so we deal with it as a name + to be locate respecting case *) try where_in_path ~warn paths filename with Not_found -> errorlabstrm "System.find_file_in_path" diff --git a/lib/system.mli b/lib/system.mli index 247d528b97..c2d64fe0d0 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -29,6 +29,8 @@ val exists_dir : string -> bool val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string +val file_exists_respecting_case : string -> string -> bool + (** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] -- cgit v1.2.3 From b1a5fe3686ecd5b03e5c7c2efd95716a8e5270ea Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 4 Nov 2015 22:22:17 +0100 Subject: Fix for case-insensitive path looking continued (#2554): Adding a second chance to dynamically regenerate the file system cache when a file is not found (suggested by Guillaume M.). --- lib/system.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/lib/system.ml b/lib/system.ml index 02d5e963ff..2e35a98f7f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -79,12 +79,20 @@ let make_dir_table dir = Unix.closedir a; !b let exists_in_dir_respecting_case dir bf = - let contents = - try StrMap.find dir !dirmap with Not_found -> + let contents, cached = + try StrMap.find dir !dirmap, true with Not_found -> let contents = make_dir_table dir in dirmap := StrMap.add dir contents !dirmap; - contents in - StrSet.mem bf contents + contents, false in + StrSet.mem bf contents || + if cached then begin + (* rescan, there is a new file we don't know about *) + let contents = make_dir_table dir in + dirmap := StrMap.add dir contents !dirmap; + StrSet.mem bf contents + end + else + false let file_exists_respecting_case path f = (* This function ensures that a file with expected lowercase/uppercase -- cgit v1.2.3