aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--INSTALL.ide2
-rw-r--r--configure.ml50
-rw-r--r--engine/termops.ml2
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/uGraph.ml4
-rw-r--r--lib/envars.ml5
-rw-r--r--lib/system.ml58
-rw-r--r--lib/system.mli2
-rw-r--r--library/global.ml4
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/vnorm.ml9
-rw-r--r--tactics/eqschemes.ml11
-rw-r--r--test-suite/success/Case22.v44
-rw-r--r--toplevel/indschemes.ml21
-rw-r--r--toplevel/obligations.ml10
-rw-r--r--toplevel/vernacentries.ml13
16 files changed, 194 insertions, 45 deletions
diff --git a/INSTALL.ide b/INSTALL.ide
index 6e41b2d05..b651e77db 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
diff --git a/configure.ml b/configure.ml
index 47721f778..b8bb650b1 100644
--- a/configure.ml
+++ b/configure.ml
@@ -670,10 +670,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
@@ -687,11 +695,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
@@ -699,10 +707,34 @@ 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 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
+ 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"
@@ -726,9 +758,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 (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;
if !Prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested");
diff --git a/engine/termops.ml b/engine/termops.ml
index 5a55d47fd..ebd9d939a 100644
--- a/engine/termops.ml
+++ b/engine/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/kernel/reduction.ml b/kernel/reduction.ml
index c5595bbc3..110555011 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -134,7 +134,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/kernel/uGraph.ml b/kernel/uGraph.ml
index 356cf4da6..ee4231b1f 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -834,8 +834,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/lib/envars.ml b/lib/envars.ml
index bafe2401b..512114d5d 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 7a62d5603..d3d4ca5ed 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -94,6 +94,57 @@ let all_subdirs ~unix_path:root =
else msg_warning (str ("Cannot open " ^ 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, cached =
+ try StrMap.find dir !dirmap, true with Not_found ->
+ let contents = make_dir_table dir in
+ dirmap := StrMap.add dir contents !dirmap;
+ 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
+ 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
| [] -> []
@@ -118,7 +169,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 ->
@@ -134,6 +185,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
@@ -141,6 +194,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 2e773fe96..7a91e005c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -59,6 +59,8 @@ val where_in_path_rex :
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]
diff --git a/library/global.ml b/library/global.ml
index 6002382c1..4cffd6b7e 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
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 156c9a277..bdd9ed81c 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/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c4c85a62e..be772a667 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/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 76bf13a57..64a68ba6b 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -177,7 +177,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
@@ -396,7 +396,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)
@@ -486,7 +486,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,
@@ -784,5 +784,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)
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index ce9050d42..3c696502c 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -17,3 +17,47 @@ 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 :=
+ 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 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.
+
+(* 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.
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index f16e6e3f3..00197bd66 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 =
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index b553700c4..e34cbab5f 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -855,7 +855,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
@@ -932,8 +934,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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4a44ad52e..b6a4ab93e 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 UGraph.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 UGraph.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 (UGraph.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 (UGraph.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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 19:11:29 +0000