Merge branch 'v8.5'

5 files changed, 30 insertions, 64 deletions

diff --git a/library/library.ml b/library/library.ml
index a09f91b15a..024ac9e6fa 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -19,10 +19,12 @@ open Lib
 (************************************************************************)
 (*s Low-level interning/externing of libraries to files *)
 
-(*s Loading from disk to cache (preparation phase) *)
+let raw_extern_library f =
+  System.raw_extern_state Coq_config.vo_magic_number f
 
-let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern Coq_config.vo_magic_number
+let raw_intern_library f =
+  System.with_magic_number_check
+    (System.raw_intern_state Coq_config.vo_magic_number) f
 
 (************************************************************************)
 (** Serialized objects loaded on-the-fly *)
@@ -56,7 +58,7 @@ let in_delayed f ch =
 let fetch_delayed del =
   let { del_digest = digest; del_file = f; del_off = pos; } = del in
   try
-    let ch = System.with_magic_number_check raw_intern_library f in
+    let ch = raw_intern_library f in
     let () = seek_in ch pos in
     let obj, _, digest' = System.marshal_in_segment f ch in
     let () = close_in ch in
@@ -434,7 +436,7 @@ let mk_summary m = {
 }
 
 let intern_from_file f =
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
   let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
   let (lmd : seg_lib delayed) = in_delayed f ch in
   let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
@@ -488,33 +490,11 @@ let rec_intern_library libs mref =
   let _, libs = intern_library libs mref None in
   libs
 
-let rec_intern_by_filename_only f =
-  let m = try intern_from_file f with Sys_error s -> error s in
-  (* We check no other file containing same library is loaded *)
-  if library_is_loaded m.library_name then
-    begin
-      msg_warning
-	(pr_dirpath m.library_name ++ str " is already loaded from file " ++
-	str (library_full_filename m.library_name));
-      m.library_name, []
-    end
- else
-    let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in
-    let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in
-    m.library_name, needed
-
 let native_name_from_filename f =
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
   let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
   Nativecode.mod_uid_of_dirpath lmd.md_name
 
-let rec_intern_library_from_file f =
-  (* A name is specified, we have to check it contains library id *)
-  let paths = Loadpath.get_paths () in
-  let _, f =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
-  rec_intern_by_filename_only f
-
 (**********************************************************************)
 (*s [require_library] loads and possibly opens a library. This is a
     synchronized operation. It is performed as follows:
@@ -590,18 +570,6 @@ let require_library_from_dirpath modrefl export =
       add_anonymous_leaf (in_require (needed,modrefl,export));
   add_frozen_state ()
 
-let require_library_from_file file export =
-  let modref,needed = rec_intern_library_from_file file in
-  let needed = List.rev_map snd needed in
-  if Lib.is_module_or_modtype () then begin
-    add_anonymous_leaf (in_require (needed,[modref],None));
-    Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp)))
-      export
-  end
-  else
-    add_anonymous_leaf (in_require (needed,[modref],export));
-  add_frozen_state ()
-
 (* the function called by Vernacentries.vernac_import *)
 
 let safe_locate_module (loc,qid) =
@@ -686,11 +654,9 @@ let start_library f =
   ldir
 
 let load_library_todo f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let longf = Loadpath.locate_file (f^".v") in
   let f = longf^"io" in
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
   let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
   let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
   let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
@@ -778,7 +744,8 @@ let save_library_to ?todo dir f otab =
   if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then
     error_recursively_dependent_library dir;
   (* Open the vo file and write the magic number *)
-  let (f',ch) = raw_extern_library f in
+  let f' = f in
+  let ch = raw_extern_library f' in
   try
     (* Writing vo payload *)
     System.marshal_out_segment f' ch (sd           : seg_sum);
@@ -801,7 +768,8 @@ let save_library_to ?todo dir f otab =
     iraise reraise
 
 let save_library_raw f sum lib univs proofs =
-  let (f',ch) = raw_extern_library (f^"o") in
+  let f' = f^"o" in
+  let ch = raw_extern_library f' in
   System.marshal_out_segment f' ch (sum        : seg_sum);
   System.marshal_out_segment f' ch (lib        : seg_lib);
   System.marshal_out_segment f' ch (Some univs : seg_univ option);
diff --git a/library/library.mli b/library/library.mli
index 3d96f9a751..d5e610dd67 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -22,7 +22,6 @@ open Libnames
 (** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
-val require_library_from_file : CUnix.physical_path -> bool option -> unit
 
 (** {6 Start the compilation of a library } *)
 
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 26af809e78..622d390a2c 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -28,8 +28,6 @@ let physical p = p.path_physical
 
 let get_load_paths () = !load_paths
 
-let get_paths () = List.map physical !load_paths
-
 let anomaly_too_many_paths path =
   anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
 
@@ -112,3 +110,9 @@ let expand_path dir =
       if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
   in
   aux !load_paths
+
+let locate_file fname =
+  let paths = List.map physical !load_paths in
+  let _,longfname =
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+  longfname
diff --git a/library/loadpath.mli b/library/loadpath.mli
index 3251b8c60c..269e28e0b5 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -27,9 +27,6 @@ val logical : t -> DirPath.t
 val get_load_paths : unit -> t list
 (** Get the current loadpath association. *)
 
-val get_paths : unit -> CUnix.physical_path list
-(** Same as [get_load_paths] but only get the physical part. *)
-
 val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit
 (** [add_load_path phys log type] adds the binding [phys := log] to the current
     loadpaths. *)
@@ -52,3 +49,7 @@ val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list
 val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list
 (** As {!expand_path} but uses a filter function instead, and ignores the
     implicit status of loadpaths. *)
+
+val locate_file : string -> string
+(** Locate a file among the registered paths. Do not use this function, as
+    it does not respect the visibility of paths. *)
diff --git a/library/states.ml b/library/states.ml
index 96a487b160..3cb6da12ec 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -21,18 +21,12 @@ let unfreeze (fl,fs) =
   Lib.unfreeze fl;
   Summary.unfreeze_summaries fs
 
-let (extern_state,intern_state) =
-  let ensure_suffix f = CUnix.make_suffix f ".coq" in
-  let (raw_extern, raw_intern) =
-    extern_intern Coq_config.state_magic_number in
-  (fun s ->
-    let s = ensure_suffix s in
-    raw_extern s (freeze ~marshallable:`Yes)),
-  (fun s ->
-    let s = ensure_suffix s in
-    let paths = Loadpath.get_paths () in
-    unfreeze (with_magic_number_check (raw_intern paths) s);
-    Library.overwrite_library_filenames s)
+let extern_state s =
+  System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes)
+
+let intern_state s =
+  unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
+  Library.overwrite_library_filenames s
 
 (* Rollback. *)