[coqc] Don't allow to pass more than one file to coqc

This has been in the TODO queue for a long time, and indeed
I have recently seen some trouble with users passing two .v files to
Coq, which it isn't a) tested, b) supported.

Moreover, it doesn't even work correctly in 8.13 due to some other
changes in the toplevel related to auxiliary files.

(*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work

5 files changed, 20 insertions, 20 deletions

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