aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checkFlags.ml1
-rw-r--r--checker/values.ml5
-rw-r--r--doc/changelog/07-commands-and-options/12034-cumul-sprop.rst5
-rw-r--r--doc/sphinx/addendum/sprop.rst7
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst2
-rw-r--r--engine/uState.ml19
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declareops.ml1
-rw-r--r--kernel/environ.ml15
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/safe_typing.mli1
-rw-r--r--kernel/uGraph.ml2
-rw-r--r--kernel/uGraph.mli4
-rw-r--r--library/global.ml4
-rw-r--r--library/global.mli3
-rw-r--r--printing/printer.ml3
-rw-r--r--toplevel/coqargs.ml10
-rw-r--r--toplevel/coqargs.mli1
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--vernac/vernacentries.ml14
-rw-r--r--vernac/vernacentries.mli1
22 files changed, 72 insertions, 33 deletions
diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml
index e8c7dfdfeb..1f5e76bd83 100644
--- a/checker/checkFlags.ml
+++ b/checker/checkFlags.ml
@@ -17,6 +17,7 @@ let set_local_flags flags env =
check_positive = flags.check_positive;
check_universes = flags.check_universes;
conv_oracle = flags.conv_oracle;
+ cumulative_sprop = flags.cumulative_sprop;
}
in
Environ.set_typing_flags flags env
diff --git a/checker/values.ml b/checker/values.ml
index b9efce6948..9bd381e4a9 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -241,7 +241,10 @@ let v_cst_def =
[|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|]
let v_typing_flags =
- v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
+ v_tuple "typing_flags"
+ [|v_bool; v_bool; v_bool;
+ v_oracle; v_bool; v_bool;
+ v_bool; v_bool; v_bool|]
let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
diff --git a/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst
new file mode 100644
index 0000000000..ad7cf44482
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+ Added :flag:`Cumulative StrictProp` to control cumulativity of
+ |SProp| and deprecated now redundant command line
+ ``--cumulative-sprop`` (`#12034
+ <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 9acdd18b89..b2d3687780 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -240,3 +240,10 @@ so correctly converts ``x`` and ``y``.
the kernel when it is passed a term with incorrect relevance marks.
To avoid conversion issues as in ``late_mark`` you may wish to use
it to find when your tactics are producing incorrect marks.
+
+.. flag:: Cumulative StrictProp
+ :name: Cumulative StrictProp
+
+ Set this flag (it is off by default) to make the kernel accept
+ cumulativity between |SProp| and other universes. This makes
+ typechecking incomplete.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7d031b9b7a..f9f7e70baa 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1076,6 +1076,8 @@ Controlling Typing Flags
Print the status of the three typing flags: guard checking, positivity checking
and universe checking.
+See also :flag:`Cumulative StrictProp` in the |SProp| chapter.
+
.. example::
.. coqtop:: all reset
diff --git a/engine/uState.ml b/engine/uState.ml
index ff85f09efa..abd5f2828f 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -39,7 +39,7 @@ type t =
uctx_weak_constraints : UPairSet.t
}
-let initial_sprop_cumulative = UGraph.make_sprop_cumulative UGraph.initial_universes
+let initial_sprop_cumulative = UGraph.set_cumulative_sprop true UGraph.initial_universes
let empty =
{ uctx_names = UNameMap.empty, LMap.empty;
@@ -57,11 +57,11 @@ let elaboration_sprop_cumul =
~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
let make ~lbound u =
- let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in
- { empty with
- uctx_universes = u;
- uctx_universes_lbound = lbound;
- uctx_initial_universes = u}
+ let u = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) u in
+ { empty with
+ uctx_universes = u;
+ uctx_universes_lbound = lbound;
+ uctx_initial_universes = u}
let is_empty ctx =
ContextSet.is_empty ctx.uctx_local &&
@@ -547,10 +547,11 @@ let emit_side_effects eff u =
merge_seff u uctx
let update_sigma_env uctx env =
- let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
+ let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) (Environ.universes env) in
let eunivs =
- { uctx with uctx_initial_universes = univs;
- uctx_universes = univs }
+ { uctx with
+ uctx_initial_universes = univs;
+ uctx_universes = univs }
in
merge_seff eunivs eunivs.uctx_local
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 244cd2865d..11d4120d7c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -92,6 +92,8 @@ type typing_flags = {
indices_matter: bool;
(** The universe of an inductive type must be above that of its indices. *)
+ cumulative_sprop : bool;
+ (** SProp <= Type *)
}
(* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 20dc21900c..b347152c16 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,6 +26,7 @@ let safe_flags oracle = {
enable_VM = true;
enable_native_compiler = true;
indices_matter = true;
+ cumulative_sprop = false;
}
(** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index de8692ff21..cf01711fe7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -431,7 +431,7 @@ let push_subgraph (levels,csts) env =
in
map_universes add_subgraph env
-let set_engagement c env = (* Unsafe *)
+let set_engagement c env =
{ env with env_stratification =
{ env.env_stratification with env_engagement = c } }
@@ -445,6 +445,7 @@ let same_flags {
share_reduction;
enable_VM;
enable_native_compiler;
+ cumulative_sprop;
} alt =
check_guarded == alt.check_guarded &&
check_positive == alt.check_positive &&
@@ -453,14 +454,18 @@ let same_flags {
indices_matter == alt.indices_matter &&
share_reduction == alt.share_reduction &&
enable_VM == alt.enable_VM &&
- enable_native_compiler == alt.enable_native_compiler
+ enable_native_compiler == alt.enable_native_compiler &&
+ cumulative_sprop == alt.cumulative_sprop
[@warning "+9"]
-let set_typing_flags c env = (* Unsafe *)
+let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b)
+
+let set_typing_flags c env =
if same_flags env.env_typing_flags c then env
- else { env with env_typing_flags = c }
+ else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c }
-let make_sprop_cumulative = map_universes UGraph.make_sprop_cumulative
+let set_cumulative_sprop b env =
+ set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
let set_allow_sprop b env =
{ env with env_stratification =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 25ecdfd852..4195f112ca 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -310,7 +310,7 @@ val push_subgraph : Univ.ContextSet.t -> env -> env
val set_engagement : engagement -> env -> env
val set_typing_flags : typing_flags -> env -> env
-val make_sprop_cumulative : env -> env
+val set_cumulative_sprop : bool -> env -> env
val set_allow_sprop : bool -> env -> env
val sprop_allowed : env -> bool
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 50922ffc52..390407fab8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -232,8 +232,6 @@ let set_native_compiler b senv =
let flags = Environ.typing_flags senv.env in
set_typing_flags { flags with enable_native_compiler = b } senv
-let make_sprop_cumulative senv = { senv with env = Environ.make_sprop_cumulative senv.env }
-
let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env }
(** Check that the engagement [c] expected by a library matches
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b42746a882..f5bd27ca12 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -135,7 +135,6 @@ val set_check_positive : bool -> safe_transformer0
val set_check_universes : bool -> safe_transformer0
val set_VM : bool -> safe_transformer0
val set_native_compiler : bool -> safe_transformer0
-val make_sprop_cumulative : safe_transformer0
val set_allow_sprop : bool -> safe_transformer0
val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 449cd0f0f9..5f5f0ef8cd 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -37,7 +37,7 @@ let g_map f g =
if g.graph == g' then g
else {g with graph=g'}
-let make_sprop_cumulative g = {g with sprop_cumulative=true}
+let set_cumulative_sprop b g = {g with sprop_cumulative=b}
let check_smaller_expr g (u,n) (v,m) =
let diff = n - m in
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8a8c09e911..8d9afb0990 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -13,8 +13,8 @@ open Univ
(** {6 Graphs of universes. } *)
type t
-val make_sprop_cumulative : t -> t
-(** Don't use this in the kernel, it makes the system incomplete. *)
+val set_cumulative_sprop : bool -> t -> t
+(** Makes the system incomplete. *)
type 'a check_function = t -> 'a -> 'a -> bool
diff --git a/library/global.ml b/library/global.ml
index abc04a5e14..5c847fda96 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -99,7 +99,9 @@ let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c)
let set_check_positive c = globalize0 (Safe_typing.set_check_positive c)
let set_check_universes c = globalize0 (Safe_typing.set_check_universes c)
let typing_flags () = Environ.typing_flags (env ())
-let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
+let set_cumulative_sprop b =
+ set_typing_flags {(typing_flags()) with Declarations.cumulative_sprop = b}
+let is_cumulative_sprop () = (typing_flags()).Declarations.cumulative_sprop
let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
let sprop_allowed () = Environ.sprop_allowed (env())
let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
diff --git a/library/global.mli b/library/global.mli
index e7133a1034..2acd7e2a67 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -36,7 +36,8 @@ val set_check_guarded : bool -> unit
val set_check_positive : bool -> unit
val set_check_universes : bool -> unit
val typing_flags : unit -> Declarations.typing_flags
-val make_sprop_cumulative : unit -> unit
+val set_cumulative_sprop : bool -> unit
+val is_cumulative_sprop : unit -> bool
val set_allow_sprop : bool -> unit
val sprop_allowed : unit -> bool
diff --git a/printing/printer.ml b/printing/printer.ml
index 81c0a36f53..c2f73715f0 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -989,4 +989,5 @@ let print_and_diff oldp newp =
let pr_typing_flags flags =
str "check_guarded: " ++ bool flags.check_guarded ++ fnl ()
++ str "check_positive: " ++ bool flags.check_positive ++ fnl ()
- ++ str "check_universes: " ++ bool flags.check_universes
+ ++ str "check_universes: " ++ bool flags.check_universes ++ fnl ()
+ ++ str "cumulative sprop: " ++ bool flags.cumulative_sprop
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index cfc89782a1..17435c051e 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -44,7 +44,6 @@ type coqargs_logic_config = {
impredicative_set : Declarations.set_predicativity;
indices_matter : bool;
toplevel_name : Stm.interactive_top;
- cumulative_sprop : bool;
}
type coqargs_config = {
@@ -110,7 +109,6 @@ let default_logic_config = {
impredicative_set = Declarations.PredicativeSet;
indices_matter = false;
toplevel_name = Stm.TopLogical default_toplevel;
- cumulative_sprop = false;
}
let default_config = {
@@ -198,6 +196,10 @@ let set_query opts q =
| Queries queries -> Queries (queries@[q])
}
+let warn_deprecated_sprop_cumul =
+ CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated"
+ (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.")
+
let warn_deprecated_inputstate =
CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
(fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
@@ -520,7 +522,9 @@ let parse_args ~help ~init arglist : t * string list =
add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None)
|"-disallow-sprop" ->
add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
- |"-sprop-cumulative" -> set_logic (fun o -> { o with cumulative_sprop = true }) oval
+ |"-sprop-cumulative" ->
+ warn_deprecated_sprop_cumul();
+ add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None)
|"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
|"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
|"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 8723d21bb4..a51ed6766a 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -20,7 +20,6 @@ type coqargs_logic_config = {
impredicative_set : Declarations.set_predicativity;
indices_matter : bool;
toplevel_name : Stm.interactive_top;
- cumulative_sprop : bool;
}
type coqargs_config = {
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1175494bad..7aad856d0a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -199,7 +199,6 @@ let init_execution opts custom_init =
Global.set_VM opts.config.enable_VM;
Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
- if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative ();
(* Native output dir *)
Nativelib.output_dir := opts.config.native_output_dir;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 044e479aeb..c4c1c2935c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1302,6 +1302,7 @@ let vernac_generalizable ~local =
Implicit_quantifiers.declare_generalizable ~local
let allow_sprop_opt_name = ["Allow";"StrictProp"]
+let cumul_sprop_opt_name = ["Cumulative";"StrictProp"]
let () =
declare_bool_option
@@ -1313,6 +1314,13 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
+ optkey = cumul_sprop_opt_name;
+ optread = Global.is_cumulative_sprop;
+ optwrite = Global.set_cumulative_sprop }
+
+let () =
+ declare_bool_option
+ { optdepr = false;
optkey = ["Silent"];
optread = (fun () -> !Flags.quiet);
optwrite = ((:=) Flags.quiet) }
@@ -1487,21 +1495,21 @@ let () =
optread = CWarnings.get_flags;
optwrite = CWarnings.set_flags }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optkey = ["Guard"; "Checking"];
optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded);
optwrite = (fun b -> Global.set_check_guarded b) }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optkey = ["Positivity"; "Checking"];
optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive);
optwrite = (fun b -> Global.set_check_positive b) }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optkey = ["Universe"; "Checking"];
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 2ac8458ad5..cf233248d7 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -26,3 +26,4 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
val command_focus : unit Proof.focus_kind
val allow_sprop_opt_name : string list
+val cumul_sprop_opt_name : string list
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:22:02 +0000