Merge PR coq#18193: Support for associating a comment or a warning to…

… a library file

Reviewed-by: proux01
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: proux01 <[email protected]>

checker/values.ml

@@ -435,8 +435,14 @@ let v_stm_seg = v_pair v_tasks v_counters
 
 (** Toplevel structures in a vo (see Cic.mli) *)
 
+let v_deprecation =
+  v_pair (Opt String) (Opt String)
+
+let v_library_info =
+  v_sum "library_info" 0 [|[|String|];[|v_deprecation|]|]
+
 let v_libsum =
-  Tuple ("summary", [|v_dp;v_deps;String|])
+  Tuple ("summary", [|v_dp;v_deps;String;List v_library_info|])
 
 let v_lib =
   Tuple ("library",[|v_compiled_lib;v_librarysyntaxobjs;v_libraryobjs|])

doc/changelog/08-vernac-commands-and-options/18193-master+docstring.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  New command :cmd:`Attributes` to assign attributes such as
+  :attr:`deprecated` to a library file
+  (`#18193 <https://github.com/coq/coq/pull/18193>`_,
+  fixes `#8032 <https://github.com/coq/coq/issues/8032>`_,
+  by Hugo Herbelin).

doc/sphinx/language/core/basic.rst

@@ -391,8 +391,9 @@ Settings
 --------
 
 There are several mechanisms for changing the behavior of Coq.  The
-:term:`attribute` mechanism is used to modify the behavior of a single
-:term:`sentence`.  The :term:`flag`, :term:`option` and :term:`table`
+:term:`attribute` mechanism is used to modify the default behavior of a
+:term:`sentence` or to attach information to Coq objects.
+The :term:`flag`, :term:`option` and :term:`table`
 mechanisms are used to modify the behavior of Coq more globally in a
 document or project.
 
@@ -401,11 +402,13 @@ document or project.
 Attributes
 ~~~~~~~~~~
 
-An :gdef:`attribute` modifies the behavior of a single sentence.
+An :gdef:`attribute` is used to modify the default behavior of a
+sentence or to attach information to a Coq object.
 Syntactically, most commands and tactics can be decorated with
 attributes (cf. :n:`@sentence`), but attributes not supported by the
 command or tactic will trigger :warn:`This command does not support
-this attribute`.
+this attribute`. There is also a command :cmd:`Attributes` to
+assign attributes to a whole document.
 
 .. insertprodn attributes legacy_attr
 
@@ -414,7 +417,7 @@ this attribute`.
    attribute ::= @ident {? @attr_value }
    attr_value ::= = @string
    | = @ident
-   | ( {*, @attribute } )
+   | ( {+, @attribute } )
    legacy_attr ::= {| Local | Global }
    | {| Polymorphic | Monomorphic }
    | {| Cumulative | NonCumulative }
@@ -499,6 +502,18 @@ The following attribute is supported by every command:
 
    Alias of :attr:`warnings`.
 
+Document-level attributes
+^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. cmd:: Attributes {+, @attribute }
+   :name: Attributes
+
+   Associates attributes with the
+   document. When compiled with ``coqc`` (see Section
+   :ref:`thecoqcommands`), the attributes are associated with the
+   compiled file and may have an effect when the file is loaded with
+   :cmd:`Require`. Supported attributes include :attr:`deprecated`.
+
 .. _flags-options-tables:
 
 Flags, Options and Tables

doc/sphinx/language/core/inductive.rst

@@ -30,7 +30,7 @@ Inductive types
 
    .. prodn::
       inductive_definition ::= @ident {? @cumul_univ_decl } {* @binder } {? %| {* @binder } } {? : @type } := {? %| } {+| @constructor } {? @decl_notations }
-      constructor ::= {* #[ {*, @attribute } ] } @ident {* @binder } {? @of_type_inst }
+      constructor ::= {* #[ {+, @attribute } ] } @ident {* @binder } {? @of_type_inst }
 
    Defines one or more
    inductive types and its constructors.  Coq generates

doc/sphinx/language/core/records.rst

@@ -22,7 +22,7 @@ Defining record types
 
    .. prodn::
       record_definition ::= {? > } @ident_decl {* @binder } {? : @sort } {? := {? @ident } %{ {*; @record_field } {? ; } %} {? as @ident } }
-      record_field ::= {* #[ {*, @attribute } ] } @name {? @field_spec } {? %| @natural }
+      record_field ::= {* #[ {+, @attribute } ] } @name {? @field_spec } {? %| @natural }
       field_spec ::= {* @binder } @of_type_inst
       | {* @binder } := @term
       | {* @binder } @of_type_inst := @term

doc/sphinx/using/libraries/writing.rst

@@ -6,11 +6,11 @@ to library and plugin authors.  A tutorial for writing Coq plugins is
 available in the Coq repository in `doc/plugin_tutorial
 <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_.
 
-Deprecating library objects or tactics
---------------------------------------
+Deprecating library objects, tactics or library files
+-----------------------------------------------------
 
 You may use the following :term:`attribute` to deprecate a notation,
-tactic, definition, axiom or theorem.  When renaming a definition or theorem, you can introduce a
+tactic, definition, axiom, theorem or file.  When renaming a definition or theorem, you can introduce a
 deprecated compatibility alias using :cmd:`Notation (abbreviation)`
 (see :ref:`the example below <compatibility-alias>`).
 
@@ -25,7 +25,9 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)`
 
    This attribute is supported by the following commands: :cmd:`Ltac`,
    :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`, :cmd:`Ltac2`,
-   :cmd:`Ltac2 Notation`, :cmd:`Ltac2 external`.
+   :cmd:`Ltac2 Notation`, :cmd:`Ltac2 external`, :cmd:`Definition`,
+   :cmd:`Theorem`, and similar commands. To attach it to a
+   compiled library file, use :cmd:`Attributes`.
 
    It can trigger the following warnings:
 

doc/tools/docgram/fullGrammar

@@ -528,6 +528,7 @@ command: [
 | "Remove" "Hints" LIST1 global opt_hintbases
 | "Hint" hint opt_hintbases
 | "Comments" LIST0 comment
+| "Attributes" attribute_list
 | "Declare" "Instance" ident_decl binders ":" term200 hint_info
 | "Declare" "Scope" IDENT
 | "Pwd"
@@ -751,7 +752,7 @@ quoted_attributes: [
 ]
 
 attribute_list: [
-| LIST0 attribute SEP ","
+| LIST1 attribute SEP ","
 ]
 
 attribute: [

doc/tools/docgram/orderedGrammar

@@ -264,7 +264,7 @@ attribute: [
 attr_value: [
 | "=" string
 | "=" ident
-| "(" LIST0 attribute SEP "," ")"
+| "(" LIST1 attribute SEP "," ")"
 ]
 
 legacy_attr: [
@@ -533,7 +533,7 @@ record_definition: [
 ]
 
 record_field: [
-| LIST0 [ "#[" LIST0 attribute SEP "," "]" ] name OPT field_spec OPT [ "|" natural ]
+| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] name OPT field_spec OPT [ "|" natural ]
 ]
 
 field_spec: [
@@ -559,7 +559,7 @@ inductive_definition: [
 ]
 
 constructor: [
-| LIST0 [ "#[" LIST0 attribute SEP "," "]" ] ident LIST0 binder OPT of_type_inst
+| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] ident LIST0 binder OPT of_type_inst
 ]
 
 import_categories: [
@@ -826,6 +826,7 @@ command: [
 | "Create" "HintDb" ident OPT "discriminated"
 | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
 | "Comments" LIST0 [ one_term | string | natural ]
+| "Attributes" LIST1 attribute SEP ","
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
 | "Declare" "Scope" scope_name
 | "Obligation" natural OPT ( "of" ident ) OPT ( ":" type OPT ( "with" ltac_expr ) )

library/global.ml

@@ -20,6 +20,7 @@ module GlobalSafeEnv : sig
   val safe_env : unit -> Safe_typing.safe_environment
   val set_safe_env : Safe_typing.safe_environment -> unit
   val is_joined_environment : unit -> bool
+  val is_curmod_library : unit -> bool
   val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag
 
 end = struct
@@ -30,6 +31,9 @@ let global_env, global_env_summary_tag =
 let is_joined_environment () =
   Safe_typing.is_joined_environment !global_env
 
+let is_curmod_library () =
+  Safe_typing.is_curmod_library !global_env
+
 let assert_not_synterp () =
   if !Flags.in_synterp_phase then
     CErrors.anomaly (
@@ -45,6 +49,7 @@ let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag
 
 let safe_env = GlobalSafeEnv.safe_env
 let is_joined_environment = GlobalSafeEnv.is_joined_environment
+let is_curmod_library = GlobalSafeEnv.is_curmod_library
 
 let env () = Safe_typing.env_of_safe_env (safe_env ())
 

library/global.mli

@@ -152,6 +152,7 @@ val import :
 val env_of_context : Environ.named_context_val -> Environ.env
 
 val is_joined_environment : unit -> bool
+val is_curmod_library : unit -> bool
 
 val is_polymorphic : GlobRef.t -> bool
 val is_template_polymorphic : GlobRef.t -> bool

library/lib.ml

@@ -132,6 +132,8 @@ let dummy = {
 let synterp_state = ref dummy
 let interp_state = ref ([] : Summary.Interp.frozen library_segment)
 
+let library_info = ref []
+
 let contents () = !interp_state
 
 let start_compilation s mp =
@@ -346,6 +348,8 @@ module type LibActions = sig
 
   val drop_objects : frozen -> frozen
 
+  val declare_info : Library_info.t list -> unit
+
 end
 
 module SynterpActions : LibActions with type summary = Summary.Synterp.frozen = struct
@@ -433,6 +437,8 @@ module SynterpActions : LibActions with type summary = Summary.Synterp.frozen =
     let lib_synterp_stk = List.map (fun (node,_) -> drop_node node, []) st.lib_stk in
     { st with lib_stk = lib_synterp_stk }
 
+  let declare_info info = library_info := !library_info @ info
+
 end
 
 module InterpActions : LibActions with type summary = Summary.Interp.frozen = struct
@@ -500,6 +506,8 @@ module InterpActions : LibActions with type summary = Summary.Interp.frozen = st
     in
     List.map (fun (node,_) -> drop_node node, []) interp_state
 
+  let declare_info _ = ()
+
 end
 
 let add_discharged_leaf obj =
@@ -564,6 +572,8 @@ module type StagedLibS = sig
 
   val drop_objects : frozen -> frozen
 
+  val declare_info : Library_info.t list -> unit
+
 end
 
 (** The [StagedLib] abstraction factors out the code dealing with Lib structure
@@ -645,6 +655,8 @@ let init () = Actions.init ()
 
 let drop_objects st = Actions.drop_objects st
 
+let declare_info info = Actions.declare_info info
+
 end
 
 module Synterp : StagedLibS with type summary = Summary.Synterp.frozen = StagedLib(SynterpActions)
@@ -659,7 +671,7 @@ let end_compilation dir =
   synterp_state := { !synterp_state with comp_name = None };
   let syntax_after = Synterp.classify_segment syntax_after in
   let after = Interp.classify_segment after in
-  !synterp_state.path_prefix, after, syntax_after
+  !synterp_state.path_prefix, !library_info, after, syntax_after
 
 (** Compatibility layer *)
 let init () =

library/lib.mli

@@ -139,6 +139,8 @@ module type StagedLibS = sig
   (** Keep only the libobject structure, not the objects themselves *)
   val drop_objects : frozen -> frozen
 
+  val declare_info : Library_info.t list -> unit
+
 end
 
 (** We provide two instances of [StagedLibS], corresponding to the Synterp and
@@ -153,7 +155,7 @@ val start_compilation : DirPath.t -> ModPath.t -> unit
 
 (** Finalize the compilation of a library and return respectively the library
     prefix, the regular objects, and the syntax-related objects. *)
-val end_compilation : DirPath.t -> Nametab.object_prefix * Interp.classified_objects * Synterp.classified_objects
+val end_compilation : DirPath.t -> Nametab.object_prefix * Library_info.t list * Interp.classified_objects * Synterp.classified_objects
 
 (** The function [library_dp] returns the [DirPath.t] of the current
    compiling library (or [default_library]) *)

library/library_info.ml

@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(* This handles attributes associated to a library file *)
+
+(*i*)
+open Names
+(*i*)
+
+type t = Deprecation of Deprecation.t
+
+let warn_library_deprecated =
+  Deprecation.create_warning ~object_name:"Library File"
+    ~warning_name_if_no_since:"deprecated-library-file"
+    (fun dp -> DirPath.print dp)
+
+let warn_library_info ?loc (dp,infos) =
+  match infos with
+  | Deprecation t -> warn_library_deprecated ?loc (dp, t)

library/library_info.mli

@@ -0,0 +1,17 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(* This handles attributes associated to a library file *)
+
+open Names
+
+type t = Deprecation of Deprecation.t
+
+val warn_library_info : ?loc:Loc.t -> DirPath.t * t -> unit

test-suite/output/library_attributes.out

@@ -0,0 +1,10 @@
+File "./output/library_attributes.v", line 4, characters 16-21:
+The command has indeed failed with message:
+This command does not support this attribute: local.
+[unsupported-attributes,parsing,default]
+File "./output/library_attributes.v", line 7, characters 0-70:
+The command has indeed failed with message:
+A library attribute should be at toplevel of the library.
+File "./output/library_attributes.v", line 11, characters 0-69:
+The command has indeed failed with message:
+A library attribute should be at toplevel of the library.

test-suite/output/library_attributes.v

@@ -0,0 +1,12 @@
+Attributes deprecated(note="This library is useless.", since="XX YY").
+
+(* unsupported attributes *)
+Fail Attributes local.
+
+Section Sec.
+Fail Attributes deprecated(note="No library attributes in sections.").
+End Sec.
+
+Module Mod.
+Fail Attributes deprecated(note="No library attributes in modules.").
+End Mod.

test-suite/output/library_attributes_require.out

@@ -0,0 +1,4 @@
+File "./output/library_attributes_require.v", line 1, characters 0-37:
+Warning: Library File TestSuite.library_attributes is deprecated since XX YY.
+This library is useless.
+[deprecated-library-file-since-XX-YY,deprecated-since-XX-YY,deprecated-library-file,deprecated,default]

test-suite/output/library_attributes_require.v

@@ -0,0 +1 @@
+Require TestSuite.library_attributes.

test-suite/prerequisite/library_attributes.v

@@ -0,0 +1 @@
+../output/library_attributes.v

vernac/declaremods.ml

@@ -1579,12 +1579,12 @@ let end_library_hook () =
 
 let end_library ~output_native_objects dir =
   end_library_hook();
-  let prefix, lib_stack, lib_stack_syntax = Lib.end_compilation dir in
+  let prefix, info, lib_stack, lib_stack_syntax = Lib.end_compilation dir in
   let mp,cenv,ast = Global.export ~output_native_objects dir in
   assert (ModPath.equal mp (MPfile dir));
   let {Lib.Interp.substobjs = substitute; keepobjs = keep; anticipateobjs = _; } = lib_stack in
   let {Lib.Synterp.substobjs = substitute_syntax; keepobjs = keep_syntax; anticipateobjs = _; } = lib_stack_syntax in
-  cenv,(substitute,keep),(substitute_syntax,keep_syntax),ast
+  cenv,(substitute,keep),(substitute_syntax,keep_syntax),ast,info
 
 (** {6 Iterators} *)
 

vernac/declaremods.mli

@@ -155,7 +155,7 @@ val start_library : library_name -> unit
 
 val end_library :
   output_native_objects:bool -> library_name ->
-  Safe_typing.compiled_library * library_objects * library_objects * Nativelib.native_library
+  Safe_typing.compiled_library * library_objects * library_objects * Nativelib.native_library * Library_info.t list
 
 (** append a function to be executed at end_library *)
 val append_end_library_hook : (unit -> unit) -> unit