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.

1 files changed, 1 insertions, 9 deletions

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)