Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

2 files changed, 45 insertions, 29 deletions

diff --git a/checker/check.ml b/checker/check.ml
index f8844975..e91516c7 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -209,7 +209,7 @@ let locate_absolute_library dir =
   if loadpath = [] then raise LibUnmappedDir;
   try
     let name = string_of_id base^".vo" in
-    let _, file = System.where_in_path loadpath name in
+    let _, file = System.where_in_path false loadpath name in
     (dir, file)
   with Not_found ->
   (* Last chance, removed from the file system but still in memory *)
@@ -229,7 +229,7 @@ let locate_qualified_library qid =
     in
     if loadpath = [] then raise LibUnmappedDir;
     let name =  qid.basename^".vo" in
-    let path, file = System.where_in_path loadpath name in
+    let path, file = System.where_in_path true loadpath name in
     let dir =
       extend_dirpath (find_logical_path path) (id_of_string qid.basename) in
     (* Look if loaded *)
@@ -267,10 +267,8 @@ let try_locate_qualified_library qid =
 
 (*s Loading from disk to cache (preparation phase) *)
 
-let vo_magic_number = 08190 (* trunk *)
-
 let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern vo_magic_number ".vo"
+  System.raw_extern_intern Coq_config.vo_magic_number ".vo"
 
 let with_magic_number_check f a =
   try f a
@@ -323,7 +321,8 @@ let get_deps (dir, f) =
 
 (* Read a compiled library and all dependencies, in reverse order.
    Do not include files that are already in the context. *)
-let rec intern_library (dir, f) needed =
+let rec intern_library seen (dir, f) needed =
+  if LibrarySet.mem dir seen then failwith "Recursive dependencies!";
   (* Look if in the current logical environment *)
   try let _ = find_library dir in needed
   with Not_found ->
@@ -332,28 +331,34 @@ let rec intern_library (dir, f) needed =
   else
     (* [dir] is an absolute name which matches [f] which must be in loadpath *)
     let m = intern_from_file (dir,f) in
-    (dir,m)::List.fold_right intern_mandatory_library m.library_deps needed
-
-(* digest error with checked modules could be a warning *)
-and intern_mandatory_library (dir,_) needed =
-  intern_library (try_locate_absolute_library dir) needed
+    let seen' = LibrarySet.add dir seen in
+    let deps =
+      List.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps in
+    (dir,m) :: List.fold_right (intern_library seen') deps needed
 
 (* Compute the reflexive transitive dependency closure *)
-let rec fold_deps ff (dir,f) s =
-  if  LibrarySet.mem dir s then s
+let rec fold_deps seen ff (dir,f) (s,acc) =
+  if LibrarySet.mem dir seen then failwith "Recursive dependencies!";
+  if LibrarySet.mem dir s then (s,acc)
   else
     let deps = get_deps (dir,f) in
     let deps = List.map (fun (d,_) -> try_locate_absolute_library d) deps in
-    ff dir (List.fold_right (fold_deps ff) deps s)
+    let seen' = LibrarySet.add dir seen in
+    let (s',acc') = List.fold_right (fold_deps seen' ff) deps (s,acc) in
+    (LibrarySet.add dir s', ff dir acc')
+
+and fold_deps_list seen ff modl needed =
+  List.fold_right (fold_deps seen ff) modl needed
 
-and fold_deps_list  ff modl needed =
-  List.fold_right (fold_deps ff) modl needed
+let fold_deps_list ff modl acc =
+  snd (fold_deps_list LibrarySet.empty ff modl (LibrarySet.empty,acc))
 
 let recheck_library ~norec ~admit ~check =
   let ml = List.map try_locate_qualified_library check in
   let nrl = List.map try_locate_qualified_library norec in
   let al =  List.map try_locate_qualified_library admit in
-  let needed = List.rev (List.fold_right intern_library (ml@nrl) []) in
+  let needed = List.rev
+    (List.fold_right (intern_library LibrarySet.empty) (ml@nrl) []) in
   (* first compute the closure of norec, remove closure of check,
      add closure of admit, and finally remove norec and check *)
   let nochk = fold_deps_list LibrarySet.add nrl LibrarySet.empty in
diff --git a/checker/checker.ml b/checker/checker.ml
index 1c7ace12..7de25835 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -73,16 +73,14 @@ let convert_string d =
     failwith "caught"
 
 let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath =
-  let dirs = all_subdirs dir in
-  let prefix = repr_dirpath coq_dirpath in
-  if dirs <> [] then
+  if exists_dir dir then
+    let dirs = all_subdirs dir in
+    let prefix = repr_dirpath coq_dirpath in
     let convert_dirs (lp,cp) =
-      (lp,Names.make_dirpath
-            ((List.map convert_string (List.rev cp))@prefix)) in
+      (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
     let dirs = map_succeed convert_dirs dirs in
-    begin
-      List.iter Check.add_load_path dirs
-    end
+    List.iter Check.add_load_path dirs;
+    Check.add_load_path (dir,coq_dirpath)
   else
     msg_warning (str ("Cannot open " ^ dir))
 
@@ -101,6 +99,14 @@ let set_default_rec_include d =
   let p = Check.default_root_prefix in
   check_coq_overwriting p; 
   push_rec_include (d, p)
+let set_include d p =
+  let p = dirpath_of_string p in
+  check_coq_overwriting p;
+  push_include (d,p)
+let set_rec_include d p =
+  let p = dirpath_of_string p in
+  check_coq_overwriting p;
+  push_rec_include(d,p)
 
 (* Initializes the LoadPath according to COQLIB and Coq_config *)
 let init_load_path () =
@@ -174,9 +180,11 @@ let print_usage_channel co command =
   output_string co command;
   output_string co "Coq options are:\n";
   output_string co
-"  -I dir                 add directory dir in the include path
+"  -I dir -as coqdir      map physical dir to logical coqdir
+  -I dir                 map directory dir to the empty logical path
   -include dir           (idem)
-  -R dir coqdir          recursively map physical dir to logical coqdir 
+  -R dir -as coqdir      recursively map physical dir to logical coqdir 
+  -R dir coqdir          (idem)
 
   -admit module          load module and dependencies without checking
   -norec module          check module but admit dependencies without checking
@@ -297,11 +305,14 @@ let parse_args() =
    | "-impredicative-set" :: rem -> 
        set_engagement Declarations.ImpredicativeSet; parse rem
 
+    | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
+    | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
     | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
-    | "-R" :: d :: p :: rem ->
-        push_rec_include (d, dirpath_of_string p);parse rem
+    | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem
+    | "-R" :: d :: "-as" :: [] -> usage ()
+    | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
     | "-R" :: ([] | [_]) -> usage ()
 
     | "-debug" :: rem -> set_debug (); parse rem