Commit 8ebe2032 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

main: use Args for common options

Also:
- don't count "" and "contraption" as available commands
- pass every option except the command name to the command
- provide an option for extended help message
parent 03277cb2
......@@ -14,33 +14,55 @@ open Why3
let opt_config = ref None
let opt_extra = ref []
let opt_loadpath = ref []
let opt_help = ref false
let common_options = [
let common_options_head = [
"-C", Arg.String (fun s -> opt_config := Some s),
"<file> Read configuration from <file>";
"<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>";
"<file> read additional configuration from <file>";
"-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
"<dir> Add <dir> to the library search path";
"<dir> add <dir> to the library search path";
"--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
" same as -L";
Debug.Args.desc_debug_list;
Debug.Args.desc_debug;
Debug.Args.desc_debug_all;
Debug.Args.desc_debug ]
Debug.Args.desc_debug_list;
]
let common_options_tail = [
"-h", Arg.Set opt_help,
" print this list of options";
"-help", Arg.Set opt_help,
"";
"--help", Arg.Set opt_help,
" same as -h";
]
let align_options options =
Arg.align (common_options_head @ options @ common_options_tail)
let initialize ?(extra_help=Format.pp_print_newline) options default usage =
let options = align_options options in
Arg.parse options default usage;
if !opt_help then begin
Format.printf "@[%s%a@]" (Arg.usage_string options usage) extra_help ();
exit 0
end;
let initialize options default usage =
Arg.parse (Arg.align (List.append options common_options)) default usage;
if Debug.Args.option_list () then exit 0;
let config = Whyconf.read_config !opt_config in
let config = List.fold_left Whyconf.merge_config config !opt_extra in
let main = Whyconf.get_main config in
Whyconf.load_plugins main;
Debug.Args.set_flags_selected ();
if Debug.Args.option_list () then exit 0;
let lp = List.rev_append !opt_loadpath (Whyconf.loadpath main) in
(Env.create_env lp, config)
let exit_with_usage options usage =
Arg.usage (Arg.align (List.append options common_options)) usage;
Arg.usage (align_options options) usage;
exit 1
......@@ -11,7 +11,9 @@
open Why3
val initialize : (string * Arg.spec * string) list ->
val initialize :
?extra_help : (Format.formatter -> unit -> unit) ->
(string * Arg.spec * string) list ->
(string -> unit) -> string -> Env.env * Whyconf.config
val exit_with_usage : (string * Arg.spec * string) list -> string -> 'a
......@@ -18,130 +18,84 @@ let usage_msg = sprintf
"Usage: %s [options] <command> [options]"
(Filename.basename Sys.argv.(0))
let version_msg = sprintf "Why3 platform, version %s (build date: %s)"
Config.version Config.builddate
let opt_config = ref None
let opt_extra = ref []
let opt_loadpath = ref []
let opt_print_libdir = ref false
let opt_print_datadir = ref false
let opt_list_transforms = ref false
let opt_list_printers = ref false
let opt_list_provers = ref false
let opt_list_formats = ref false
let opt_list_metas = ref false
let opt_version = ref false
let opt_help = ref false
let option_list = Arg.align [
"-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>";
"-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
"<dir> Add <dir> to the library search path";
"--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
" same as -L";
let option_list = [
"--list-transforms", Arg.Set opt_list_transforms,
" List known transformations";
" list known transformations";
"--list-printers", Arg.Set opt_list_printers,
" List known printers";
" list known printers";
"--list-provers", Arg.Set opt_list_provers,
" List known provers";
" list known provers";
"--list-formats", Arg.Set opt_list_formats,
" List known input formats";
" list known input formats";
"--list-metas", Arg.Set opt_list_metas,
" List known metas";
Debug.Args.desc_debug_list;
Debug.Args.desc_debug_all;
Debug.Args.desc_debug;
"--print-libdir", Arg.Set opt_print_libdir,
" Print location of binary components (plugins, etc)";
"--print-datadir", Arg.Set opt_print_datadir,
" Print location of non-binary data (theories, modules, etc)";
"--version", Arg.Set opt_version,
" Print version information";
"--help", Arg.Set opt_help, " Display this list of options";
"-help", Arg.Set opt_help, " Display this list of options" ]
let command_path =
match Config.localdir with
" list known metas";
"--print-libdir",
Arg.Unit (fun _ -> printf "%s@." Config.libdir; exit 0),
" print location of binary components (plugins, etc)";
"--print-datadir",
Arg.Unit (fun _ -> printf "%s@." Config.datadir; exit 0),
" print location of non-binary data (theories, modules, etc)";
"--version",
Arg.Unit (fun _ -> printf "Why3 platform, version %s (build date: %s)@."
Config.version Config.builddate; exit 0),
" print version information";
]
let command_path = match Config.localdir with
| Some p -> Filename.concat p "bin"
| None -> Filename.concat Config.libdir "commands"
let extra_help fmt commands =
fprintf fmt "@\nAvailable commands:@.";
List.iter (fun (v,_) -> fprintf fmt " %s@." v) commands
let available_commands () =
let commands = Sys.readdir command_path in
Array.sort String.compare commands;
let re = Str.regexp "^why3\\([^.]*\\)\\([.].*\\)?" in
let re = Str.regexp "^why3\\([^.]+\\)\\([.].*\\)?" in
let commands = Array.fold_left (fun acc v ->
if Str.string_match re v 0 then
let w = Str.matched_group 1 v in
match acc with
| _ when w = "contraption" -> acc
| (h,_)::_ when h = w -> acc
| _ -> (w, v) :: acc
else acc) [] commands in
List.rev commands
let command sscmd =
let (scmd,cmd) =
let cmd =
let scmd = "why3" ^ sscmd in
let cmd = Filename.concat command_path scmd in
if Sys.file_exists cmd then (scmd, cmd)
if cmd <> "" && cmd <> "contraption" && Sys.file_exists cmd
then cmd
else begin
let commands = available_commands () in
let scmd =
try List.assoc sscmd commands
with Not_found ->
eprintf "'%s' is not a why3 command.@\n@\nAvailable commands:@." cmd;
List.iter (fun (v,_) -> eprintf " %s@." v) commands;
exit 1 in
let cmd = Filename.concat command_path scmd in
(scmd, cmd)
try List.assoc sscmd commands
with Not_found ->
eprintf "'%s' is not a Why3 command.@\n%a"
sscmd extra_help commands;
exit 1 in
Filename.concat command_path scmd
end in
let args = ref [] in
(match !opt_config with Some v -> args := v :: "-C" :: !args | None -> ());
List.iter (fun v -> args := v :: "-L" :: !args) (List.rev !opt_loadpath);
for i = !Arg.current + 1 to Array.length Sys.argv - 1 do
args := Sys.argv.(i) :: !args;
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 (scmd :: List.rev !args))
Unix.execv cmd (Array.of_list (sscmd :: List.rev !args))
let () = try
Arg.parse option_list command usage_msg;
if !opt_version then begin
printf "%s@." version_msg;
exit 0
end;
if !opt_help then begin
printf "%s@\nAvailable commands:@." (Arg.usage_string option_list usage_msg);
List.iter (fun (v,_) -> printf " %s@." v) (available_commands ());
exit 0
end;
if !opt_print_libdir then begin
printf "%s@." Config.libdir;
exit 0
end;
if !opt_print_datadir then begin
printf "%s@." Config.datadir;
exit 0
end;
(** Configuration *)
let config = read_config !opt_config in
let config = List.fold_left merge_config config !opt_extra in
let main = get_main config in
Whyconf.load_plugins main;
Debug.Args.set_flags_selected ();
let extra_help fmt () = extra_help fmt (available_commands ()) in
let _, config = Args.initialize ~extra_help option_list command usage_msg in
(** listings*)
(** listings *)
let sort_pair (x,_) (y,_) = String.compare x y in
let opt_list = ref false in
......@@ -196,11 +150,9 @@ let () = try
printf "@[<hov 2>Known metas:@\n%a@]@\n@."
(Pp.print_list Pp.newline2 print) (List.sort cmp (Theory.list_metas ()))
end;
opt_list := Debug.Args.option_list () || !opt_list;
if !opt_list then exit 0;
printf "%s@\n@\nAvailable commands:@." usage_msg;
List.iter (fun (v,_) -> printf " %s@." v) (available_commands ())
printf "@[%s%a@]" usage_msg extra_help ()
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment