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 <command>" as argv[0]
- remove "-version" options from everything but the main executable

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;

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

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 ())

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
 

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) =

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 *)
 

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 () =

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 () =

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

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 () =

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 () = *)

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
 

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 () =

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 ();

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;

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;
   }

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;
   }

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;
   }

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;