diff --git a/src/driver/whyconf.ml b/src/driver/whyconf.ml
index 6acd32a306d4f5591429ead819ba66d5a0842afe..05fa399bd028903e37fa5bf319f96ef13e07d690 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 b86696683e315f06abaf6e9b8fdd1c74d1f49b92..19fde288e5da648417c06479e21d67359c5a910a 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 c829b398fe28ebc2d1d0f60bdd76f60da6c3b10a..482684de975d12f23a4850de7480c594b45064b1 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 3fff85ca1103a3bdbd8dd2d706cdc2c54ddda1fa..ecb36cdb697405eb702d1d8b88652a293d5ec650 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 883764b30929097a5a03bcfaeed0b120cd42ee07..263a8f975aedfcd3c2864d1f53e5d31a9ccc63df 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),
- "<dir> Add <dir> 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),
- "<file> Read configuration from <file>";
- "--config", Arg.String (fun s -> opt_config := Some s),
- " same as -C";
- "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
- "<file> Read additional configuration from <file>";
"-F", Arg.String (fun s -> opt_parser := Some s),
- "<format> Select input format (default: \"why\")";
+ "<format> 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),
- "<f> add file f to the project (ignored if it is already there)") ;
+ "<file> 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] [<file.why>|<project directory> [<file.why> ...]]"
+ "Usage: %s [options] [<file.why>|<project directory>]..."
(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 0e1690cd8d42df5a64b5138182f1ce7dcb400792..e0043d8d466ec4eeec6d2ea8e13467b460a5dc13 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 3b96c949aef29179eaf71e41706d2f17fe04d629..8b26a8d8e0e3d1036b7d2886d5284686e0942ad6 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 268f09456cf73c1f7f3dc2f5788b463587c96938..b84bd6b6e9a3f4ae411313cbfee13e579fb8eea3 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 <driver> -o <dir> [[file|-] [-T <theory>]...]..."
+ "Usage: %s [options] -D <driver> -o <dir> [[file|-] [-T <theory>]...]..."
(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 62bb11fd6053ff5d3f8ae8031bc3c3989808a246..a2dbfcccbd10b329621d59b4161b8b3491f8f69d 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 <theory> [-G <goal>]...]...]..."
+ "Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
(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 6fe8c226cab196766707452dac47097396a499e8..419b22020935e53f0bd201bf12e5d2ce5f62408c 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 <driver> -o <dir> -T <theory> ..."
+ "Usage: %s [options] -D <driver> -o <dir> -T <theory> ..."
(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 2f70fbc4c576e3a02e80147c6c9bf19434e66210..429fab0ea11d32e737747e9b45880dc787cb2486 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] [<file.why>|<project directory>]"
+ "Usage: %s [options] [<file.why>|<project directory>]"
(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 5d6eb91499f6cc98ef6ad76d96a4d7556808aa69..bdb0a8f85849c1febd33df50db9aefa58202fead 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 fa1bcbb8c486809b664ab5ab711a56b908f306f3..a47c6314adcbbd6a3761997481cee02b1ebb67df 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, "<flag> Set a debug flag")
+ ("--debug", Arg.String add_flag, "<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 aad5ffae9bb320dcfc98a33a9cb784e81dc11cda..30f8a4bae86a0c8408bd39cd610c22e541004fb6 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), *)
(* "<dir> set the data directory ($WHY3DATA)"; *)
"-C", Arg.String (set_oref conf_file),
- "<file> Config file to create";
+ "<file> 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)]),
- "<id><file> Add a new prover executable";
+ "<id><file> 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,
- "<file> Install a plugin to the actual libdir";
+ "<file> 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 567d6780cc4e04633d1c2a8bd4d1fe4c93162121..0be76caa5099c9591a372c2e2f3e117d2a1825bb 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),
- "<dir> Add <dir> to the library search path";
"-o", Arg.String (fun s -> opt_output := Some s),
- "<dir> Print files in <dir>";
+ "<dir> print files in <dir>";
"--output", Arg.String (fun s -> opt_output := Some s),
" same as -o";
"--stdlib-url", Arg.String Doc_def.set_stdlib_url,
- "<url> Add links to <url> for files found on loadpath";
+ "<url> add links to <url> 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),
- " <title> 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 d1b0087b2c69a24bf9769812ce7b4938d0da0ab5..69cc5a459531b97bcea774cd6ae0eff0e68fe792 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 8eb70b689aa8d27063ec38f723f4bec73e29fbcf..2c6224a2f04bd8c676975c1d1dbc16a93d07dc73 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 278baf49d9baec688a1f76594aed03d6c6f9217c..173664304b554e94724d265d84508fa66ebbbe9f 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 ea0ca9e7676d185e16b38e55f4d77358e3493dc3..4f4b745bc9c447292f99db9d8c7c1f074c2d9feb 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 20999a29495d528f2a2d116bf2332d9b478ab43d..eaf9d17b3e2cf29487959e46a5027609e91e1244 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 bd234ee4e0d8d2c23005dd8848d4652d569ba415..3bbdc259068b74548685a906d1f63016f35ac9a0 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 aa3c0ea27751b40aa923935e878470a6e707767b..bb9902bd7195917ac79480af6ff16079a3b58242 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 140feef24e091b8132e2e847c6bb1a021ea2d165..ebb23f29e14604e883ff64afe9e9752220c59208 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 ce48049d907e0f3482b1e265111f235521bd6577..87fc9bd7e5b0dc591cda278482cfc5f6a63670f9 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 aa0f56fb6737f4765059f00acb8ef8109b05ab0f..1a57dc73656760e4f3a12cd1464412b2d1473e13 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 90df4cde496569bf8f66eb845a4a65c2aa8ae3c1..c9c814a89289d8700375d9817060ec04b778af8e 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;
}