Merge PR coq#18088: coq_makefile: print help to stdout when using -h,…

… add -v --version flags Reviewed-by: silene Reviewed-by: JasonGross Co-authored-by: silene <[email protected]>
Villetaneuse · Oct 5, 2023 · d5b30cb · d5b30cb
2 parents b5d259a + ec3083c
commit d5b30cb
Show file tree

Hide file tree

Showing 4 changed files with 61 additions and 32 deletions.
diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml
@@ -19,7 +19,7 @@ type 'a sourced = { thing : 'a; source : arg_source }
 
 type meta_file = Absent | Present of string | Generate of string
 
-type project = {
+type 'a project = {
   project_file  : string option;
   makefile : string option;
   native_compiler : native_compiler option;
@@ -34,6 +34,8 @@ type project = {
   q_includes  : (path * logic_path) sourced list;
   extra_args : string sourced list;
   defs : (string * string) sourced list;
+
+  extra_data : 'a;
 }
 and logic_path = string
 and path = { path : string; canonical_path : string }
@@ -43,7 +45,7 @@ and native_compiler =
 | NativeOndemand
 
 (* TODO generate with PPX *)
-let mk_project project_file makefile native_compiler = {
+let mk_project project_file makefile native_compiler extra_data = {
   project_file;
   makefile;
   native_compiler;
@@ -57,6 +59,8 @@ let mk_project project_file makefile native_compiler = {
   q_includes = [];
   extra_args = [];
   defs = [];
+
+  extra_data;
 }
 
 (********************* utils ********************************************)
@@ -205,7 +209,7 @@ let expand_paths project =
       (List.sort (fun a b -> String.compare a.thing b.thing) !exp) @ rv)
     [] project.files
 
-let process_cmd_line ~warning_fn orig_dir proj args =
+let process_cmd_line ~warning_fn orig_dir parse_extra proj args =
   let parsing_project_file = ref (proj.project_file <> None) in
   let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in
   let orig_dir = (* avoids turning foo.v in ./foo.v *)
@@ -269,6 +273,10 @@ let process_cmd_line ~warning_fn orig_dir proj args =
     aux { proj with defs = proj.defs @ [sourced (v,def)] } r
   | "-arg" :: a :: r ->
     aux { proj with extra_args = proj.extra_args @ List.map sourced (process_extra_args a) } r
+  | f :: r when CString.is_prefix "-" f -> begin match parse_extra f r proj.extra_data with
+      | None -> raise (Parsing_error ("Unknown option " ^ f))
+      | Some (r,extra_data) -> aux { proj with extra_data } r
+    end
   | f :: r ->
       let abs_f = CUnix.correct_path f orig_dir in
       let ext = Filename.extension abs_f in
@@ -318,12 +326,12 @@ let process_cmd_line ~warning_fn orig_dir proj args =
 
  (******************************* API ************************************)
 
-let cmdline_args_to_project ~warning_fn ~curdir args =
-  process_cmd_line ~warning_fn curdir (mk_project None None None) args
+let cmdline_args_to_project ~warning_fn ~curdir ~parse_extra extra args =
+  process_cmd_line ~warning_fn curdir parse_extra (mk_project None None None extra) args
 
 let read_project_file ~warning_fn f =
-  process_cmd_line ~warning_fn (Filename.dirname f)
-    (mk_project (Some f) None None) (parse f)
+  process_cmd_line ~warning_fn (Filename.dirname f) (fun _ _ () -> None)
+    (mk_project (Some f) None None ()) (parse f)
 
 let rec find_project_file ~from ~projfile_name =
   let fname = Filename.concat from projfile_name in

diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
@@ -16,7 +16,7 @@ type 'a sourced = { thing : 'a; source : arg_source }
 
 type meta_file = Absent | Present of string | Generate of string
 
-type project = {
+type 'a project = {
   project_file  : string option;
   makefile : string option;
   native_compiler : native_compiler option;
@@ -33,6 +33,8 @@ type project = {
   q_includes  : (path * logic_path) sourced list;
   extra_args : string sourced list;
   defs : (string * string) sourced list;
+
+  extra_data : 'a;
 }
 and logic_path = string
 and path = { path : string; canonical_path : string }
@@ -41,21 +43,24 @@ and native_compiler =
 | NativeNo
 | NativeOndemand
 
-val cmdline_args_to_project : warning_fn:(string -> unit) -> curdir:string -> string list -> project
+val cmdline_args_to_project
+  : warning_fn:(string -> unit) -> curdir:string
+  -> parse_extra:(string -> string list -> 'a -> (string list * 'a) option)
+  -> 'a -> string list -> 'a project
 
 exception UnableToOpenProjectFile of string
 
-val read_project_file : warning_fn:(string -> unit) -> string -> project
+val read_project_file : warning_fn:(string -> unit) -> string -> unit project
 (** [read_project_file warning_fn file] parses [file] as a Coq project;
     use [warning_fn] for deprecate options;
     raise [Parsing_error] on illegal options or arguments;
     raise [UnableToOpenProjectFile msg] if the file could not be opened;
     fails on some illegal non-project-file options *)
 
-val coqtop_args_from_project : project -> string list
+val coqtop_args_from_project : _ project -> string list
 val find_project_file : from:string -> projfile_name:string -> string option
 
-val all_files : project -> string sourced list
+val all_files : _ project -> string sourced list
 val files_by_suffix : string sourced list -> string list -> string sourced list
 
 val map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list

diff --git a/test-suite/unit-tests/lib/coqProject.ml b/test-suite/unit-tests/lib/coqProject.ml
@@ -16,7 +16,7 @@ let t () =
   (fun (project_file_path, project_file_channel) ->
     output_string project_file_channel project_file_contents;
     flush project_file_channel;
-    let expected : project = {
+    let expected : unit project = {
       project_file = Some project_file_path;
       makefile = None;
       native_compiler = None;
@@ -31,6 +31,8 @@ let t () =
       q_includes = [];
       extra_args = [];
       defs = [];
+
+      extra_data = ();
     } in
     assert_equal expected (read_project_file ~warning_fn project_file_path)
   ) ()
@@ -42,7 +44,7 @@ let t () =
   (fun (project_file_path, project_file_channel) ->
     output_string project_file_channel project_file_contents;
     flush project_file_channel;
-    let expected : project = {
+    let expected : unit project = {
       project_file = Some project_file_path;
       makefile = None;
       native_compiler = None;
@@ -57,6 +59,8 @@ let t () =
       q_includes = [];
       extra_args = List.map sourced_file ["-w"; "default"; "-w"; "foo"; "-set"; "Default Goal Selector=!"];
       defs = [];
+
+      extra_data = ();
     } in
     assert_equal expected (read_project_file ~warning_fn project_file_path)
   ) ()

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
@@ -15,17 +15,18 @@ open Printf
 
 let (>) f g = fun x -> g (f x)
 
-let usage_coq_makefile () =
-  output_string stderr "Usage summary:\
+let usage_coq_makefile ~ok =
+  let out = if ok then stdout else stderr in
+  output_string out "Usage summary:\
 \n\
 \ncoq_makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}]\
 \n  ... [-I dir] ... [-R physicalpath logicalpath]\
 \n  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
 \n  ... [-arg opt] ... [-docroot path] [-f file] [-o file]\
 \n  ... [-generate-meta-for-package project-name]\
-\n  [-h] [--help]\
+\n  [-h] [--help] [-v] [--version]\
 \n";
-  output_string stderr "\
+  output_string out "\
 \nFull list of options:\
 \n\
 \n[file.v]: Coq file to be compiled\
@@ -48,8 +49,11 @@ let usage_coq_makefile () =
 \n	Output file outside the current directory is forbidden.\
 \n[-generate-meta-for-package project-name]: generate META.project-name.\
 \n[-h]: print this usage summary\
-\n[--help]: equivalent to [-h]\n";
-  exit 1
+\n[--help]: equivalent to [-h]\
+\n[-v]: print version information\
+\n[--version]: equivalent to [-v]\
+\n";
+  exit (if ok then 0 else 1)
 
 let is_prefix dir1 dir2 =
   let l1 = String.length dir1 in
@@ -373,6 +377,23 @@ let chop_prefix p f =
   let len_f = String.length f in
   String.sub f len_p (len_f - len_p)
 
+type extra_opts = {
+  only_destination : string option;
+  only_sources : bool;
+}
+
+let empty_extra = {
+  only_destination = None;
+  only_sources = false;
+}
+
+let parse_extra f r opts = match f, r with
+  | "-destination-of", tgt :: r -> Some (r, { opts with only_destination = Some tgt })
+  | "-sources-of", r -> Some (r, { opts with only_sources = true })
+  | ("-h"|"--help"), _ -> usage_coq_makefile ~ok:true
+  | ("-v"|"--version"), _ -> Boot.Usage.version (); exit 0
+  | _ -> None
+
 let destination_of { ml_includes; q_includes; r_includes; } file =
   let file_dir = CUnix.canonical_path_name (Filename.dirname file) in
   let includes = q_includes @ r_includes in
@@ -413,19 +434,10 @@ let () =
     let prog = List.hd args in
     prog, List.tl args in
 
-  let only_destination, args = match args with
-    | "-destination-of" :: tgt :: rest -> Some tgt, rest
-    | _ -> None, args in
-
-  (* -sources-of and -destination-of must be the first parameter *)
-  let only_sources, args = match args with
-    | "-sources-of" :: rest -> true, rest
-    | _ -> false, args in
-
-  let project =
+  let { extra_data = { only_destination; only_sources } } as project =
     let warning_fn x = Format.eprintf "%s@\n%!" x in
-    try cmdline_args_to_project ~warning_fn ~curdir:Filename.current_dir_name args
-    with Parsing_error s -> prerr_endline s; usage_coq_makefile () in
+    try cmdline_args_to_project ~warning_fn ~curdir:Filename.current_dir_name ~parse_extra empty_extra args
+    with Parsing_error s -> prerr_endline s; usage_coq_makefile ~ok:false in
 
   if only_destination <> None then begin
     destination_of project (Option.get only_destination);