Fix native_compute for systems with a limited size for the command line.

The call to the native compiler can fail due to the sheer amounts of -I
options passed to it. Indeed, it is easy to get the command line to exceed
512KB, thus causing various operating systems to reject it. This commit
avoids the issue by only passing the -I options that matter for the
currently compiled code.

Note that, in the worst case, this commit is still not sufficient on
Windows (32KB max), but this worst case should be rather uncommon and thus
can be ignored for now.

For the record, the command-line size mandated by Posix is 4KB.

5 files changed, 17 insertions, 23 deletions

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 05e470da9..b877dda8f 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -59,7 +59,8 @@ let write_ml_code fn ?(header=[]) code =
   List.iter (pp_global fmt) (header@code);
   close_out ch_out
 
-let call_compiler ml_filename load_path =
+let call_compiler ml_filename =
+  let load_path = !get_load_paths () in
   let load_path = List.map (fun dn -> dn / output_dir) load_path in
   let include_dirs = List.map Filename.quote (include_dirs () @ load_path) in
   let include_dirs = String.concat " -I " include_dirs in
@@ -75,9 +76,9 @@ let call_compiler ml_filename load_path =
 
 let compile fn code =
   write_ml_code fn code;
-  call_compiler fn (!get_load_paths())
+  call_compiler fn
 
-let compile_library dir code load_path fn =
+let compile_library dir code fn =
   let header = mk_library_header dir in
   let fn = fn ^ source_ext in
   let basename = Filename.basename fn in
@@ -86,7 +87,7 @@ let compile_library dir code load_path fn =
   if not (Sys.file_exists dirname) then Unix.mkdir dirname 0o755;
   let fn = dirname / basename in
   write_ml_code fn ~header code;
-  fst (call_compiler fn load_path)
+  fst (call_compiler fn)
 
 (* call_linker links dynamically the code for constants in environment or a  *)
 (* conversion test. Silently fails if the file does not exist in bytecode    *)
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index e577a9032..a2633ac2c 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -18,8 +18,7 @@ val get_ml_filename : unit -> string * string
 
 val compile : string -> global list -> int * string
 
-val compile_library : Names.dir_path ->
-		      global list -> string list -> string -> int
+val compile_library : Names.dir_path -> global list -> string -> int
 
 val call_linker :
   ?fatal:bool -> string -> string -> code_location_updates option -> unit
diff --git a/library/library.ml b/library/library.ml
index d2d2d72e4..a9cdf1f2f 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -763,9 +763,8 @@ let save_library_to ?todo dir f =
     close_out ch;
     (* Writing native code files *)
     if not !Flags.no_native_compiler then
-      let lp = Loadpath.get_accessible_paths () in
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
-      if not (Int.equal (Nativelib.compile_library dir ast lp fn) 0) then
+      if not (Int.equal (Nativelib.compile_library dir ast fn) 0) then
         msg_error (str"Could not compile the library to native code. Skipping.")
    with reraise ->
     let reraise = Errors.push reraise in
@@ -794,7 +793,13 @@ let mem s =
 		 (CObj.size_kb m) (CObj.size_kb m.library_compiled)
 		 (CObj.size_kb m.library_objects)))
 
-let get_load_paths_str () =
-  List.map CUnix.string_of_physical_path (Loadpath.get_accessible_paths ())
+module StringOrd = struct type t = string let compare = String.compare end
+module StringSet = Set.Make(StringOrd)
 
-let _ = Nativelib.get_load_paths := get_load_paths_str
+let get_used_load_paths () =
+  StringSet.elements
+    (List.fold_left (fun acc m -> StringSet.add
+      (Filename.dirname (library_full_filename m.library_name)) acc)
+       StringSet.empty !libraries_loaded_list)
+
+let _ = Nativelib.get_load_paths := get_used_load_paths
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 2a548fcb6..bc6ea8910 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -24,9 +24,6 @@ type t = {
 
 let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS"
 
-let accessible_paths =
-  Summary.ref ([] : CUnix.physical_path list) ~name:"ACCPATHS"
-
 let logical p = p.path_logical
 
 let physical p = p.path_physical
@@ -35,8 +32,6 @@ let get_load_paths () = !load_paths
 
 let get_paths () = List.map physical !load_paths
 
-let get_accessible_paths () = !accessible_paths
-
 let anomaly_too_many_paths path =
   anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
 
@@ -69,10 +64,7 @@ let add_load_path phys_path path_type coq_path =
   } in
   match List.filter filter !load_paths with
   | [] ->
-    load_paths := binding :: !load_paths;
-    if path_type <> ImplicitPath then
-      accessible_paths := List.fold_left (fun acc v -> (fst v) :: acc)
-	(phys_path :: !accessible_paths) (System.all_subdirs phys_path)
+    load_paths := binding :: !load_paths
   | [p] ->
     let dir = p.path_logical in
     if not (DirPath.equal coq_path dir)
diff --git a/library/loadpath.mli b/library/loadpath.mli
index af86122cf..c8bfd2e59 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -35,9 +35,6 @@ val get_load_paths : unit -> t list
 val get_paths : unit -> CUnix.physical_path list
 (** Same as [get_load_paths] but only get the physical part. *)
 
-val get_accessible_paths : unit -> CUnix.physical_path list
-(** Same as [get_paths] but also get paths that can be relatively accessed. *)
-
 val add_load_path : CUnix.physical_path -> path_type -> DirPath.t -> unit
 (** [add_load_path phys type log] adds the binding [phys := log] to the current
     loadpaths. *)