Include digests of Declare ML Module dependencies in .vo

cf coq#17490

vernac/mltop.ml

@@ -75,6 +75,8 @@ module Fl_internals = struct
 
 end
 
+let dbg_dynlink = CDebug.create ~name:"dynlink" ()
+
 module PluginSpec : sig
 
   type t
@@ -94,6 +96,9 @@ module PluginSpec : sig
      should strengthen this invariant. *)
   val digest : t -> Digest.t list
 
+  (** bool = true for implicit dependencies *)
+  val add_deps : t list -> (bool * t) list
+
   val pp : t -> string
 
   module Set : CSet.ExtS with type elt = t
@@ -103,6 +108,16 @@ end = struct
 
   type t = { lib : string }
 
+  let compare { lib = l1 } { lib = l2 } = String.compare l1 l2
+
+  module Self = struct
+      type nonrec t = t
+      let compare = compare
+    end
+
+  module Set = CSet.Make(Self)
+  module Map = CMap.Make(Self)
+
   module Errors = struct
 
     let warn_legacy_loading =
@@ -136,27 +151,47 @@ end = struct
 
   let load = function
     | { lib } ->
-      Fl_dynload.load_packages [lib]
+      if Findlib.is_recorded_package lib then
+        dbg_dynlink Pp.(fun () -> str lib ++ str " already loaded")
+      else begin
+        (* no point in using Fl_dynload since we [add_deps] to get digests *)
+        let plugins = Fl_internals.fl_find_plugins lib in
+        dbg_dynlink Pp.(fun () ->
+            str lib ++ str ": linking" ++ spc() ++
+            prlist_with_sep spc str plugins);
+        List.iter Dynlink.loadfile plugins;
+        Findlib.record_package Record_load lib
+      end
+
+  let add_deps plugins =
+    let explicit = Set.of_list plugins in
+    let preds = Findlib.recorded_predicates() in
+    let allplugins = Findlib.package_deep_ancestors preds (List.map to_package plugins) in
+    let deps = List.filter_map (fun lib ->
+        (* comes from findlib so guaranteed valid *)
+        let plugin = { lib } in
+        let explicit = Set.mem plugin explicit in
+        (* only add not-yet-loaded implicit deps *)
+        if not explicit && Findlib.is_recorded_package lib then None
+        else Some (not explicit, plugin))
+      allplugins
+    in
+    dbg_dynlink Pp.(fun () ->
+        str "for " ++ prlist_with_sep spc (fun {lib} -> str lib) plugins ++
+        str ":" ++ fnl() ++
+        str "all deps " ++ prlist_with_sep spc str allplugins ++ fnl() ++
+        str "filtered " ++ prlist_with_sep spc (fun (_,{lib}) -> str lib) deps);
+    deps
 
   let digest s =
     match s with
     | { lib } ->
       let plugins = Fl_internals.fl_find_plugins lib in
       List.map Digest.file plugins
 
-  let compare { lib = l1 } { lib = l2 } = String.compare l1 l2
-
   let pp = function
     | { lib } -> lib
 
-  module Self = struct
-      type nonrec t = t
-      let compare = compare
-    end
-
-  module Set = CSet.Make(Self)
-  module Map = CMap.Make(Self)
-
 end
 
 (* If there is a toplevel under Coq *)
@@ -317,28 +352,36 @@ let add_loaded_module md =
 
 let reset_loaded_modules () = loaded_modules := []
 
-let if_verbose_load verb f name =
-  if not verb then f name
-  else
-    let info = str "[Loading ML file " ++ str (PluginSpec.pp name) ++ str " ..." in
-    try
-      let path = f name in
-      Feedback.msg_info (info ++ str " done]");
-      path
-    with reraise ->
-      Feedback.msg_info (info ++ str " failed]");
-      raise reraise
+type load_request =
+  | Summary
+  | Regular of { implicit : bool }
+
+let if_verbose_load req f name =
+  match req with
+  | Regular {implicit} when not !Flags.quiet -> begin
+      let info =
+        str "[Loading ML file " ++ str (PluginSpec.pp name) ++
+        (if implicit then str " (implicit dependency)" else mt()) ++ str " ..." in
+      try
+        let path = f name in
+        Feedback.msg_info (info ++ str " done]");
+        path
+      with reraise ->
+        Feedback.msg_info (info ++ str " failed]");
+        raise reraise
+    end
+  | Summary | Regular _ -> f name
 
 (** Load a module for the first time (i.e. dynlink it) *)
 
-let trigger_ml_object ~verbose plugin =
+let trigger_ml_object req plugin =
   let () =
     if not @@ plugin_is_known plugin then begin
       if not has_dynlink then
         CErrors.user_err
           (str "Dynamic link not supported (module " ++ str (PluginSpec.pp plugin) ++ str ").")
       else
-        if_verbose_load (verbose && not !Flags.quiet) load_ml_object plugin
+        if_verbose_load req load_ml_object plugin
     end
   in
   add_loaded_module plugin
@@ -348,7 +391,7 @@ let unfreeze_ml_modules x =
   List.iter
     (fun name ->
        let name = PluginSpec.of_package name in
-       trigger_ml_object ~verbose:false name) x
+       trigger_ml_object Summary name) x
 
 let () =
   Summary.declare_ml_modules_summary
@@ -361,22 +404,26 @@ let () =
 (* Liboject entries of declared ML Modules *)
 type ml_module_object =
   { mlocal : Vernacexpr.locality_flag
-  ; mnames : PluginSpec.t list
+  ; mnames : (bool * PluginSpec.t) list
+  (* bool: if true then implicit dep
+     XXX should we init_ml_object even for implicit deps? *)
   ; mdigests : Digest.t list
   }
 
 let cache_ml_objects mnames =
-  let iter obj =
-    trigger_ml_object ~verbose:true obj;
-    init_ml_object obj;
-    perform_cache_obj obj
+  let iter (implicit,obj) =
+    trigger_ml_object (Regular {implicit}) obj;
+    if not implicit then begin
+      init_ml_object obj;
+      perform_cache_obj obj
+    end
   in
   List.iter iter mnames
 
 let load_ml_objects _ {mnames; _} =
-  let iter obj =
-    trigger_ml_object ~verbose:true obj;
-    init_ml_object obj
+  let iter (implicit,obj) =
+    trigger_ml_object (Regular {implicit}) obj;
+    if not implicit then init_ml_object obj
   in
   List.iter iter mnames
 
@@ -397,7 +444,8 @@ let declare_ml_modules local mnames =
   let mnames = List.map (PluginSpec.of_package ~usercode:true) mnames in
   if Lib.sections_are_opened()
   then CErrors.user_err Pp.(str "Cannot Declare ML Module while sections are opened.");
-  let mdigests = CList.concat_map PluginSpec.digest mnames in
+  let mnames = PluginSpec.add_deps mnames in
+  let mdigests = CList.concat_map (fun (_,plugin) -> PluginSpec.digest plugin) mnames in
   Lib.add_leaf (inMLModule {mlocal=local; mnames; mdigests});
   (* We can't put this in cache_function: it may declare other
      objects, and when the current module is required we want to run