From 2cf609c41f7af83d9eaf43308a368fcb7307e6fa Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 28 Sep 2015 11:04:59 +0200
Subject: Make -load-vernac-object respect the loadpath.

This command-line option was behaving like the old -require, except that
it did not do Import. In other words, it was loading files without
respecting the loadpath. Now it behaves exactly like Require, while
-require now behaves like Require Import.

This patch also removes Library.require_library_from_file and all its
dependencies, since they are no longer used inside Coq.
---
 library/library.ml  | 34 ----------------------------------
 library/library.mli |  1 -
 2 files changed, 35 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index a09f91b15a..6d7b0f603a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -488,33 +488,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 (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 +568,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) =
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 } *)
 
-- 
cgit v1.2.3


From da4d0b0e3d82621fe8338dd313b788472fc31bb2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 29 Sep 2015 10:26:08 +0200
Subject: Remove some uses of Loadpath.get_paths.

The single remaining use is in library/states.ml. This use should be
reviewed, as it is most certainly broken.

The other uses of Loadpath.get_paths did not disappear by miracle though.
They were replaced by a new function Loadpath.locate_file which factors
all the uses of the function. This function should not be used as it is as
broken as Loadpath.get_paths, by definition.

Vernac.load_vernac now takes a complete path rather than looking up for
the file. That is the way it was used most of the time, so the lookup was
unnecessary. For instance, Vernac.compile was calling Library.start_library
which already expected a complete path.

Another consequence is that System.find_file_in_path is almost no longer
used (except for Loadpath.locate_file, obviously). The two remaining uses
are System.intern_state (used by States.intern_state, cf above) and
Mltop.dir_ml_load for dynamically loading compiled .ml files.
---
 library/library.ml   | 4 +---
 library/loadpath.ml  | 6 ++++++
 library/loadpath.mli | 4 ++++
 3 files changed, 11 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 6d7b0f603a..f5c7f63358 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -652,9 +652,7 @@ 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 (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 26af809e78..d35dca2125 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -112,3 +112,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 = get_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..c2c689af70 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -52,3 +52,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. *)
-- 
cgit v1.2.3


From 82a618e8a4945752698a7900c8af7a51091f7b1b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 29 Sep 2015 17:05:45 +0200
Subject: Prevent States.intern_state and System.extern_intern from looking up
 files in the loadpath.

This patch causes a bit of code duplication (because of the .coq suffix
added to state files) but it makes it clear which part of the code is
looking up files in the loadpath and for what purpose. Also it makes the
interface of System.extern_intern and System.raw_extern_intern much saner.
---
 library/library.ml | 6 ++++--
 library/states.ml  | 6 +-----
 2 files changed, 5 insertions(+), 7 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index f5c7f63358..0fb938e9b6 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -742,7 +742,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);
@@ -765,7 +766,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/states.ml b/library/states.ml
index 96a487b160..4e55f0cdc6 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -22,16 +22,12 @@ let unfreeze (fl,fs) =
   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);
+    unfreeze (with_magic_number_check raw_intern s);
     Library.overwrite_library_filenames s)
 
 (* Rollback. *)
-- 
cgit v1.2.3


From 05ab666a1283de5500dbc0520d18bdb05d95f286 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 29 Sep 2015 17:45:27 +0200
Subject: Make the interface of System.raw_extern_intern much saner.

There is no reason (any longer?) to create simultaneous closures for
interning and externing files. This patch makes the code more readable
by separating both functions and their signatures.
---
 library/library.ml | 16 +++++++++-------
 library/states.ml  | 14 ++++++--------
 2 files changed, 15 insertions(+), 15 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 0fb938e9b6..6da9ccf68b 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
@@ -489,7 +491,7 @@ let rec_intern_library libs mref =
   libs
 
 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
 
@@ -654,7 +656,7 @@ let start_library f =
 let load_library_todo f =
   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
diff --git a/library/states.ml b/library/states.ml
index 4e55f0cdc6..3cb6da12ec 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -21,14 +21,12 @@ let unfreeze (fl,fs) =
   Lib.unfreeze fl;
   Summary.unfreeze_summaries fs
 
-let (extern_state,intern_state) =
-  let (raw_extern, raw_intern) =
-    extern_intern Coq_config.state_magic_number in
-  (fun s ->
-    raw_extern s (freeze ~marshallable:`Yes)),
-  (fun s ->
-    unfreeze (with_magic_number_check raw_intern 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. *)
 
-- 
cgit v1.2.3


From 99918c8a8cfb4285798a70351673be2679a6e819 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 29 Sep 2015 21:27:26 +0200
Subject: Fix dumb typo.

---
 library/library.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 6da9ccf68b..024ac9e6fa 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -768,7 +768,7 @@ let save_library_to ?todo dir f otab =
     iraise reraise
 
 let save_library_raw f sum lib univs proofs =
-  let f' = 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);
-- 
cgit v1.2.3


From b248c23b84a96ef692e4a3ded6668733820e1a77 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 30 Sep 2015 06:52:01 +0200
Subject: Unexport Loadpath.get_paths.

---
 library/loadpath.ml  | 4 +---
 library/loadpath.mli | 3 ---
 2 files changed, 1 insertion(+), 6 deletions(-)

(limited to 'library')

diff --git a/library/loadpath.ml b/library/loadpath.ml
index d35dca2125..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)
 
@@ -114,7 +112,7 @@ let expand_path dir =
   aux !load_paths
 
 let locate_file fname =
-  let paths = get_paths () in
+  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 c2c689af70..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. *)
-- 
cgit v1.2.3