Command "Library [Comment|Warning] string" to bind a comment/warning …

…to a file.

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

vernac/g_vernac.mlg

@@ -923,6 +923,9 @@ GRAMMAR EXTEND Gram
   command:
     [ [ IDENT "Comments"; l = LIST0 comment -> { VernacSynPure (VernacComments l) }
 
+      | IDENT "Library"; b = [ IDENT "Comment" -> { false } | IDENT "Warning" -> { true } ];
+        s = STRING -> { VernacSynPure (VernacLibraryComment (b, s)) }
+
       (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
       | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
          t = term LEVEL "200";

vernac/ppvernac.ml

@@ -1216,6 +1216,14 @@ let pr_synpure_vernac_expr v =
          ++ prlist_with_sep sep (pr_comment pr_constr) l)
     )
 
+  | VernacLibraryComment (warning,s) ->
+    return (
+      hov 2
+        (keyword "Library" ++ spc()
+         ++ keyword (if warning then "Warning" else "Comment") ++ spc ()
+         ++ qs s)
+    )
+
   | VernacProof (None, None) ->
     return (keyword "Proof")
   | VernacProof (None, Some e) ->

vernac/vernac_classifier.ml

@@ -176,6 +176,7 @@ let classify_vernac e =
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacComments _
+    | VernacLibraryComment _
     | VernacSchemeEquality _
     | VernacDeclareInstance _ -> VtSideff ([], VtLater)
     (* Who knows *)

vernac/vernacentries.ml

@@ -1399,7 +1399,11 @@ let vernac_require_interp needed modrefl export qidl =
   in
   if Dumpglob.dump () then
     List.iter2 (fun ({CAst.loc},_) dp -> Dumpglob.dump_libref ?loc dp "lib") qidl modrefl;
+  (* Load *)
   Library.require_library_from_dirpath needed;
+  (* Output warnings of the file *)
+  Flags.if_verbose (List.iter (fun m -> Docstring.output_warnings_modpath (MPfile m))) modrefl;
+  (* Import*)
   Option.iter (fun (export,cats) ->
       let cats = interp_import_cats cats in
       List.iter2 (fun m (_,f) ->
@@ -2076,6 +2080,13 @@ let vernac_register qid r =
     end
     else Coqlib.register_ref (Libnames.string_of_qualid n) gr
 
+let vernac_library_comment warning comment =
+  if Global.is_curmod_library () && not (Lib.sections_are_opened ()) then
+    Docstring.declare_docstring_modpath (MPfile (Lib.library_dp ()))
+      { comment; warning }
+  else
+    user_err (Pp.str "A library comment should be at toplevel of the library.")
+
 (********************)
 (* Proof management *)
 
@@ -2499,6 +2510,11 @@ let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with
         unsupported_attributes atts;
         Flags.if_verbose Feedback.msg_info (str "Comments ok\n"))
 
+  | VernacLibraryComment (b,s) ->
+    vtdefault(fun () ->
+        unsupported_attributes atts;
+        vernac_library_comment b s)
+
   (* Proof management *)
   | VernacFocus n ->
     vtmodifyproof(unsupported_attributes atts;vernac_focus n)

vernac/vernacexpr.mli

@@ -472,6 +472,7 @@ type nonrec synpure_vernac_expr =
   | VernacRegister of qualid * register_kind
   | VernacPrimitive of ident_decl * CPrimitives.op_or_type * constr_expr option
   | VernacComments of comment list
+  | VernacLibraryComment of bool * string
 
   (* Proof management *)
   | VernacAbort