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.

6 files changed, 23 insertions, 18 deletions

diff --git a/lib/system.ml b/lib/system.ml
index d1cdd8efc..139effd9f 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -178,7 +178,7 @@ let raw_extern_intern magic =
   let extern_state filename =
     let channel = open_trapping_failure filename in
     output_binary_int channel magic;
-    filename, channel
+    channel
   and intern_state filename =
     try
       let channel = open_in_bin filename in
@@ -191,11 +191,11 @@ let raw_extern_intern magic =
   in
   (extern_state,intern_state)
 
-let extern_intern ?(warn=true) magic =
+let extern_intern magic =
   let (raw_extern,raw_intern) = raw_extern_intern magic in
-  let extern_state name val_0 =
+  let extern_state filename val_0 =
     try
-      let (filename,channel) = raw_extern name in
+      let channel = raw_extern filename in
       try
         marshal_out channel val_0;
         close_out channel
@@ -205,9 +205,8 @@ let extern_intern ?(warn=true) magic =
         iraise reraise
     with Sys_error s ->
       errorlabstrm "System.extern_state" (str "System error: " ++ str s)
-  and intern_state paths name =
+  and intern_state filename =
     try
-      let _,filename = find_file_in_path ~warn paths name in
       let channel = raw_intern filename in
       let v = marshal_in filename channel in
       close_in channel;
diff --git a/lib/system.mli b/lib/system.mli
index a3d66d577..5797502e9 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -37,10 +37,10 @@ val find_file_in_path :
 exception Bad_magic_number of string
 
 val raw_extern_intern : int ->
-  (string -> string * out_channel) * (string -> in_channel)
+  (string -> out_channel) * (string -> in_channel)
 
-val extern_intern : ?warn:bool -> int ->
-  (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a)
+val extern_intern : int ->
+  (string -> 'a -> unit) * (string -> 'a)
 
 val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
 
diff --git a/library/library.ml b/library/library.ml
index f5c7f6335..0fb938e9b 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 96a487b16..4e55f0cdc 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. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 4031a161b..7562c29f7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -144,13 +144,19 @@ let inputstate = ref ""
 let set_inputstate s =
   let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in
   inputstate:=s
-let inputstate () = if not (String.is_empty !inputstate) then intern_state !inputstate
+let inputstate () =
+  if not (String.is_empty !inputstate) then
+    let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in
+    intern_state fname
 
 let outputstate = ref ""
 let set_outputstate s =
   let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in
   outputstate:=s
-let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate
+let outputstate () =
+  if not (String.is_empty !outputstate) then
+    let fname = CUnix.make_suffix !outputstate ".coq" in
+    extern_state fname
 
 let set_include d p implicit =
   let p = dirpath_of_string p in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ec81a3f1a..8ae6ac2bc 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -929,10 +929,12 @@ let vernac_chdir = function
 
 let vernac_write_state file =
   Pfedit.delete_all_proofs ();
+  let file = CUnix.make_suffix file ".coq" in
   States.extern_state file
 
 let vernac_restore_state file =
   Pfedit.delete_all_proofs ();
+  let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
   States.intern_state file
 
 (************)