From 143244e0606a790b73da2360fb0eabe3d98d4b4e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 4 Nov 2017 19:46:50 +0100 Subject: Removing failure of coq_makefile on no arguments. Nevertheless making option -o of coq_makefile recommended as discussed in PR#6040. This is one way to resolve the inconsistency with the usage which says that all arguments are optional. --- tools/coq_makefile.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'tools') diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 2feaaa04c..28fca0a82 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -66,7 +66,7 @@ let usage () = \n \"none\" to build a makefile with no install target or\ \n \"global\" to force install in $COQLIB directory\ \n[-f file]: take the contents of file as arguments\ -\n[-o file]: output should go in file file\ +\n[-o file]: output should go in file file (recommended)\ \n Output file outside the current directory is forbidden.\ \n[-bypass-API]: when compiling plugins, bypass Coq API\ \n[-h]: print this usage summary\ @@ -381,7 +381,6 @@ let share_prefix s1 s2 = let _ = let prog, args = - if Array.length Sys.argv = 1 then usage (); let args = Array.to_list Sys.argv in let prog = List.hd args in prog, List.tl args in -- cgit v1.2.3 From 19a584d3fa9594abdf3dcc0148f368547ce77ccc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 4 Nov 2017 19:47:18 +0100 Subject: Forbidding -o and -f in input file of coq_makefile. This was apparently either silently doing nothing or failing. --- lib/coqProject_file.ml4 | 7 +++++++ tools/coq_makefile.ml | 35 +++++++++++++++++++++++------------ 2 files changed, 30 insertions(+), 12 deletions(-) (limited to 'tools') diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 970666638..34f9aed37 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -113,6 +113,7 @@ let exists_dir dir = let process_cmd_line orig_dir proj args = + let parsing_project_file = ref (proj.project_file <> None) in let orig_dir = (* avoids turning foo.v in ./foo.v *) if orig_dir = "." then "" else orig_dir in let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in @@ -155,16 +156,22 @@ let process_cmd_line orig_dir proj args = aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r | "-f" :: file :: r -> + if !parsing_project_file then + raise (Parsing_error ("Invalid option -f in project file " ^ Option.get proj.project_file)); let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match proj.project_file with | None -> () | Some _ -> Feedback.msg_warning (Pp.str "Multiple project files are deprecated.") in + parsing_project_file := true; let proj = aux { proj with project_file = Some file } (parse file) in + parsing_project_file := false; aux proj r | "-o" :: file :: r -> + if !parsing_project_file then + raise (Parsing_error ("Invalid option -o in project file " ^ Option.get proj.project_file)); if String.contains file '/' then error "Output file must be in the current directory"; if proj.makefile <> None then diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 28fca0a82..ee59479a5 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -27,16 +27,8 @@ let rec print_prefix_list sep = function | x :: l -> print sep; print x; print_prefix_list sep l | [] -> () -let usage () = - output_string stderr "Usage summary:\ -\n\ -\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ -\n ... [any] ... [-extra[-phony] result dependencies command]\ -\n ... [-I dir] ... [-R physicalpath logicalpath]\ -\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ -\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ -\n [-h] [--help]\ -\n\ +let usage_common () = + output_string stderr "\ \n[file.v]: Coq file to be compiled\ \n[file.ml[i4]?]: Objective Caml file to be compiled\ \n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ @@ -65,10 +57,29 @@ let usage () = \n[-install opt]: where opt is \"user\" to force install into user directory,\ \n \"none\" to build a makefile with no install target or\ \n \"global\" to force install in $COQLIB directory\ +\n[-bypass-API]: when compiling plugins, bypass Coq API\ +\n" + +let usage_coq_project () = + output_string stderr "Available arguments:"; + usage_common (); + exit 1 + +let usage_coq_makefile () = + output_string stderr "Usage summary:\ +\n\ +\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ +\n ... [any] ... [-extra[-phony] result dependencies command]\ +\n ... [-I dir] ... [-R physicalpath logicalpath]\ +\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ +\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ +\n [-h] [--help]\ +\n"; + usage_common (); + output_string stderr "\ \n[-f file]: take the contents of file as arguments\ \n[-o file]: output should go in file file (recommended)\ \n Output file outside the current directory is forbidden.\ -\n[-bypass-API]: when compiling plugins, bypass Coq API\ \n[-h]: print this usage summary\ \n[--help]: equivalent to [-h]\n"; exit 1 @@ -391,7 +402,7 @@ let _ = let project = try cmdline_args_to_project ~curdir:Filename.current_dir_name args - with Parsing_error s -> prerr_endline s; usage () in + with Parsing_error s -> prerr_endline s; usage_coq_project () in if only_destination <> None then begin destination_of project (Option.get only_destination); -- cgit v1.2.3 From b455e96cce263ea48ff0aa8b8ebf530d0f1eea9c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 6 Nov 2017 21:09:00 +0100 Subject: Registering a printing handler in coq_makefile. This allows to fix the non-printing of error messages produced when parsing arguments. --- tools/coq_makefile.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'tools') diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ee59479a5..b7a62a78c 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -391,6 +391,7 @@ let share_prefix s1 s2 = | _ -> false let _ = + let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in let prog, args = let args = Array.to_list Sys.argv in let prog = List.hd args in -- cgit v1.2.3