From d692c5dc034778a1d97ace593c9a3658a44e698b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 7 Mar 2014 16:38:59 +0100
Subject: Fix lookup of native files when option -R is missing.

Testcase:
mkdir a
echo "Definition t := O." > a/a.v
coqc -R a a a/a.v
echo "Require Import a.a. Definition u := t." > b.v
coqc -I . b.v
rm -rf a b.*
---
 library/library.ml   | 8 ++------
 library/loadpath.ml  | 8 ++++++++
 library/loadpath.mli | 3 +++
 3 files changed, 13 insertions(+), 6 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 64c2c2ad5..a1760cdf1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -754,9 +754,7 @@ 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_load_paths () in
-      let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in
-      let lp = List.map map_path lp in
+      let lp = Loadpath.get_accessible_paths () in
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Int.equal (Nativelibrary.compile_library dir ast lp fn) 0) then
         msg_error (str"Could not compile the library to native code. Skipping.")
@@ -788,8 +786,6 @@ let mem s =
 		 (CObj.size_kb m.library_objects)))
 
 let get_load_paths_str () =
-  let lp = Loadpath.get_load_paths () in
-  let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in
-  List.map map_path lp
+  List.map CUnix.string_of_physical_path (Loadpath.get_accessible_paths ())
 
 let _ = Nativelib.get_load_paths := get_load_paths_str
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 60799a8a7..7c203bc88 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -22,6 +22,9 @@ 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
@@ -30,6 +33,8 @@ 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)
 
@@ -63,6 +68,9 @@ let add_load_path phys_path isroot coq_path =
   match List.filter filter !load_paths with
   | [] ->
     load_paths := binding :: !load_paths;
+    if isroot then
+      accessible_paths := List.fold_left (fun acc v -> (fst v) :: acc)
+	(phys_path :: !accessible_paths) (System.all_subdirs phys_path)
   | [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 8928542a6..f755ace9e 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -30,6 +30,9 @@ 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 -> bool -> DirPath.t -> unit
 (** [add_load_path root phys log] adds the binding [phys := log] to the current
     loadpaths. The [root] flag indicates whether this loadpath has to be treated
-- 
cgit v1.2.3