mltop: when a plugin is loaded store its full path in the summary

This fixes the following bug related to stm: if one passes -I to coqide, then
such flag is passes to the workers; but if one uses "Add ML LoadPath" to
extend the paths in which coq looks for plugins, this extra path was
no passed to the slaves (via the command line) nor store in the system
state and hence sent to the slaves.

With this patch, when a cmxs is loaded, its full path is stored in the
summary and hence sent to the workers as one may expect.

1 files changed, 52 insertions, 26 deletions

diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 7f421c2644..c609a6e241 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -112,10 +112,11 @@ let report_on_load_obj_error exc =
   else str (Printexc.to_string exc)
 
 (* Dynamic loading of .cmo/.cma *)
-let dir_ml_load s =
+
+let ml_load s =
   match !load with
     | WithTop t ->
-      (try t.load_obj s
+      (try t.load_obj s; s
        with
        | e when Errors.noncritical e ->
         let e = Errors.push e in
@@ -126,15 +127,21 @@ let dir_ml_load s =
             errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
                   str s ++ str" to Coq code (" ++ msg ++ str ")."))
     | WithoutTop ->
-        let warn = Flags.is_verbose() in
-        let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
         try
-          Dynlink.loadfile gname;
+          Dynlink.loadfile s; s
 	with Dynlink.Error a ->
           errorlabstrm "Mltop.load_object"
             (strbrk "while loading " ++ str s ++
              strbrk ": " ++ str (Dynlink.error_message a))
 
+let dir_ml_load s =
+  match !load with
+    | WithTop _ -> ml_load s
+    | WithoutTop ->
+        let warn = Flags.is_verbose() in
+        let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
+        ml_load gname
+
 (* Dynamic interpretation of .ml *)
 let dir_ml_use s =
   match !load with
@@ -215,7 +222,9 @@ let file_of_name name =
     errorlabstrm "Mltop.load_object"
       (str"File not found on loadpath : " ++ str s ++ str"\n" ++
        str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in
-  if is_native then
+  if not (Filename.is_relative name) then
+    if Sys.file_exists name then name else fail name
+  else if is_native then
     let name = match suffix with
       | Some ((".cmo"|".cma") as suffix) ->
           (Filename.chop_suffix name suffix) ^ ".cmxs"
@@ -248,20 +257,25 @@ let file_of_name name =
  * (linked or loaded with load_object). It is used not to load a
  * module twice. It is NOT the list of ML modules Coq knows. *)
 
-let known_loaded_modules = ref String.Set.empty
+let known_loaded_modules = ref String.Map.empty
 
-let add_known_module mname =
-  known_loaded_modules := String.Set.add mname !known_loaded_modules
+let add_known_module mname path =
+  if not (String.Map.mem mname !known_loaded_modules) ||
+     String.Map.find mname !known_loaded_modules = None then
+    known_loaded_modules := String.Map.add mname path !known_loaded_modules
 
 let module_is_known mname =
-  String.Set.mem mname !known_loaded_modules
+  String.Map.mem mname !known_loaded_modules
+
+let known_module_path mname =
+  String.Map.find mname !known_loaded_modules
 
 (** A plugin is just an ML module with an initialization function. *)
 
 let known_loaded_plugins = ref String.Map.empty
 
 let add_known_plugin init name =
-  add_known_module name;
+  add_known_module name None;
   known_loaded_plugins := String.Map.add name init !known_loaded_plugins
 
 let init_known_plugins () =
@@ -288,11 +302,16 @@ let init_ml_object mname =
   try String.Map.find mname !known_loaded_plugins ()
   with Not_found -> ()
 
-let load_ml_object mname fname=
-  dir_ml_load fname;
-  add_known_module mname;
-  init_ml_object mname
+let load_ml_object mname ?path fname=
+  let path = match path with
+    | None -> dir_ml_load fname
+    | Some p -> ml_load p in
+  add_known_module mname (Some path);
+  init_ml_object mname;
+  path
 
+let dir_ml_load m = ignore(dir_ml_load m)
+let add_known_module m = add_known_module m None
 let load_ml_object_raw fname = dir_ml_load (file_of_name fname)
 let load_ml_objects_raw_rex rex =
   List.iter (fun (_,fp) -> dir_ml_load (file_of_name (Filename.basename fp)))
@@ -304,16 +323,19 @@ let load_ml_objects_raw_rex rex =
 
 let loaded_modules = ref []
 let get_loaded_modules () = List.rev !loaded_modules
-let add_loaded_module md = loaded_modules := md :: !loaded_modules
+let add_loaded_module md path =
+  if not (List.mem_assoc md !loaded_modules) then
+    loaded_modules := (md,path) :: !loaded_modules
 let reset_loaded_modules () = loaded_modules := []
 
-let if_verbose_load verb f name fname =
-  if not verb then f name fname
+let if_verbose_load verb f name ?path fname =
+  if not verb then f name ?path fname
   else
     let info = "[Loading ML file "^fname^" ..." in
     try
-      f name fname;
+      let path = f name ?path fname in
       msg_info (str (info^" done]"));
+      path
     with reraise ->
       msg_info (str (info^" failed]"));
       raise reraise
@@ -322,23 +344,27 @@ let if_verbose_load verb f name fname =
     or simulate its reload (i.e. doing nothing except maybe
     an initialization function). *)
 
-let trigger_ml_object verb cache reinit name =
+let trigger_ml_object verb cache reinit ?path name =
   if module_is_known name then begin
     if reinit then init_ml_object name;
-    add_loaded_module name;
+    add_loaded_module name (known_module_path name);
     if cache then perform_cache_obj name
   end else if not has_dynlink then
     error ("Dynamic link not supported (module "^name^")")
   else begin
-    let file = file_of_name name in
-    if_verbose_load (verb && is_verbose ()) load_ml_object name file;
-    add_loaded_module name;
+    let file = file_of_name (Option.default name path) in
+    let path =
+      if_verbose_load (verb && is_verbose ()) load_ml_object name ?path file in
+    add_loaded_module name (Some path);
     if cache then perform_cache_obj name
   end
 
+let load_ml_object n m = ignore(load_ml_object n m)
+
 let unfreeze_ml_modules x =
   reset_loaded_modules ();
-  List.iter (trigger_ml_object false false false) x
+  List.iter
+    (fun (name,path) -> trigger_ml_object false false false ?path name) x
 
 let _ =
   Summary.declare_summary Summary.ml_modules
@@ -385,7 +411,7 @@ let print_ml_path () =
 
 let print_ml_modules () =
   let l = get_loaded_modules () in
-  str"Loaded ML Modules: " ++ pr_vertical_list str l
+  str"Loaded ML Modules: " ++ pr_vertical_list str (List.map fst l)
 
 let print_gc () =
   let stat = Gc.stat () in