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

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

8 files changed, 92 insertions, 70 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index ce00ba6d8c..970d7cf650 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -537,7 +537,11 @@ let rec parse = function
         Xmlprotocol.document Xml_printer.to_string_fmt; exit 0
   | "--xml_format=Ppcmds" :: rest ->
         msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest
-  | x :: rest -> x :: parse rest
+  | x :: rest ->
+     if String.length x > 0 && x.[0] = '-' then
+       (prerr_endline ("Unknown option " ^ x); exit 1)
+     else
+       x :: parse rest
   | [] -> []
 
 let () = Usage.add_to_usage "coqidetop"
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/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 2493b1fac4..8b455821af 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -125,7 +125,7 @@ module Make(T : Task) () = struct
                  "-async-proofs-worker-priority";
                  CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
         (* Options to discard: 0 arguments *)
-        | ("-emacs"|"-emacs-U"|"-batch")::tl ->
+        | ("-emacs"|"-batch")::tl ->
           set_slave_opt tl
         (* Options to discard: 1 argument *)
         | ( "-async-proofs" | "-vio2vo" | "-o"
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
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\