Merge PR #10160: Miscellaneous fixes related to the command line

Ack-by: gares
Ack-by: herbelin
Reviewed-by: vbgl

3 files changed, 65 insertions, 37 deletions

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
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index 7445619d26..2279ce5505 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -56,6 +56,13 @@ let error_missing_arg s =
   prerr_endline "See -help for the syntax of supported options";
   exit 1
 
+let check_compilation_output_name_consistency args =
+  match args.compilation_output_name, args.compile_list with
+  | Some _, _::_::_ ->
+    prerr_endline ("Error: option -o is not valid when more than one");
+    prerr_endline ("file have to be compiled")
+  | _ -> ()
+
 let add_compile ?echo copts s =
   (* make the file name explicit; needed not to break up Coq loadpath stuff. *)
   let echo = Option.default copts.echo echo in
@@ -82,7 +89,22 @@ let set_vio_checking_j opts opt j =
     prerr_endline "setting the J variable like in 'make vio2vo J=3'";
     exit 1
 
-let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
+let set_compilation_mode opts mode =
+  match opts.compilation_mode with
+  | BuildVo -> { opts with compilation_mode = mode }
+  | mode' when mode <> mode' ->
+    prerr_endline "Options -quick and -vio2vo are exclusive";
+    exit 1
+  | _ -> opts
+
+let get_task_list s =
+  List.map (fun s ->
+      try int_of_string s
+      with Failure _ ->
+        prerr_endline "Option -check-vio-tasks expects a comma-separated list";
+        prerr_endline "of integers followed by a list of files";
+        exit 1)
+    (Str.split (Str.regexp ",") s)
 
 let is_not_dash_option = function
   | Some f when String.length f > 0 && f.[0] <> '-' -> true
@@ -138,7 +160,7 @@ let parse arglist : t =
         | "-o" ->
           { oval with compilation_output_name = Some (next ()) }
         | "-quick" ->
-          { oval with compilation_mode = BuildVio }
+          set_compilation_mode oval BuildVio
         | "-check-vio-tasks" ->
           let tno = get_task_list (next ()) in
           let tfile = next () in
@@ -157,7 +179,7 @@ let parse arglist : t =
 
         | "-vio2vo" ->
           let oval = add_compile ~echo:false oval (next ()) in
-          { oval with compilation_mode = Vio2Vo }
+          set_compilation_mode oval Vio2Vo
 
         | "-outputstate" ->
           set_outputstate oval (next ())
@@ -170,5 +192,7 @@ let parse arglist : t =
   in
   try
     let opts, extra = parse default in
-    List.fold_left add_compile opts extra
+    let args = List.fold_left add_compile opts extra in
+    check_compilation_output_name_consistency args;
+    args
   with any -> fatal_error any
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index da2094653b..29948d50b2 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -42,12 +42,12 @@ let print_usage_common co command =
 \n\
 \n  -load-ml-object f      load ML object file f\
 \n  -load-ml-source f      load ML file f\
-\n  -load-vernac-source f  load Coq file f.v (Load f.)\
+\n  -load-vernac-source f  load Coq file f.v (Load \"f\".)\
 \n  -l f                   (idem)\
-\n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose f.)\
-\n  -lv f	                 (idem)\
-\n  -load-vernac-object f  load Coq object file f.vo\
 \n  -require path          load Coq library path and import it (Require Import path.)\
+\n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose \"f\".)\
+\n  -lv f	           (idem)\
+\n  -load-vernac-object path  load Coq library path (Require path)\
 \n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config, --config      print Coq's configuration information and exit\
@@ -74,9 +74,9 @@ let print_usage_common co command =
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -mangle-names x        mangle auto-generated names using prefix x\
-\n  -set \"Foo Bar\"       enable Foo Bar (as Set Foo Bar. in a file)\
-\n  -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\
-\n  -unset \"Foo Bar\"     disable Foo Bar (as Unset Foo Bar. in a file)\
+\n  -set \"Foo Bar\"         enable Foo Bar (as Set Foo Bar. in a file)\
+\n  -set \"Foo Bar=value\"   set Foo Bar to value (value is interpreted according to Foo Bar's type)\
+\n  -unset \"Foo Bar\"       disable Foo Bar (as Unset Foo Bar. in a file)\
 \n  -time                  display the time taken by each command\
 \n  -profile-ltac          display the time taken by each (sub)tactic\
 \n  -m, --memory           display total heap size at program exit\
@@ -107,7 +107,7 @@ coqtop specific options:\
   exit 1
 
 let print_usage_coqc () =
-  print_usage_common stderr "Usage: coqc <options> <Coq options> file...";
+  print_usage_common stderr "Usage: coqc <options> <Coq options> file...\n\n";
   output_string stderr "\n\
 coqc specific options:\
 \n\