Ensuring suffix of file to compile also for -vio2vo checking.

We do it by consistently using variants of the "ensure_exists" policy
in compilation modes: vo (default), vio (-quick), vio2vo (-vio2vo) and
parallel vio2vo (schedule-vio2vo), vio checking (-check-vio-tasks) and
parallel vio checking (schedule-vio-checking).

For instance, coqc -vio2vo dir/file.vio now works, while before,
dir/file was expected.

Incidentally, this avoids the non-recommended Loadpath.locate_file.

4 files changed, 50 insertions, 56 deletions

diff --git a/library/library.ml b/library/library.ml
index 04e38296d9..500e77f89b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -612,8 +612,6 @@ let import_module export modl =
 (*s Initializing the compilation of a library. *)
 
 let load_library_todo f =
-  let longf = Loadpath.locate_file (f^".v") in
-  let f = longf^"io" 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
@@ -626,7 +624,7 @@ let load_library_todo f =
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
-  longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
+  s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
@@ -727,14 +725,13 @@ let save_library_to ?todo ~output_native_objects dir f otab =
     iraise reraise
 
 let save_library_raw f sum lib univs proofs =
-  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);
-  System.marshal_out_segment f' ch (None       : seg_discharge option);
-  System.marshal_out_segment f' ch (None       : 'tasks option);
-  System.marshal_out_segment f' ch (proofs     : seg_proofs);
+  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);
+  System.marshal_out_segment f ch (None       : seg_discharge option);
+  System.marshal_out_segment f ch (None       : 'tasks option);
+  System.marshal_out_segment f ch (proofs     : seg_proofs);
   close_out ch
 
 module StringOrd = struct type t = string let compare = String.compare end
diff --git a/library/library.mli b/library/library.mli
index a976be0184..390299bf56 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -46,7 +46,7 @@ val save_library_to :
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
 val load_library_todo :
-  string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+  string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
 val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
 
 (** {6 Interrogate the status of libraries } *)
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 69c1d9bd23..0f78e0acf6 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -10,11 +10,11 @@
 
 open Util
 
-let check_vio (ts,f) =
+let check_vio (ts,f_in) =
   Dumpglob.noglob ();
-  let long_f_dot_v, _, _, _, _, tasks, _ = Library.load_library_todo f in
-  Stm.set_compilation_hints long_f_dot_v;
-  List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
+  let _, _, _, _, tasks, _ = Library.load_library_todo f_in in
+  Stm.set_compilation_hints f_in;
+  List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts
 
 module Worker = Spawn.Sync ()
 
@@ -28,15 +28,12 @@ module Pool = Map.Make(IntOT)
 let schedule_vio_checking j fs =
   if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
   let jobs = ref [] in
-  List.iter (fun f ->
-    let f =
-      if Filename.check_suffix f ".vio" then Filename.chop_extension f
-      else f in
-    let long_f_dot_v, _,_,_,_, tasks, _ = Library.load_library_todo f in
-    Stm.set_compilation_hints long_f_dot_v;
+  List.iter (fun long_f_dot_vio ->
+    let _,_,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in
+    Stm.set_compilation_hints long_f_dot_vio;
     let infos = Stm.info_tasks tasks in
     let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
-    if infos <> [] then jobs := (f, eta, infos) :: !jobs)
+    if infos <> [] then jobs := (long_f_dot_vio, eta, infos) :: !jobs)
   fs;
   let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in
   jobs := List.sort cmp_job !jobs;
@@ -103,16 +100,12 @@ let schedule_vio_checking j fs =
 let schedule_vio_compilation j fs =
   if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0");
   let jobs = ref [] in
-  List.iter (fun f ->
-    let f =
-      if Filename.check_suffix f ".vio" then Filename.chop_extension f
-      else f in
-    let long_f_dot_v = Loadpath.locate_file (f^".v") in
-    let aux = Aux_file.load_aux_file_for long_f_dot_v in
+  List.iter (fun long_f_dot_vio ->
+    let aux = Aux_file.load_aux_file_for long_f_dot_vio in
     let eta =
       try float_of_string (Aux_file.get aux "vo_compile_time")
       with Not_found -> 0.0 in
-    jobs := (f, eta) :: !jobs)
+    jobs := (long_f_dot_vio, eta) :: !jobs)
   fs;
   let cmp_job (_,t1) (_,t2) = compare t2 t1 in
   jobs := List.sort cmp_job !jobs;
@@ -146,7 +139,7 @@ let schedule_vio_compilation j fs =
     (* set the access and last modification time of all files to the same t
      * not to confuse make into thinking that some of them are outdated *)
     let t = Unix.gettimeofday () in
-    List.iter (fun (f,_) -> Unix.utimes (f^".vo") t t) all_jobs;
+    List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs;
   end;
   exit !rc
 
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 8934385091..2f63410761 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -73,14 +73,18 @@ let ensure_bname src tgt =
 
 let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt
 
-let ensure_v v = ensure ".v" v v
-let ensure_vo v vo = ensure ".vo" v vo
-let ensure_vio v vio = ensure ".vio" v vio
-
 let ensure_exists f =
   if not (Sys.file_exists f) then
     fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
+let ensure_exists_with_prefix f_in f_out src_suffix tgt_suffix =
+  let long_f_dot_src = ensure src_suffix f_in f_in in
+  ensure_exists long_f_dot_src;
+  let long_f_dot_tgt = match f_out with
+    | None -> chop_extension long_f_dot_src ^ tgt_suffix
+    | Some f -> ensure tgt_suffix long_f_dot_src f in
+  long_f_dot_src, long_f_dot_tgt
+
 (* Compile a vernac file *)
 let compile opts copts ~echo ~f_in ~f_out =
   let open Vernac.State in
@@ -102,12 +106,9 @@ let compile opts copts ~echo ~f_in ~f_out =
   match copts.compilation_mode with
   | BuildVo ->
       Flags.record_aux_file := true;
-      let long_f_dot_v = ensure_v f_in in
-      ensure_exists long_f_dot_v;
-      let long_f_dot_vo =
-        match f_out with
-        | None -> long_f_dot_v ^ "o"
-        | Some f -> ensure_vo long_f_dot_v f in
+
+      let long_f_dot_v, long_f_dot_vo =
+        ensure_exists_with_prefix f_in f_out ".v" ".vo" in
 
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
@@ -138,13 +139,8 @@ let compile opts copts ~echo ~f_in ~f_out =
       Flags.record_aux_file := false;
       Dumpglob.noglob ();
 
-      let long_f_dot_v = ensure_v f_in in
-      ensure_exists long_f_dot_v;
-
-      let long_f_dot_vio =
-        match f_out with
-        | None -> long_f_dot_v ^ "io"
-        | Some f -> ensure_vio long_f_dot_v f in
+      let long_f_dot_v, long_f_dot_vio =
+        ensure_exists_with_prefix f_in f_out ".v" ".vio" in
 
       (* We need to disable error resiliency, otherwise some errors
          will be ignored in batch mode. c.f. #6707
@@ -175,13 +171,15 @@ let compile opts copts ~echo ~f_in ~f_out =
       Stm.reset_task_queue ()
 
   | Vio2Vo ->
-      let open Filename in
+
       Flags.record_aux_file := false;
       Dumpglob.noglob ();
-      let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in
-      let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in
-      let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
-      Library.save_library_raw lfdv sum lib univs proofs
+      let long_f_dot_vio, long_f_dot_vo =
+        ensure_exists_with_prefix f_in f_out ".vio" ".vo" in
+      let sum, lib, univs, disch, tasks, proofs =
+        Library.load_library_todo long_f_dot_vio in
+      let univs, proofs = Stm.finish_tasks long_f_dot_vo univs disch proofs tasks in
+      Library.save_library_raw long_f_dot_vo sum lib univs proofs
 
 let compile opts copts ~echo ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
@@ -205,16 +203,22 @@ let compile_files opts copts =
 (******************************************************************************)
 let check_vio_tasks copts =
   let rc =
-    List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
+    List.fold_left (fun acc (n,f) ->
+        let f_in = ensure ".vio" f f in
+        ensure_exists f_in;
+        Vio_checking.check_vio (n,f_in) && acc)
       true (List.rev copts.vio_tasks) in
   if not rc then fatal_error Pp.(str "VIO Task Check failed")
 
 (* vio files *)
 let schedule_vio copts =
+  let l =
+    List.map (fun f -> let f_in = ensure ".vio" f f in ensure_exists f_in; f_in)
+      copts.vio_files in
   if copts.vio_checking then
-    Vio_checking.schedule_vio_checking copts.vio_files_j copts.vio_files
+    Vio_checking.schedule_vio_checking copts.vio_files_j l
   else
-    Vio_checking.schedule_vio_compilation copts.vio_files_j copts.vio_files
+    Vio_checking.schedule_vio_compilation copts.vio_files_j l
 
 let do_vio opts copts =
   (* We must initialize the loadpath here as the vio scheduling