Merge PR #13876: [coqc] Don't allow to pass more than one file to coqc

Reviewed-by: silene
Reviewed-by: gares

8 files changed, 27 insertions, 21 deletions

diff --git a/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst b/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst
new file mode 100644
index 0000000000..e48b772f01
--- /dev/null
+++ b/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  `coqc` now enforces that at most a single `.v` file can be passed in
+  the command line. Support for multiple `.v` files in the form of
+  `coqc f1.v f2.v` didn't properly work in 8.13, tho it was accepted.
+  (`#13876 <https://github.com/coq/coq/pull/13876>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/bugs/closed/PLACEHOLDER.v
deleted file mode 100644
index e69de29bb2..0000000000
--- a/test-suite/bugs/closed/PLACEHOLDER.v
+++ /dev/null
diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v
index 9aefb10172..62d39619b0 100644
--- a/test-suite/bugs/closed/bug_4836.v
+++ b/test-suite/bugs/closed/bug_4836.v
@@ -1 +1 @@
-(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *)
+(* Placeholder file for directory / file test *)
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index ca09bad441..041097d2d3 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -216,9 +216,8 @@ let compile_file opts stm_opts copts injections (f_in, echo) =
   else
     compile opts stm_opts copts injections ~echo ~f_in ~f_out
 
-let compile_files (opts, stm_opts) copts injections =
-  let compile_list = copts.compile_list in
-  List.iter (compile_file opts stm_opts copts injections) compile_list
+let compile_file opts stm_opts copts injections =
+  Option.iter (compile_file opts stm_opts copts injections) copts.compile_file
 
 (******************************************************************************)
 (* VIO Dispatching                                                            *)
diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli
index 9f3783f32e..e9e83af3ad 100644
--- a/toplevel/ccompile.mli
+++ b/toplevel/ccompile.mli
@@ -12,8 +12,8 @@
    the init (rc) file *)
 val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t
 
-(** [compile_files opts] compile files specified in [opts] *)
-val compile_files : Coqargs.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> Coqargs.injection_command list -> unit
+(** [compile_file opts] compile file specified in [opts] *)
+val compile_file : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Coqcargs.t -> Coqargs.injection_command list -> unit
 
 (** [do_vio opts] process [.vio] files in [opts] *)
 val do_vio : Coqargs.t -> Coqcargs.t -> Coqargs.injection_command list -> unit
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index a403640149..b7af66b2ee 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -44,7 +44,7 @@ coqc specific options:\
 
 let coqc_main ((copts,_),stm_opts) injections ~opts =
   Topfmt.(in_phase ~phase:CompilationPhase)
-    Ccompile.compile_files (opts,stm_opts) copts injections;
+    Ccompile.compile_file opts stm_opts copts injections;
 
   (* Careful this will modify the load-path and state so after this
      point some stuff may not be safe anymore. *)
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index f84d73ed17..efd8a79e18 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -13,7 +13,7 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok
 type t =
   { compilation_mode : compilation_mode
 
-  ; compile_list: (string * bool) list  (* bool is verbosity  *)
+  ; compile_file: (string * bool) option  (* bool is verbosity  *)
   ; compilation_output_name : string option
 
   ; vio_checking : bool
@@ -32,7 +32,7 @@ type t =
 let default =
   { compilation_mode = BuildVo
 
-  ; compile_list = []
+  ; compile_file = None
   ; compilation_output_name = None
 
   ; vio_checking = false
@@ -62,17 +62,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 arg_error msg = CErrors.user_err msg
 
 let is_dash_argument s = String.length s > 0 && s.[0] = '-'
 
 let add_compile ?echo copts s =
-  if is_dash_argument s then (prerr_endline ("Unknown option " ^ s); exit 1);
+  if is_dash_argument s then
+    arg_error Pp.(str "Unknown option " ++ str s);
   (* make the file name explicit; needed not to break up Coq loadpath stuff. *)
   let echo = Option.default copts.echo echo in
   let s =
@@ -81,7 +77,14 @@ let add_compile ?echo copts s =
     then concat current_dir_name s
     else s
   in
-  { copts with compile_list = (s,echo) :: copts.compile_list }
+  { copts with compile_file = Some (s,echo) }
+
+let add_compile ?echo copts v_file =
+  match copts.compile_file with
+  | Some _ ->
+    arg_error Pp.(str "More than one file to compile: " ++ str v_file)
+  | None ->
+    add_compile ?echo copts v_file
 
 let add_vio_task opts f =
   { opts with vio_tasks = f :: opts.vio_tasks }
@@ -230,14 +233,12 @@ let parse arglist : t =
   try
     let opts, extra = parse default in
     let args = List.fold_left add_compile opts extra in
-    check_compilation_output_name_consistency args;
     args
   with any -> fatal_error any
 
 let parse args =
   let opts = parse args in
   { opts with
-    compile_list = List.rev opts.compile_list
-  ; vio_tasks = List.rev opts.vio_tasks
+    vio_tasks = List.rev opts.vio_tasks
   ; vio_files = List.rev opts.vio_files
   }
diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli
index 905250e363..96895568ea 100644
--- a/toplevel/coqcargs.mli
+++ b/toplevel/coqcargs.mli
@@ -27,7 +27,7 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok
 type t =
   { compilation_mode : compilation_mode
 
-  ; compile_list: (string * bool) list  (* bool is verbosity  *)
+  ; compile_file: (string * bool) option  (* bool is verbosity  *)
   ; compilation_output_name : string option
 
   ; vio_checking : bool