diff --git a/dev/ci/user-overlays/17716-proux01-deprecate_nonuniform.sh b/dev/ci/user-overlays/17716-proux01-deprecate_nonuniform.sh new file mode 100644 index 000000000000..c9ce6bbca818 --- /dev/null +++ b/dev/ci/user-overlays/17716-proux01-deprecate_nonuniform.sh @@ -0,0 +1,3 @@ +overlay elpi https://github.com/proux01/coq-elpi coq_17716 17716 + +overlay mtac2 https://github.com/proux01/Mtac2 coq_17716 17716 diff --git a/doc/changelog/08-vernac-commands-and-options/17716-deprecate_nonuniform.rst b/doc/changelog/08-vernac-commands-and-options/17716-deprecate_nonuniform.rst new file mode 100644 index 000000000000..a16584f8deb7 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/17716-deprecate_nonuniform.rst @@ -0,0 +1,5 @@ +- **Deprecated:** + the :attr:`nonuniform` attribute, + now subsumed by :attr:`warnings` with "-uniform-inheritance" + (`#17716 `_, + by Pierre Roux). diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index a4084b47b129..85ee17dce29b 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -171,6 +171,10 @@ Coercion Classes Silence the non uniform inheritance warning. + .. deprecated:: 8.18 + + Use the :attr:`warnings` attribute instead with "-uniform-inheritance". + .. exn:: @qualid not declared. :token:`qualid` is not defined globally. @@ -209,7 +213,7 @@ Coercion Classes The :ref:`test for ambiguous coercion paths ` may yield false positives involving the coercion :token:`qualid`. - Use the :attr:`nonuniform` attribute to silence this warning. + Use the :attr:`warnings` attribute with "-uniform-inheritance" to silence this warning. .. warn:: New coercion path ... is ambiguous with existing ... diff --git a/test-suite/output/coercions_nonuniform.out b/test-suite/output/coercions_nonuniform.out index 3817b89621b7..1ce4e81ce29a 100644 --- a/test-suite/output/coercions_nonuniform.out +++ b/test-suite/output/coercions_nonuniform.out @@ -4,7 +4,3 @@ Warning: f does not respect the uniform inheritance condition. File "./output/coercions_nonuniform.v", line 55, characters 0-17: Warning: f' does not respect the uniform inheritance condition. [uniform-inheritance,coercions,default] -File "./output/coercions_nonuniform.v", line 71, characters 7-17: -The command has indeed failed with message: -This command does not support this attribute: nonuniform. -[unsupported-attributes,parsing,default] diff --git a/test-suite/output/coercions_nonuniform.v b/test-suite/output/coercions_nonuniform.v index d0e1dd0312aa..583029ebc6cc 100644 --- a/test-suite/output/coercions_nonuniform.v +++ b/test-suite/output/coercions_nonuniform.v @@ -30,7 +30,7 @@ Parameter D : Type. Parameter f : forall (b : bool) (n : nat), C n b -> D. (* uniform inheritance not satisfied but attribute, no warning *) -#[nonuniform] Coercion f : C >-> D. +#[warning="-uniform-inheritance"] Coercion f : C >-> D. End Test2. @@ -63,9 +63,6 @@ Parameter D : Type. Parameter f : forall (b : bool) (n : nat), C n b -> D. (* uniform inheritance not satisfied but attribute, no warning *) -#[nonuniform] Coercion f' := f. +#[warning="-uniform-inheritance"] Coercion f' := f. End Test5. - -(* Check that attribute is not supported for non coercion definitions *) -Fail #[nonuniform] Definition f := id. diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 578f8a7acc73..5097ac97fe29 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ univs imps impl {CAst.v=name} = let () = if is_coe = Vernacexpr.AddCoercion then ComCoercion.try_add_new_coercion - r ~local:true ~poly:false ~nonuniform:false ~reversible:true in + r ~local:true ~poly:false ~reversible:true in () let instance_of_univ_entry = function @@ -59,7 +59,7 @@ let declare_axiom is_coe ~poly ~local ~kind ?deprecation typ (univs, ubinders) i let () = if is_coe = Vernacexpr.AddCoercion then ComCoercion.try_add_new_coercion - gr ~local ~poly ~nonuniform:false ~reversible:true in + gr ~local ~poly ~reversible:true in let inst = instance_of_univ_entry univs in (gr,inst) diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 3d2fe3c80057..646859400525 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -301,7 +301,7 @@ let warn_uniform_inheritance = Printer.pr_global g ++ strbrk" does not respect the uniform inheritance condition.") -let add_new_coercion_core coef stre poly ~nonuniform ~reversible source target isid : unit = +let add_new_coercion_core coef stre poly ~reversible source target isid : unit = check_source source; let env = Global.env () in let t, _ = Typeops.type_of_global_in_context env coef in @@ -316,7 +316,7 @@ let add_new_coercion_core coef stre poly ~nonuniform ~reversible source target i raise (CoercionError (NoSource source)) in check_source (Some cls); - if not (nonuniform || uniform_cond Evd.empty (* FIXME - for when possibly called with unresolved evars in the future *) + if not (uniform_cond Evd.empty (* FIXME - for when possibly called with unresolved evars in the future *) ctx lvs) then warn_uniform_inheritance coef; let clt = @@ -335,45 +335,44 @@ let add_new_coercion_core coef stre poly ~nonuniform ~reversible source target i let params = List.length (Context.Rel.instance_list EConstr.mkRel 0 ctx) in declare_coercion coef t ~local ~reversible ~isid ~src:cls ~target:clt ~params () - -let try_add_new_coercion_core ref ~local c ~nonuniform ~reversible d e f = - try add_new_coercion_core ref (loc_of_bool local) c ~nonuniform ~reversible d e f +let try_add_new_coercion_core ref ~local c ~reversible d e f = + try add_new_coercion_core ref (loc_of_bool local) c ~reversible d e f with CoercionError e -> user_err (explain_coercion_error ref e ++ str ".") -let try_add_new_coercion ref ~local ~poly ~nonuniform ~reversible = - try_add_new_coercion_core ref ~local poly ~nonuniform ~reversible None None false +let try_add_new_coercion ref ~local ~poly ~reversible = + try_add_new_coercion_core ref ~local poly ~reversible None None false -let try_add_new_coercion_subclass cl ~local ~poly ~nonuniform ~reversible = +let try_add_new_coercion_subclass cl ~local ~poly ~reversible = let coe_ref = build_id_coercion None cl poly in - try_add_new_coercion_core coe_ref ~local poly ~nonuniform ~reversible (Some cl) None true + try_add_new_coercion_core coe_ref ~local poly ~reversible (Some cl) None true -let try_add_new_coercion_with_target ref ~local ~poly ~nonuniform ~reversible ~source ~target = - try_add_new_coercion_core ref ~local poly ~nonuniform ~reversible +let try_add_new_coercion_with_target ref ~local ~poly ~reversible ~source ~target = + try_add_new_coercion_core ref ~local poly ~reversible (Some source) (Some target) false let try_add_new_identity_coercion id ~local ~poly ~source ~target = let ref = build_id_coercion (Some id) source poly in - try_add_new_coercion_core ref ~local poly ~nonuniform:false ~reversible:true + try_add_new_coercion_core ref ~local poly ~reversible:true (Some source) (Some target) true -let try_add_new_coercion_with_source ref ~local ~poly ~nonuniform ~reversible ~source = - try_add_new_coercion_core ref ~local poly ~nonuniform ~reversible (Some source) None false +let try_add_new_coercion_with_source ref ~local ~poly ~reversible ~source = + try_add_new_coercion_core ref ~local poly ~reversible (Some source) None false -let add_coercion_hook poly nonuniform reversible { Declare.Hook.S.scope; dref; _ } = +let add_coercion_hook poly reversible { Declare.Hook.S.scope; dref; _ } = let open Locality in let local = match scope with | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) | Global ImportNeedQualified -> true | Global ImportDefaultBehavior -> false in - let () = try_add_new_coercion dref ~local ~poly ~nonuniform ~reversible in + let () = try_add_new_coercion dref ~local ~poly ~reversible in let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg -let add_coercion_hook ~poly ~nonuniform ~reversible = - Declare.Hook.make (add_coercion_hook poly nonuniform reversible) +let add_coercion_hook ~poly ~reversible = + Declare.Hook.make (add_coercion_hook poly reversible) let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } = let open Locality in @@ -383,7 +382,7 @@ let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } = | Global ImportDefaultBehavior -> false in let cl = class_of_global dref in - try_add_new_coercion_subclass cl ~local:stre ~poly ~nonuniform:false + try_add_new_coercion_subclass cl ~local:stre ~poly let nonuniform = Attributes.bool_attribute ~name:"nonuniform" diff --git a/vernac/comCoercion.mli b/vernac/comCoercion.mli index cfcf341aabac..b214d4f7571a 100644 --- a/vernac/comCoercion.mli +++ b/vernac/comCoercion.mli @@ -19,7 +19,6 @@ val try_add_new_coercion_with_target : GlobRef.t -> local:bool -> poly:bool - -> nonuniform:bool -> reversible:bool -> source:cl_typ -> target:cl_typ @@ -28,7 +27,6 @@ val try_add_new_coercion_with_target (** [try_add_new_coercion ref s] declares [ref], assumed to be of type [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *) val try_add_new_coercion : GlobRef.t -> local:bool -> poly:bool -> - nonuniform:bool -> reversible:bool -> unit (** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a @@ -36,13 +34,12 @@ val try_add_new_coercion : GlobRef.t -> local:bool -> poly:bool -> an identity coercion from [cst] to [tg], named something like ["Id_cst_tg"] *) val try_add_new_coercion_subclass : cl_typ -> local:bool -> poly:bool -> - nonuniform:bool -> reversible:bool -> unit (** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion from [src] to [tg] where the target is inferred from the type of [ref] *) val try_add_new_coercion_with_source : GlobRef.t -> local:bool -> - poly:bool -> nonuniform:bool -> reversible:bool -> source:cl_typ -> unit + poly:bool -> reversible:bool -> source:cl_typ -> unit (** [try_add_new_identity_coercion id s src tg] enriches the environment with a new definition of name [id] declared as an @@ -52,14 +49,14 @@ val try_add_new_identity_coercion -> local:bool -> poly:bool -> source:cl_typ -> target:cl_typ -> unit -val add_coercion_hook : poly:bool -> nonuniform:bool -> reversible:bool -> Declare.Hook.t +val add_coercion_hook : poly:bool -> reversible:bool -> Declare.Hook.t val add_subclass_hook : poly:bool -> reversible:bool -> Declare.Hook.t val class_of_global : GlobRef.t -> cl_typ (** Attribute to silence warning for coercions that don't satisfy - the uniform inheritance condition. *) + the uniform inheritance condition. (deprecated in 8.18) *) val nonuniform : bool option Attributes.attribute val change_reverse : GlobRef.t -> reversible:bool -> unit diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 09c3be70cebc..c0ac9b1936fd 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -811,7 +811,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~pr (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation ~local:false (Global.env ())) where_notations; (* Declare the coercions *) - List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly ~nonuniform:false ~reversible:true) coercions + List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly ~reversible:true) coercions (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name diff --git a/vernac/record.ml b/vernac/record.ml index 3b5c28005d32..6af19212f297 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -340,7 +340,7 @@ let declare_proj_coercion_instance ~flags ref from ~poly ~with_coercion = if with_coercion && flags.Data.pf_coercion then begin let cl = ComCoercion.class_of_global from in let local = flags.Data.pf_locality = Goptions.OptLocal in - ComCoercion.try_add_new_coercion_with_source ref ~local ~poly ~nonuniform:false ~reversible:flags.Data.pf_reversible ~source:cl + ComCoercion.try_add_new_coercion_with_source ref ~local ~poly ~reversible:flags.Data.pf_reversible ~source:cl end; if flags.Data.pf_instance then begin let env = Global.env () in @@ -803,7 +803,7 @@ let declare_structure { Record_decl.mie; primitive_proj; impls; globnames; globa let cstr = (rsp, 1) in let projections = declare_projections rsp (projunivs,ubinders) ~kind:projections_kind inhabitant_id proj_flags implfs fields in let build = GlobRef.ConstructRef cstr in - let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly ~nonuniform:false ~reversible:true in + let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly ~reversible:true in let struc = Structure.make (Global.env ()) rsp projections in let () = declare_structure_entry struc in GlobRef.IndRef rsp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7464f2216b06..11c1c6f04926 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -60,7 +60,6 @@ module DefAttributes = struct canonical_instance : bool; typing_flags : Declarations.typing_flags option; using : Vernacexpr.section_subset_expr option; - nonuniform : bool; reversible : bool; clearbody: bool option; } @@ -71,23 +70,21 @@ module DefAttributes = struct let clearbody = bool_attribute ~name:"clearbody" let parse ?(coercion=false) ?(discharge=NoDischarge) f = - let nonuniform = if coercion then ComCoercion.nonuniform else return None in let clearbody = match discharge with DoDischarge -> clearbody | NoDischarge -> return None in - let ((((((((locality, deprecated), polymorphic), program), - canonical_instance), typing_flags), using), nonuniform), + let (((((((locality, deprecated), polymorphic), program), + canonical_instance), typing_flags), using), reversible), clearbody = parse (locality ++ deprecation ++ polymorphic ++ program ++ - canonical_instance ++ typing_flags ++ using ++ nonuniform ++ + canonical_instance ++ typing_flags ++ using ++ reversible ++ clearbody) f in let using = Option.map Proof_using.using_from_string using in let reversible = Option.default true reversible in - let nonuniform = Option.default false nonuniform in let () = if Option.has_some clearbody && not (Lib.sections_are_opened()) then CErrors.user_err Pp.(str "Cannot use attribute clearbody outside sections.") in - { polymorphic; program; locality; deprecated; canonical_instance; typing_flags; using; nonuniform; reversible; clearbody } + { polymorphic; program; locality; deprecated; canonical_instance; typing_flags; using; reversible; clearbody } end let with_def_attributes ?coercion ?discharge ~atts f = @@ -646,9 +643,9 @@ let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ?clearbody ~kind ~d (* XXX: This should be handled in start_with_initialization, see duplicate using in declare.ml *) |> vernac_set_used_variables_opt ?using -let vernac_definition_hook ~canonical_instance ~local ~poly ~nonuniform ~reversible = let open Decls in function +let vernac_definition_hook ~canonical_instance ~local ~poly ~reversible = let open Decls in function | Coercion -> - Some (ComCoercion.add_coercion_hook ~poly ~nonuniform ~reversible) + Some (ComCoercion.add_coercion_hook ~poly ~reversible) | CanonicalStructure -> Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) | SubClass -> @@ -680,7 +677,7 @@ let vernac_definition_name lid local = let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in - let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic ~nonuniform:atts.nonuniform ~reversible:atts.reversible kind in + let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic ~reversible:atts.reversible kind in let program_mode = atts.program in let poly = atts.polymorphic in let typing_flags = atts.typing_flags in @@ -692,7 +689,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in let scope = enforce_locality_exp atts.locality discharge in - let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind ~nonuniform:atts.nonuniform ~reversible:atts.reversible in + let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind ~reversible:atts.reversible in let program_mode = atts.program in let typing_flags = atts.typing_flags in let name = vernac_definition_name lid scope in @@ -1407,14 +1404,13 @@ let vernac_coercion ~atts ref qidst = let ref' = smart_global ref in match qidst with | Some (qids, qidt) -> - let ((local, poly), nonuniform), reversible = - Attributes.parse Notations.(locality ++ polymorphic ++ ComCoercion.nonuniform ++ reversible) atts in + let (local, poly), reversible = + Attributes.parse Notations.(locality ++ polymorphic ++ reversible) atts in let local = enforce_locality local in - let nonuniform = Option.default false nonuniform in let reversible = Option.default false reversible in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~nonuniform ~reversible + ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~reversible ~source ~target; Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") | None -> diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 99764795c1da..d44af1025d2b 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -104,6 +104,12 @@ let interp_control_entry ~loc (f : control_entry) ~st | ControlRedirect s -> Topfmt.with_output_to_file s (fun () -> fn ~st) () +let deprecated_nonuniform = + CWarnings.create ~name:"deprecated-nonuniform-attribute" + ~category:Deprecation.Version.v8_18 + Pp.(fun () -> strbrk "Attribute '#[nonuniform]' is deprecated, \ + use '#[warning=\"-uniform-inheritance\"]' instead.") + let warnings_att = Attributes.attribute_of_list [ "warnings", Attributes.payload_parser ~cat:(^) ~name:"warnings"; @@ -112,6 +118,12 @@ let warnings_att = let with_generic_atts atts f = let atts, warnings = Attributes.parse_with_extra warnings_att atts in + let atts, nonuniform = Attributes.parse_with_extra ComCoercion.nonuniform atts in + let warnings = + let () = if nonuniform <> None then deprecated_nonuniform () in + if nonuniform <> Some true then warnings else + let ui = "-uniform-inheritance" in + Some (match warnings with Some w -> w ^ "," ^ ui | None -> ui) in match warnings with | None -> f ~atts | Some warnings -> CWarnings.with_warn warnings (fun () -> f ~atts) ()