From 241961df4fcb51baa4cb7c54e60ea48108fdeb0f Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Fri, 11 Jul 2014 17:12:28 +0200 Subject: [PATCH] use Whyconf.Args in why3ide and why3doc - make Whyconf.Args.initialize return the base config file, too. This is needed when we change configuration and want to save it. - make Main pass "why3 " as argv[0] - remove "-version" options from everything but the main executable --- src/driver/whyconf.ml | 6 +-- src/driver/whyconf.mli | 2 +- src/ide/gconfig.ml | 23 ++------- src/ide/gconfig.mli | 4 +- src/ide/gmain.ml | 71 +++++++-------------------- src/tools/main.ml | 5 +- src/tools/why3execute.ml | 4 +- src/tools/why3extract.ml | 4 +- src/tools/why3prove.ml | 4 +- src/tools/why3realize.ml | 4 +- src/tools/why3replay.ml | 4 +- src/tools/why3wc.mll | 3 +- src/util/debug.ml | 6 +-- src/why3config/why3config.ml | 27 +++------- src/why3doc/doc_main.ml | 27 ++++------ src/why3session/why3session_copy.ml | 6 +-- src/why3session/why3session_csv.ml | 12 ++--- src/why3session/why3session_html.ml | 6 +-- src/why3session/why3session_info.ml | 8 +-- src/why3session/why3session_latex.ml | 4 +- src/why3session/why3session_lib.ml | 18 ++----- src/why3session/why3session_lib.mli | 4 -- src/why3session/why3session_main.ml | 30 ++++++----- src/why3session/why3session_output.ml | 6 +-- src/why3session/why3session_rm.ml | 4 +- src/why3session/why3session_run.ml | 2 +- 26 files changed, 107 insertions(+), 187 deletions(-) diff --git a/src/driver/whyconf.ml b/src/driver/whyconf.ml index 6acd32a30..05fa399bd 100644 --- a/src/driver/whyconf.ml +++ b/src/driver/whyconf.ml @@ -786,14 +786,14 @@ module Args = struct Format.printf "@[%s%a@]" (Arg.usage_string options usage) extra_help (); exit 0 end; - let config = read_config !opt_config in - let config = List.fold_left merge_config config !opt_extra in + let base_config = read_config !opt_config in + let config = List.fold_left merge_config base_config !opt_extra in let main = get_main config in load_plugins main; Debug.Args.set_flags_selected (); if Debug.Args.option_list () then exit 0; let lp = List.rev_append !opt_loadpath (loadpath main) in - config, Env.create_env lp + config, base_config, Env.create_env lp let exit_with_usage options usage = Arg.usage (align_options options) usage; diff --git a/src/driver/whyconf.mli b/src/driver/whyconf.mli index b86696683..19fde288e 100644 --- a/src/driver/whyconf.mli +++ b/src/driver/whyconf.mli @@ -239,7 +239,7 @@ module Args : sig ?extra_help : (Format.formatter -> unit -> unit) -> (string * Arg.spec * string) list -> (string -> unit) -> string -> - config * Env.env + config * config * Env.env val exit_with_usage : (string * Arg.spec * string) list -> string -> 'a end diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml index c829b398f..482684de9 100644 --- a/src/ide/gconfig.ml +++ b/src/ide/gconfig.ml @@ -9,8 +9,6 @@ (* *) (********************************************************************) -open Format - open Why3 open Rc open Whyconf @@ -202,7 +200,7 @@ let load_altern alterns (_,section) = Mprover.add unknown known alterns *) -let load_config config original_config = +let load_config config original_config env = let main = get_main config in let ide = match Whyconf.get_section config "ide" with | None -> default_ide @@ -211,8 +209,6 @@ let load_config config original_config = (* let alterns = *) (* List.fold_left load_altern *) (* Mprover.empty (get_family config "alternative_prover") in *) - (* temporary sets env to empty *) - let env = Env.create_env [] in set_labels_flag ide.ide_show_labels; set_locs_flag ide.ide_show_locs; { window_height = ide.ide_window_height; @@ -307,25 +303,14 @@ let save_config t = let config = Whyconf.set_section config "ide" ide in Whyconf.save_config config -let read_config conf_file extra_files = - try - let config = Whyconf.read_config conf_file in - let merged_config = List.fold_left Whyconf.merge_config config extra_files in - load_config merged_config config - with e when not (Debug.test_flag Debug.stack_trace) -> - eprintf "@.%a@." Exn_printer.exn_printer e; - exit 1 - -let config,read_config = +let config,load_config = let config = ref None in (fun () -> match !config with | None -> invalid_arg "configuration not yet loaded" | Some conf -> conf), - (fun conf_file extra_files -> - (*Debug.dprintf debug "[Info] reading config file...@?";*) - let c = read_config conf_file extra_files in - (*Debug.dprintf debug " done.@.";*) + (fun conf base_conf env -> + let c = load_config conf base_conf env in config := Some c) let save_config () = save_config (config ()) diff --git a/src/ide/gconfig.mli b/src/ide/gconfig.mli index 3fff85ca1..ecb36cdb6 100644 --- a/src/ide/gconfig.mli +++ b/src/ide/gconfig.mli @@ -40,8 +40,8 @@ type t = mutable session_nb_processes : int; } -val read_config : string option -> string list -> unit -(** None use the default config *) +val load_config : Whyconf.config -> Whyconf.config -> Why3.Env.env -> unit +(** [load_config config original_config env] creates and saves IDE config *) val init : unit -> unit diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index 883764b30..263a8f975 100644 --- a/src/ide/gmain.ml +++ b/src/ide/gmain.ml @@ -39,54 +39,35 @@ let debug = Debug.lookup_flag "ide_info" (* parsing command line *) (************************) -let includes = ref [] let files = Queue.create () let opt_parser = ref None -let opt_config = ref None -let opt_extra = ref [] let spec = Arg.align [ - ("-L", - Arg.String (fun s -> includes := s :: !includes), - " Add to the library search path") ; - "--library", - Arg.String (fun s -> includes := s :: !includes), - " same as -L" ; - "-C", Arg.String (fun s -> opt_config := Some s), - " Read configuration from "; - "--config", Arg.String (fun s -> opt_config := Some s), - " same as -C"; - "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]), - " Read additional configuration from "; "-F", Arg.String (fun s -> opt_parser := Some s), - " Select input format (default: \"why\")"; + " select input format (default: \"why\")"; "--format", Arg.String (fun s -> opt_parser := Some s), " same as -F"; (* - ("-f", + "-f", Arg.String (fun s -> input_files := s :: !input_files), - " add file f to the project (ignored if it is already there)") ; + " add file to the project (ignored if it is already there)"; *) - Debug.Args.desc_debug_list; - Debug.Args.desc_debug_all; - Debug.Args.desc_debug ] let usage_str = sprintf - "Usage: %s [options] [| [ ...]]" + "Usage: %s [options] [|]..." (Filename.basename Sys.argv.(0)) -let () = Arg.parse spec (fun f -> Queue.add f files) usage_str +let gconfig = try + let config, base_config, env = + Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str in + if Queue.is_empty files then Whyconf.Args.exit_with_usage spec usage_str; + Gconfig.load_config config base_config env; + Gconfig.config () -let () = Gconfig.read_config !opt_config !opt_extra - -let () = C.load_plugins (Gconfig.get_main ()) - -let () = - Debug.Args.set_flags_selected (); - if Debug.Args.option_list () then exit 0 - -let () = if Queue.is_empty files then begin Arg.usage spec usage_str; exit 1 end + with e when not (Debug.test_flag Debug.stack_trace) -> + eprintf "%a@." Exn_printer.exn_printer e; + exit 1 let () = Debug.dprintf debug "[Info] Init the GTK interface...@?"; @@ -115,9 +96,7 @@ let (why_lang, any_lang) = | Some _ as l -> l in (why_lang, any_lang) - - -(* Borrowed from Frama-C src/gui/source_manager.ml: +(* Borrowed from Frama-C src/gui/source_manager.ml: Try to convert a source file either as UTF-8 or as locale. *) let try_convert s = try @@ -142,22 +121,6 @@ let source_text fname = with e when not (Debug.test_flag Debug.stack_trace) -> "Error while opening or reading file '" ^ fname ^ "':\n" ^ (Printexc.to_string e) -(********************************) -(* loading WhyIDE configuration *) -(********************************) - -let loadpath = (C.loadpath (Gconfig.get_main ())) @ List.rev !includes - -let gconfig = - let c = Gconfig.config () in - c.env <- Env.create_env loadpath; -(* - let provers = C.get_provers c.Gconfig.config in - c.provers <- - Util.Mstr.fold (Session.get_prover_data c.env) provers Util.Mstr.empty; -*) - c - (***************) (* Main window *) (***************) @@ -637,7 +600,7 @@ module MA = struct let notify_timer_state = let c = ref 0 in fun t s r -> - reset_gc (); + reset_gc (); incr c; monitor_waiting#set_text ("Waiting: " ^ (string_of_int t)); monitor_scheduled#set_text ("Scheduled: " ^ (string_of_int s)); @@ -1636,7 +1599,7 @@ let evaluate_window () = files_map (0, []) in let (_store, column) = - GTree.store_of_list Gobject.Data.string file_names + GTree.store_of_list Gobject.Data.string file_names in files_combo#set_text_column column; let ( _ : GtkSignal.id) = files_combo#connect#changed @@ -1889,7 +1852,7 @@ let reload () = current_file := ""; (** create a new environnement (in order to reload the files which are "use") *) - gconfig.env <- Env.create_env loadpath; + gconfig.env <- Env.create_env (Env.get_loadpath gconfig.env); (** reload the session *) let old_session = (env_session()).S.session in let new_env_session,(_:bool),(_:bool) = diff --git a/src/tools/main.ml b/src/tools/main.ml index 0e1690cd8..e0043d8d4 100644 --- a/src/tools/main.ml +++ b/src/tools/main.ml @@ -89,11 +89,12 @@ let command sscmd = for i = 1 to Array.length Sys.argv - 1 do if i <> !Arg.current then args := Sys.argv.(i) :: !args; done; - Unix.execv cmd (Array.of_list (sscmd :: List.rev !args)) + let scmd = "why3 " ^ sscmd in + Unix.execv cmd (Array.of_list (scmd :: List.rev !args)) let () = try let extra_help fmt () = extra_help fmt (available_commands ()) in - let config,_ = Args.initialize ~extra_help option_list command usage_msg in + let config,_,_ = Args.initialize ~extra_help option_list command usage_msg in (** listings *) diff --git a/src/tools/why3execute.ml b/src/tools/why3execute.ml index 3b96c949a..8b26a8d8e 100644 --- a/src/tools/why3execute.ml +++ b/src/tools/why3execute.ml @@ -14,7 +14,7 @@ open Why3 open Stdlib let usage_msg = sprintf - "Usage: why3 %s [options] file module.ident..." + "Usage: %s [options] file module.ident..." (Filename.basename Sys.argv.(0)) let opt_file = ref None @@ -37,7 +37,7 @@ let option_list = [ "--format", Arg.String (fun s -> opt_parser := Some s), " same as -F" ] -let config, env = +let config, _, env = Whyconf.Args.initialize option_list add_opt usage_msg let () = diff --git a/src/tools/why3extract.ml b/src/tools/why3extract.ml index 268f09456..b84bd6b6e 100644 --- a/src/tools/why3extract.ml +++ b/src/tools/why3extract.ml @@ -15,7 +15,7 @@ open Stdlib open Theory let usage_msg = sprintf - "Usage: why3 %s [options] -D -o [[file|-] [-T ]...]..." + "Usage: %s [options] -D -o [[file|-] [-T ]...]..." (Filename.basename Sys.argv.(0)) let opt_queue = Queue.create () @@ -71,7 +71,7 @@ let option_list = [ "--output", Arg.String (fun s -> opt_output := Some s), " same as -o" ] -let config, env = +let config, _, env = Whyconf.Args.initialize option_list add_opt_file usage_msg let () = diff --git a/src/tools/why3prove.ml b/src/tools/why3prove.ml index 62bb11fd6..a2dbfcccb 100644 --- a/src/tools/why3prove.ml +++ b/src/tools/why3prove.ml @@ -18,7 +18,7 @@ open Task open Driver let usage_msg = sprintf - "Usage: why3 %s [options] [[file|-] [-T [-G ]...]...]..." + "Usage: %s [options] [[file|-] [-T [-G ]...]...]..." (Filename.basename Sys.argv.(0)) let opt_queue = Queue.create () @@ -144,7 +144,7 @@ let option_list = [ Debug.Args.desc_shortcut "type_only" "--type-only" " stop after type checking" ] -let config, env = +let config, _, env = Whyconf.Args.initialize option_list add_opt_file usage_msg let () = try diff --git a/src/tools/why3realize.ml b/src/tools/why3realize.ml index 6fe8c226c..419b22020 100644 --- a/src/tools/why3realize.ml +++ b/src/tools/why3realize.ml @@ -13,7 +13,7 @@ open Format open Why3 let usage_msg = sprintf - "Usage: why3 %s [options] -D -o -T ..." + "Usage: %s [options] -D -o -T ..." (Filename.basename Sys.argv.(0)) let opt_queue = Queue.create () @@ -60,7 +60,7 @@ let option_list = [ "--output", Arg.String (fun s -> opt_output := Some s), " same as -o" ] -let config, env = +let config, _, env = Whyconf.Args.initialize option_list add_opt_file usage_msg let () = diff --git a/src/tools/why3replay.ml b/src/tools/why3replay.ml index 2f70fbc4c..429fab0ea 100644 --- a/src/tools/why3replay.ml +++ b/src/tools/why3replay.ml @@ -62,7 +62,7 @@ let set_opt_smoke = function | _ -> assert false let usage_msg = Format.sprintf - "Usage: why3 %s [options] [|]" + "Usage: %s [options] [|]" (Filename.basename Sys.argv.(0)) let option_list = [ @@ -104,7 +104,7 @@ let add_opt_file f = match !opt_file with | None -> opt_file := Some f -let config, env = +let config, _, env = Whyconf.Args.initialize option_list add_opt_file usage_msg (* let () = *) diff --git a/src/tools/why3wc.mll b/src/tools/why3wc.mll index 5d6eb9149..bdb0a8f85 100644 --- a/src/tools/why3wc.mll +++ b/src/tools/why3wc.mll @@ -323,11 +323,12 @@ and skip_until_nl = parse end; Queue.add file files - let usage = "why3 wc [options] files...\n\ + let usage = Format.sprintf "Usage: %s [options] files...\n\ \n\ Counts tokens/lines in Why3 source files.\n\ Assumes source files to be lexically well-formed.\n\ If no source file is given, standard input is analyzed.\n" + (Filename.basename Sys.argv.(0)) let () = Arg.parse spec add_file usage diff --git a/src/util/debug.ml b/src/util/debug.ml index fa1bcbb8c..a47c6314a 100644 --- a/src/util/debug.ml +++ b/src/util/debug.ml @@ -98,7 +98,7 @@ module Args = struct let opt_list_flags = ref false in let desc = "--list-debug-flags", Arg.Set opt_list_flags, - " List known debug flags" in + " list known debug flags" in let list () = if !opt_list_flags then begin let list = @@ -127,14 +127,14 @@ module Args = struct (option, Arg.Unit set_flag, desc) let desc_debug = - ("--debug", Arg.String add_flag, " Set a debug flag") + ("--debug", Arg.String add_flag, " set a debug flag") let opt_debug_all = ref false let desc_debug_all = let desc_debug = Pp.sprintf - " Set all debug flags that do not change Why3 behaviour" in + " set all debug flags that do not change Why3 behaviour" in ("--debug-all", Arg.Set opt_debug_all, desc_debug) let set_flags_selected () = diff --git a/src/why3config/why3config.ml b/src/why3config/why3config.ml index aad5ffae9..30f8a4bae 100644 --- a/src/why3config/why3config.ml +++ b/src/why3config/why3config.ml @@ -19,16 +19,11 @@ let usage_msg = can be set to change the default paths.@." (Filename.basename Sys.argv.(0)) -let version_msg = sprintf - "Why3 configuration utility, version %s (build date: %s)" - Config.version Config.builddate - (* let libdir = ref None *) (* let datadir = ref None *) let conf_file = ref None let autoprovers = ref false let autoplugins = ref false -let opt_version = ref false let opt_list_prover_ids = ref false @@ -47,31 +42,29 @@ let option_list = Arg.align [ (* "--datadir", Arg.String (set_oref datadir), *) (* " set the data directory ($WHY3DATA)"; *) "-C", Arg.String (set_oref conf_file), - " Config file to create"; + " config file to create"; "--config", Arg.String (set_oref conf_file), " same as -C"; "--detect-provers", Arg.Set autoprovers, - " Search for provers in $PATH"; + " search for provers in $PATH"; "--detect-plugins", Arg.Set autoplugins, - " Search for plugins in the default library directory"; + " search for plugins in the default library directory"; "--detect", Arg.Unit (fun () -> autoprovers := true; autoplugins := true), - " Search for both provers and plugins"; + " search for both provers and plugins"; "--add-prover", Arg.Tuple (let id = ref "" in [Arg.Set_string id; Arg.String (fun name -> Queue.add (!id, name) prover_bins)]), - " Add a new prover executable"; + " add a new prover executable"; "--list-prover-ids", Arg.Set opt_list_prover_ids, - " List known prover families"; + " list known prover families"; "--install-plugin", Arg.String add_plugin, - " Install a plugin to the actual libdir"; + " install a plugin to the actual libdir"; "--dont-save", Arg.Clear save, - " Do not modify the config file"; + " do not modify the config file"; Debug.Args.desc_debug_list; Debug.Args.desc_debug_all; Debug.Args.desc_debug; - "--version", Arg.Set opt_version, - " Print version information" ] let anon_file _ = Arg.usage option_list usage_msg; exit 1 @@ -125,10 +118,6 @@ let main () = Arg.parse option_list anon_file usage_msg; let opt_list = ref false in - if !opt_version then begin - opt_list := true; - printf "%s@." version_msg - end; (** Debug flag *) Debug.Args.set_flags_selected (); diff --git a/src/why3doc/doc_main.ml b/src/why3doc/doc_main.ml index 567d6780c..0be76caa5 100644 --- a/src/why3doc/doc_main.ml +++ b/src/why3doc/doc_main.ml @@ -20,7 +20,6 @@ let usage_msg = sprintf "Usage: %s [options...] [files...]" (Filename.basename Sys.argv.(0)) -let opt_loadpath = ref [] let opt_output = ref None let opt_index = ref None (* default behavior *) let opt_title = ref None @@ -28,33 +27,25 @@ let opt_body = ref false let opt_queue = Queue.create () let option_list = Arg.align [ - "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath), - " Add to the library search path"; "-o", Arg.String (fun s -> opt_output := Some s), - " Print files in "; + " print files in "; "--output", Arg.String (fun s -> opt_output := Some s), " same as -o"; "--stdlib-url", Arg.String Doc_def.set_stdlib_url, - " Add links to for files found on loadpath"; + " add links to for files found on loadpath"; "--index", Arg.Unit (fun () -> opt_index := Some true), - " generates an index file index.html"; + " generate an index file index.html"; "--no-index", Arg.Unit (fun () -> opt_index := Some false), " do not generate an index file index.html"; "--title", Arg.String (fun s -> opt_title := Some s), - " Set a title for the index page"; + " <title> set a title for the index page"; "--body-only", Arg.Set opt_body, - " Only produce the body of the HTML document"; + " only produce the body of the HTML document"; ] -let add_opt_file x = Queue.add x opt_queue - -let () = - Arg.parse option_list add_opt_file usage_msg; - let config = Whyconf.read_config None in - let main = Whyconf.get_main config in - opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main); - (* Doc_def.set_loadpath !opt_loadpath; *) - Doc_def.set_output_dir !opt_output +let _,_,env = + Whyconf.Args.initialize option_list + (fun x -> Queue.add x opt_queue) usage_msg let index = match !opt_index with | Some b -> b @@ -96,7 +87,7 @@ let print_file fname = let () = (* Queue.iter Doc_def.add_file opt_queue; *) try - let env = Env.create_env !opt_loadpath in + Doc_def.set_output_dir !opt_output; (* process files *) Queue.iter (do_file env) opt_queue; Queue.iter print_file opt_queue; diff --git a/src/why3session/why3session_copy.ml b/src/why3session/why3session_copy.ml index d1b0087b2..69cc5a459 100644 --- a/src/why3session/why3session_copy.ml +++ b/src/why3session/why3session_copy.ml @@ -189,7 +189,7 @@ but@ one@ is@ needed.@."; let cmd_copy = { cmd_spec = spec; - cmd_desc = "copy proof based on a filter."; + cmd_desc = "copy proof based on a filter"; cmd_name = "copy"; cmd_run = run ~action:Copy; } @@ -197,7 +197,7 @@ let cmd_copy = let cmd_archive = { cmd_spec = spec; - cmd_desc = "same as copy but archive the source."; + cmd_desc = "same as copy but archive the source"; cmd_name = "copy-archive"; cmd_run = run ~action:CopyArchive; } @@ -205,7 +205,7 @@ let cmd_archive = let cmd_mod = { cmd_spec = spec; - cmd_desc = "modify proof based on filter."; + cmd_desc = "modify proof based on filter"; cmd_name = "mod"; cmd_run = run ~action:Mod; } diff --git a/src/why3session/why3session_csv.ml b/src/why3session/why3session_csv.ml index 8eb70b689..2c6224a2f 100644 --- a/src/why3session/why3session_csv.ml +++ b/src/why3session/why3session_csv.ml @@ -75,23 +75,23 @@ let spec = opt_provers := (simple_read_opt_prover s)::!opt_provers), " select the provers"):: ("--data", Arg.Set opt_data, - "For all the goals give the time taken by each provers that proved it."):: + " for all the goals give the time taken by each provers that proved it"):: ("--aggregate", Arg.Set opt_aggregate, " aggregate all the input into one file named \ aggregate_data.* and aggregate.*"):: ("--value-not-valid", Arg.Set_string opt_value_not_valid, " value used when the external proof is not valid (only for --data)"):: ("--valid_by_time", Arg.Set opt_by_time, - "Give the evolution of the number of goal proved \ + " give the evolution of the number of goal proved \ for each provers (default)"):: ("--gnuplot", Arg.Symbol (["pdf";"png";"svg";"qt";"gp"],select_gnuplot), - "Run gnuplot on the produced file (currently only with --valid_by_time)\ + " run gnuplot on the produced file (currently only with --valid_by_time)\ (gp write the gnuplot script used for generating the other case)"):: ("--gnuplot-x", Arg.Symbol (["time";"goals"],select_gnuplot_x), - "Select the data used for the x axes time or number of goal proved \ + " select the data used for the x axes time or number of goal proved \ (default time)"):: ("--output-csv", Arg.Set opt_print_csv, - "print the csv, set byt default when --gnuplot is not set"):: + " print the csv, set by default when --gnuplot is not set"):: common_options (** Normal *) @@ -359,7 +359,7 @@ let run () = let cmd = { cmd_spec = spec; cmd_desc = - "output session as a table or graph for simple processing or viewing."; + "output session as a table or graph for simple processing or viewing"; cmd_name = "csv"; cmd_run = run; } diff --git a/src/why3session/why3session_html.ml b/src/why3session/why3session_html.ml index 278baf49d..173664304 100644 --- a/src/why3session/why3session_html.ml +++ b/src/why3session/why3session_html.ml @@ -48,7 +48,7 @@ let spec = Arg.Set_string output_dir, "<path> output directory ('-' for stdout)") :: ("--context", Arg.Set opt_context, - " adds context around the generated HTML code") :: + " add context around the generated HTML code") :: ("--style", Arg.Symbol (["simpletree";"jstree";"table"], set_opt_style), " style to use, defaults to '" ^ default_style ^ "'." ) :: @@ -56,7 +56,7 @@ let spec = [Arg.String set_opt_pp_in; Arg.String set_opt_pp_cmd; Arg.String set_opt_pp_out], - "<suffix> <cmd> <out_suffix> declares a pretty-printer for edited proofs") :: + "<suffix> <cmd> <out_suffix> declare a pretty-printer for edited proofs") :: ("--coqdoc", Arg.Unit (fun ()-> opt_pp := (".v",("coqdoc --no-index --html -o %o %i",".html"))::!opt_pp), @@ -555,7 +555,7 @@ let run () = let cmd = { cmd_spec = spec; - cmd_desc = "output session in HTML format."; + cmd_desc = "output session in HTML format"; cmd_name = "html"; cmd_run = run; } diff --git a/src/why3session/why3session_info.ml b/src/why3session/why3session_info.ml index ea0ca9e76..4f4b745bc 100644 --- a/src/why3session/why3session_info.ml +++ b/src/why3session/why3session_info.ml @@ -36,14 +36,14 @@ let spec = ("--edited-files", Arg.Set opt_print_edited, " edited proof scripts in the session" ) :: ("--stats", Arg.Set opt_stats_print, - " prints various proofs statistics" ) :: + " print various proofs statistics" ) :: ("--graph", Arg.Set opt_hist_print, - " outputs a graph of the total time needed for \ + " print a graph of the total time needed for \ proving a given number of goals for each provers" ) :: ("--tree", Arg.Set opt_tree_print, " session contents as a tree in textual format" ) :: ("--dir", Arg.Set opt_project_dir, - " prints the directory of the session" ) :: + " print the directory of the session" ) :: ("--print0", Arg.Set opt_print0, " use the null character instead of newline" ) :: common_options @@ -452,7 +452,7 @@ let run () = let cmd = { cmd_spec = spec; - cmd_desc = "print informations and statistics about a session."; + cmd_desc = "print informations and statistics about a session"; cmd_name = "info"; cmd_run = run; } diff --git a/src/why3session/why3session_latex.ml b/src/why3session/why3session_latex.ml index 20999a294..eaf9d17b3 100644 --- a/src/why3session/why3session_latex.ml +++ b/src/why3session/why3session_latex.ml @@ -32,7 +32,7 @@ let add_element s = let spec = ("-style", Arg.Set_int opt_style, - "<n> sets output style (1 or 2, default 1)") :: + "<n> set output style (1 or 2, default 1)") :: ("-o", Arg.Set_string opt_output_dir, "<dir> where to produce LaTeX files (default: session dir)") :: @@ -472,7 +472,7 @@ let run () = let cmd = { cmd_spec = spec; - cmd_desc = "output session in LaTeX format."; + cmd_desc = "output session in LaTeX format"; cmd_name = "latex"; cmd_run = run; } diff --git a/src/why3session/why3session_lib.ml b/src/why3session/why3session_lib.ml index bd234ee4e..3bbdc2590 100644 --- a/src/why3session/why3session_lib.ml +++ b/src/why3session/why3session_lib.ml @@ -31,37 +31,25 @@ let files = Queue.create () let iter_files f = Queue.iter f files let anon_fun (f:string) = Queue.add f files -let opt_version = ref false - -let print_version () = - Format.printf "Why3 session, version %s (build date: %s)@." - Config.version Config.builddate - let read_simple_spec () = - if !opt_version then begin - print_version (); exit 0 - end; Debug.Args.set_flags_selected (); Debug.Args.option_list () - - let opt_config = ref None let opt_loadpath = ref [] let opt_extra = ref [] let common_options = [ "-C", Arg.String (fun s -> opt_config := Some s), - "<file> reads configuration from <file>"; + "<file> read configuration from <file>"; "--config", Arg.String (fun s -> opt_config := Some s), "<file> same as -C"; "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]), - "<file> reads additional configuration from <file>"; + "<file> read additional configuration from <file>"; "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath), - "<dir> adds <dir> to the library search path"; + "<dir> add <dir> to the library search path"; "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath), "<dir> same as -L"; - "-v", Arg.Set opt_version, " prints version information" ; Debug.Args.desc_shortcut "verbose" "--verbose" "increase verbosity"; Debug.Args.desc_debug_list; Debug.Args.desc_debug_all; diff --git a/src/why3session/why3session_lib.mli b/src/why3session/why3session_lib.mli index aa3c0ea27..bb9902bd7 100644 --- a/src/why3session/why3session_lib.mli +++ b/src/why3session/why3session_lib.mli @@ -31,10 +31,6 @@ type cmd = val iter_files : (string -> unit) -> unit val anon_fun : Arg.anon_fun -(** print_version *) -val print_version : unit -> unit - - (** {2 Spec for version, debug} *) (* val simple_spec : spec_list *) diff --git a/src/why3session/why3session_main.ml b/src/why3session/why3session_main.ml index 140feef24..ebb23f29e 100644 --- a/src/why3session/why3session_main.ml +++ b/src/why3session/why3session_main.ml @@ -27,27 +27,32 @@ let cmds = Why3session_run.cmd; |] -let exec_name = Sys.argv.(0) +let exec_name = Filename.basename Sys.argv.(0) -let print_usage () = +let print_usage fmt () = let maxl = Array.fold_left (fun acc e -> max acc (String.length e.cmd_name)) 0 cmds in - eprintf "%s <command> [options] <session directories>@\n@\navailable commands:@.@[<hov>%a@]@\n@." + fprintf fmt "Usage: %s <command> [options] <session directories>@\n@\n\ + Available commands:@.@[<hov>%a@]@\n@." exec_name (Pp.print_iter1 Array.iter Pp.newline - (fun fmt e -> fprintf fmt "%s @[<hov>%s@]" + (fun fmt e -> fprintf fmt " %s @[<hov>%s@]" (Strings.pad_right ' ' e.cmd_name maxl) e.cmd_desc)) cmds; - Arg.usage (Arg.align Why3session_lib.common_options) "common options:"; - eprintf "@\nspecific command options: %s <command> -help@." exec_name; - exit 1 + let usage = Arg.usage_string + (Arg.align Why3session_lib.common_options) "Common options:" in + fprintf fmt "%s@\nSpecific command options: %s <command> --help@." + usage exec_name let () = - if Array.length Sys.argv < 2 then print_usage (); + if Array.length Sys.argv < 2 then begin + print_usage err_formatter (); + exit 1 + end; let cmd_name = Sys.argv.(1) in begin match cmd_name with - | "-h" | "--help" -> print_usage () - | "-v" | "--version" -> print_version (); exit 0 + | "-h" | "-help" | "--help" -> + print_usage std_formatter (); exit 0 | _ -> () end; let module M = struct exception Found of cmd end in @@ -57,11 +62,12 @@ let () = if e.cmd_name = cmd_name then raise (M.Found e)) cmds; eprintf "command %s unknown@." cmd_name; - print_usage () + print_usage err_formatter (); + exit 1 with M.Found cmd -> cmd in incr Arg.current; - let cmd_usage = sprintf "%s %s [options]:" Sys.argv.(0) cmd_name in + let cmd_usage = sprintf "Usage: %s %s [options]" exec_name cmd_name in Arg.parse (Arg.align cmd.cmd_spec) anon_fun cmd_usage; try cmd.cmd_run () diff --git a/src/why3session/why3session_output.ml b/src/why3session/why3session_output.ml index ce48049d9..87fc9bd7e 100644 --- a/src/why3session/why3session_output.ml +++ b/src/why3session/why3session_output.ml @@ -29,9 +29,9 @@ let opt_output_dir = ref None let spec = ["--output", Arg.String (fun s -> opt_output_dir := Some s), - " Set the directory where to output the files"; + " set the directory where to output the files"; "-o", Arg.String (fun s -> opt_output_dir := Some s), - " Same as --output" + " same as --output" ]@ (force_obsolete_spec @ filter_spec @ common_options) @@ -105,7 +105,7 @@ let run () = let cmd = { cmd_spec = spec; - cmd_desc = "output file send to the prover."; + cmd_desc = "output file send to the prover"; cmd_name = "output"; cmd_run = run; } diff --git a/src/why3session/why3session_rm.ml b/src/why3session/why3session_rm.ml index aa0f56fb6..1a57dc736 100644 --- a/src/why3session/why3session_rm.ml +++ b/src/why3session/why3session_rm.ml @@ -32,7 +32,7 @@ let spec = ("--clean", Arg.Unit (fun () -> set_remove Not_valid (); set_filter_verified_goal FT_Yes), - " Remove unsuccessful proof attempts \ + " remove unsuccessful proof attempts \ associated to proved goals (same as --filter-verified-goal --conservative)"):: ("--interactive", Arg.Unit (set_remove Interactive), " ask before replacing proof_attempt"):: @@ -80,7 +80,7 @@ let run () = let cmd = { cmd_spec = spec; - cmd_desc = "remove proof based on a filter."; + cmd_desc = "remove proof based on a filter"; cmd_name = "rm"; cmd_run = run; } diff --git a/src/why3session/why3session_run.ml b/src/why3session/why3session_run.ml index 90df4cde4..c9c814a89 100644 --- a/src/why3session/why3session_run.ml +++ b/src/why3session/why3session_run.ml @@ -358,7 +358,7 @@ let run () = let cmd = { cmd_spec = spec; - cmd_desc = "run the proof attempt that corresponds to the filter."; + cmd_desc = "run the proof attempt that corresponds to the filter"; cmd_name = "run"; cmd_run = run; } -- GitLab