Make -print-mod-uid accept a list of files.

Solves an efficiency problem in Makefiles generated by coq_makefile.

3 files changed, 14 insertions, 3 deletions

diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index b4a3639f7..0941dc56c 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -10,6 +10,9 @@ open Nativecode
 (** This file provides facilities to access OCaml compiler and dynamic linker,
 used by the native compiler. *)
 
+(* Directory where compiled files are stored *)
+val output_dir : string
+
 val get_load_paths : (unit -> string list) ref
 
 val load_obj : (string -> unit) ref
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 28b86ddc7..badaf280e 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -503,9 +503,14 @@ let parameters () =
   print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n";
   print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
   print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
+  print "vo_to_obj = $(addsuffix .o,\\\n";
+  print "  $(filter-out Warning: Error:,\\\n";
+  print "  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
+(*
   print "vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),\\\n";
   print "  $(addprefix $(dir $(vo)),$(addprefix .coq-native/,$(filter-out Warning: Error:,$(firstword \\\n";
   print "    $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(vo))))))))\n\n"
+ *)
 
 let include_dirs (inc_ml,inc_i,inc_r) =
   let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9f670c731..142f33867 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -375,9 +375,12 @@ let schedule_vio_compilation () =
   if !vio_files <> [] && not !vio_checking then
     Vio_checking.schedule_vio_compilation !vio_files_j !vio_files
 
-let print_native_name s =
+let get_native_name s =
   (* We ignore even critical errors because this mode has to be super silent *)
-  try print_endline (Library.native_name_from_filename s) with _ -> ()
+  try
+    String.concat Filename.dir_sep [Filename.dirname s;
+      Nativelib.output_dir; Library.native_name_from_filename s]
+  with _ -> ""
 
 let parse_args arglist =
   let args = ref arglist in
@@ -461,7 +464,7 @@ let parse_args arglist =
     |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ())
     |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ())
     |"-outputstate" -> set_outputstate (next ())
-    |"-print-mod-uid" -> print_native_name (next ()); exit 0
+    |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
     |"-require" -> add_require (next ())
     |"-top" -> set_toplevel_name (dirpath_of_string (next ()))
     |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())