Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

26 files changed, 109 insertions, 51 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index d47a93c70d..a16a871dc3 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,5 +1,6 @@
 Analyze
 
+CheckFlags
 CheckInductive
 Mod_checking
 CheckTypes
diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml
new file mode 100644
index 0000000000..1f5e76bd83
--- /dev/null
+++ b/checker/checkFlags.ml
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Declarations
+
+let set_local_flags flags env =
+  let flags =
+    { (Environ.typing_flags env) with
+      check_guarded = flags.check_guarded;
+      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/checkFlags.mli b/checker/checkFlags.mli
new file mode 100644
index 0000000000..2e41e656f1
--- /dev/null
+++ b/checker/checkFlags.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val set_local_flags : Declarations.typing_flags -> Environ.env -> Environ.env
+(** Set flags except for those ignored by the checker (eg vm_compute). *)
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index a1d5aedb01..c370a77ea0 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -164,16 +164,7 @@ let check_inductive env mind mb =
         mind_private; mind_typing_flags; }
     =
     (* Locally set typing flags for further typechecking *)
-    let mb_flags = mb.mind_typing_flags in
-    let env = Environ.set_typing_flags
-        {env.env_typing_flags with
-         check_guarded = mb_flags.check_guarded;
-         check_positive = mb_flags.check_positive;
-         check_universes = mb_flags.check_universes;
-         conv_oracle = mb_flags.conv_oracle;
-        }
-        env
-    in
+    let env = CheckFlags.set_local_flags mb.mind_typing_flags env in
     Indtypes.check_inductive env ~sec_univs:None mind entry
   in
   let check = check mind in
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 44b7089fd0..8fd81d43be 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -17,14 +17,7 @@ let set_indirect_accessor f = indirect_accessor := f
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
-  let cb_flags = cb.const_typing_flags in
-  let env = Environ.set_typing_flags
-      {env.env_typing_flags with
-       check_guarded = cb_flags.check_guarded;
-       check_universes = cb_flags.check_universes;
-       conv_oracle = cb_flags.conv_oracle;}
-      env
-  in
+  let env = CheckFlags.set_local_flags cb.const_typing_flags env in
   let poly, env =
     match cb.const_universes with
     | Monomorphic ctx ->
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 a0d1080314..60fdbf0a9d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1096,6 +1096,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 58b516dfdd..9fabb441d1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -243,8 +243,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 3926b91a55..d84bac5608 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