From 1cffe2f00d91bc9739b40887eb36f4bbad761c5f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 18 Feb 2021 19:25:53 +0100 Subject: [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 --- .../08-cli-tools/13876-coqc+no_multiple_files.rst | 6 +++++ test-suite/bugs/closed/PLACEHOLDER.v | 0 test-suite/bugs/closed/bug_4836.v | 2 +- toplevel/ccompile.ml | 5 ++-- toplevel/ccompile.mli | 4 ++-- toplevel/coqc.ml | 2 +- toplevel/coqcargs.ml | 27 +++++++++++----------- toplevel/coqcargs.mli | 2 +- 8 files changed, 27 insertions(+), 21 deletions(-) create mode 100644 doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst delete mode 100644 test-suite/bugs/closed/PLACEHOLDER.v 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 `_, + 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 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 -- cgit v1.2.3