aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xdev/make-macos-dmg.sh4
-rw-r--r--ide/coqOps.ml5
-rw-r--r--ide/ide_slave.ml1
-rw-r--r--kernel/closure.ml2
-rw-r--r--kernel/indtypes.ml19
-rw-r--r--lib/system.ml6
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--printing/prettyp.ml4
-rw-r--r--stm/asyncTaskQueue.ml7
-rw-r--r--test-suite/bugs/closed/4588.v10
-rw-r--r--test-suite/success/primitiveproj.v16
-rw-r--r--test-suite/success/univers.v17
-rw-r--r--toplevel/record.ml13
13 files changed, 71 insertions, 35 deletions
diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index 20b7b5b53..b43ada907 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/make-macos-dmg.sh
@@ -28,4 +28,8 @@ codesign -f -s - $APP
mkdir -p $DMGDIR
ln -sf /Applications $DMGDIR/Applications
cp -r $APP $DMGDIR
+
+# Temporary countermeasure to hdiutil error 5341
+head -c9703424 /dev/urandom > $DMGDIR/.padding
+
hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 6200f1490..aa1a75db6 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -869,7 +869,10 @@ object(self)
method initialize =
let get_initial_state =
let next = function
- | Fail _ -> messages#set (Richpp.richpp_of_string "Couln't initialize Coq"); Coq.return ()
+ | Fail (_, _, message) ->
+ let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in
+ let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in
+ ignore (popup#run ()); exit 1
| Good id -> initial_state <- id; Coq.return () in
Coq.bind (Coq.init (get_filename ())) next in
Coq.seq get_initial_state Coq.PrintOpt.enforce
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 12ef0e075..9a3e85e47 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -371,6 +371,7 @@ let init =
0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
else Stm.get_current_state (), `NewTip in
Stm.set_compilation_hints file;
+ Stm.finish ();
initial_id
end
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 4476fe524..bf3801e54 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -778,7 +778,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
| Some (Some (_,projs,pbs)) when
- mib.Declarations.mind_finite <> Decl_kinds.CoFinite ->
+ mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
let pars = mib.Declarations.mind_nparams in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4834f95d1..33abfe5b7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -465,7 +465,7 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else
considered sub-terms) as well as the number of of non-uniform
arguments (used to generate induction schemes, so a priori less
relevant to the kernel). *)
-let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
+let check_positivity_one recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
let lparams = Context.Rel.length hyps in
let nmr = Context.Rel.nhyps hyps in
(** Positivity of one argument [c] of a constructor (i.e. the
@@ -580,6 +580,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
| Prod (na,b,d) ->
let () = assert (List.is_empty largs) in
+ if not recursive && not (noccur_between n ntypes b) then
+ raise (InductiveError BadEntry);
let nmr',recarg = check_pos ienv nmr b in
let ienv' = ienv_push_var ienv (na,b,mk_norec) in
check_constr_rec ienv' nmr' (recarg::lrec) d
@@ -614,9 +616,11 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
(** [check_positivity kn env_ar params] checks that the mutually
inductive block [inds] is strictly positive. *)
-let check_positivity kn env_ar params inds =
+let check_positivity kn env_ar params finite inds =
let ntypes = Array.length inds in
- let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
+ let recursive = finite != Decl_kinds.BiFinite in
+ let rc = Array.mapi (fun j t -> (Mrec (kn,j),t))
+ (Rtree.mk_rec_calls ntypes) in
let lra_ind = Array.rev_to_list rc in
let lparams = Context.Rel.length params in
let nmr = Context.Rel.nhyps params in
@@ -625,7 +629,7 @@ let check_positivity kn env_ar params inds =
List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
let nargs = Context.Rel.nhyps sign - nmr in
- check_positivity_one ienv params (kn,i) nargs lcnames lc
+ check_positivity_one recursive ienv params (kn,i) nargs lcnames lc
in
let irecargs_nmr = Array.mapi check_one inds in
let irecargs = Array.map snd irecargs_nmr
@@ -850,10 +854,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
mind_reloc_tbl = rtbl;
} in
let packets = Array.map2 build_one_packet inds recargs in
- let pkt = packets.(0) in
+ let pkt = packets.(0) in
let isrecord =
match isrecord with
- | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1
+ | Some (Some rid) when pkt.mind_kelim == all_sorts
+ && Array.length pkt.mind_consnames == 1
&& pkt.mind_consnrealargs.(0) > 0 ->
(** The elimination criterion ensures that all projections can be defined. *)
let u =
@@ -894,7 +899,7 @@ let check_inductive env kn mie =
(* First type-check the inductive definition *)
let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in
(* Then check positivity conditions *)
- let (nmr,recargs) = check_positivity kn env_ar_par params inds in
+ let (nmr,recargs) = check_positivity kn env_ar_par params mie.mind_entry_finite inds in
(* Build the inductive packets *)
build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
mie.mind_entry_universes
diff --git a/lib/system.ml b/lib/system.ml
index 13cfad4ae..10ef8580b 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -63,8 +63,10 @@ let apply_subdir f path name =
| Unix.S_REG -> f (FileRegular name)
| _ -> ()
+let readdir dir = try Sys.readdir dir with any -> [||]
+
let process_directory f path =
- Array.iter (apply_subdir f path) (Sys.readdir path)
+ Array.iter (apply_subdir f path) (readdir path)
let process_subdirectories f path =
let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
@@ -106,7 +108,7 @@ let dirmap = ref StrMap.empty
let make_dir_table dir =
let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
- Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
+ Array.fold_left filter_dotfiles StrSet.empty (readdir dir)
let exists_in_dir_respecting_case dir bf =
let cache_dir dir =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0ccc5b654..f77e3312b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -858,7 +858,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
- | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite ->
+ | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
let pars = mib.Declarations.mind_nparams in
(try
let l1' = Stack.tail pars sk1 in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b7b1d67f0..9745a7925 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -218,8 +218,8 @@ let print_polymorphism ref =
let print_primitive_record recflag mipv = function
| Some (Some (_, ps,_)) ->
let eta = match recflag with
- | Decl_kinds.CoFinite -> mt ()
- | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+ | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
+ | Decl_kinds.BiFinite -> str " and has eta conversion"
in
[pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
| _ -> []
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 1c6b542ab..c7faef333 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -182,6 +182,13 @@ module Make(T : Task) = struct
let () = Unix.sleep 1 in
kill_if ()
in
+ let kill_if () =
+ try kill_if ()
+ with Sys.Break ->
+ let () = stop_waiting := true in
+ let () = TQueue.broadcast queue in
+ Worker.kill proc
+ in
let _ = Thread.create kill_if () in
try while true do
diff --git a/test-suite/bugs/closed/4588.v b/test-suite/bugs/closed/4588.v
new file mode 100644
index 000000000..ff66277e0
--- /dev/null
+++ b/test-suite/bugs/closed/4588.v
@@ -0,0 +1,10 @@
+Set Primitive Projections.
+
+(* This proof was accepted in Coq 8.5 because the subterm specs were not
+projected correctly *)
+Inductive foo : Prop := mkfoo { proj1 : False -> foo; proj2 : (forall P : Prop, P -> P) }.
+
+Fail Fixpoint loop (x : foo) : False :=
+ loop (proj2 x _ x).
+
+Fail Definition bad : False := loop (mkfoo (fun x => match x with end) (fun _ x => x)).
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 281d707cb..b5e6ccd61 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -35,10 +35,6 @@ Set Implicit Arguments.
Check nat.
-(* Inductive X (U:Type) := Foo (k : nat) (x : X U). *)
-(* Parameter x : X nat. *)
-(* Check x.(k). *)
-
Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }.
Parameter x:X nat.
@@ -49,18 +45,8 @@ Inductive Y := { next : option Y }.
Check _.(next) : option Y.
Lemma eta_ind (y : Y) : y = Build_Y y.(next).
-Proof. reflexivity. Defined.
-
-Variable t : Y.
-
-Fixpoint yn (n : nat) (y : Y) : Y :=
- match n with
- | 0 => t
- | S n => {| next := Some (yn n y) |}
- end.
+Proof. Fail reflexivity. Abort.
-Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}.
-Proof. reflexivity. Defined.
(*
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index e00701fb6..269359ae6 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,3 +60,20 @@ Qed.
(* Submitted by Danko Ilik (bug report #1507); related to LetIn *)
Record U : Type := { A:=Type; a:A }.
+
+(** Check assignement of sorts to inductives and records. *)
+
+Variable sh : list nat.
+
+Definition is_box_in_shape (b :nat * nat) := True.
+Definition myType := Type.
+
+Module Ind.
+Inductive box_in : myType :=
+ myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in.
+End Ind.
+
+Module Rec.
+Record box_in : myType :=
+ BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }.
+End Rec. \ No newline at end of file
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c0bb9eb86..ae0b885e4 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -145,12 +145,13 @@ let typecheck_params_and_fields def id pl t ps nots fs =
arity, evars
else
let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
- if Univ.is_small_univ univ then
- (* We can assume that the level aritysort is not constrained
- and clear it. *)
- mkArity (ctx, Sorts.sort_of_univ univ),
- Evd.set_eq_sort env_ar evars (Prop Pos) aritysort
- else arity, evars
+ if Univ.is_small_univ univ &&
+ Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars aritysort) then
+ (* We can assume that the level in aritysort is not constrained
+ and clear it, if it is flexible *)
+ mkArity (ctx, Sorts.sort_of_univ univ),
+ Evd.set_eq_sort env_ar evars (Prop Pos) aritysort
+ else arity, evars
in
let evars, nf = Evarutil.nf_evars_and_universes evars in
let newps = Context.Rel.map nf newps in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 07:34:08 +0000