Commit e245c1e9 authored by François Bobot's avatar François Bobot

why3config : simpler messages during prover detection

parent f206aa74
......@@ -38,14 +38,19 @@ let autoprovers = ref false
let autoplugins = ref false
let opt_version = ref false
let opt_list_flags = ref false
let opt_debug_all = ref false
let save = ref true
let set_oref r = (fun s -> r := Some s)
let plugins = Queue.create ()
let add_plugin x = Queue.add x plugins
let opt_debug = ref []
let add_opt_debug x = opt_debug := x::!opt_debug
let option_list = Arg.align [
(* "--libdir", Arg.String (set_oref libdir), *)
(* "<dir> set the lib directory ($WHY3LIB)"; *)
......@@ -64,6 +69,12 @@ let option_list = Arg.align [
" install a plugin to the actual libdir";
"--dont-save", Arg.Clear save,
" dont modify the config file";
"--list-debug-flags", Arg.Set opt_list_flags,
" List known debug flags";
"--debug-all", Arg.Set opt_debug_all,
" Set all debug flags (except parse_only and type_only)";
"--debug", Arg.String add_opt_debug,
"<flag> Set a debug flag";
"--version", Arg.Set opt_version,
" print version information"
]
......@@ -102,11 +113,34 @@ let plugins_auto_detection config =
set_main config main
let () =
(** Parse the command line *)
Arg.parse option_list anon_file usage_msg;
let opt_list = ref false in
if !opt_version then begin
printf "%s@." version_msg;
exit 0
opt_list := true;
printf "%s@." version_msg
end;
(** Debug flag *)
if !opt_debug_all then begin
List.iter (fun (_,f,_) -> Debug.set_flag f) (Debug.list_flags ());
Debug.unset_flag Typing.debug_parse_only;
Debug.unset_flag Typing.debug_type_only
end;
List.iter (fun s -> Debug.set_flag (Debug.lookup_flag s)) !opt_debug;
if !opt_list_flags then begin
opt_list := true;
let print fmt (p,_,_) = fprintf fmt "%s" p in
printf "@[<hov 2>Known debug flags:@\n%a@]@."
(Pp.print_list Pp.newline print)
(List.sort Pervasives.compare (Debug.list_flags ()))
end;
if !opt_list then exit 0;
(** Main *)
let config =
try read_config !conf_file
with Not_found ->
......
......@@ -22,6 +22,7 @@ open Util
open Whyconf
open Rc
let debug = Debug.register_flag "autodetect"
(* auto-detection of provers *)
......@@ -108,18 +109,18 @@ let sanitize_exec =
in
Ident.sanitizer first rest
let detect_prover main acc data =
let detect_prover main acc0 data =
let keys = Queue.create () in
let acc = List.fold_left
(fun acc com ->
let out = Filename.temp_file "out" "" in
let cmd = sprintf "%s %s" com data.version_switch in
let c = sprintf "(%s) > %s 2>&1" cmd out in
eprintf "Run : %s@." c;
Debug.dprintf debug "Run : %s@." c;
let ret = Sys.command c in
if ret <> 0 then
begin
eprintf "command '%s' failed@." cmd;
Debug.dprintf debug "command '%s' failed@." cmd;
acc
end
else
......@@ -169,15 +170,19 @@ let detect_prover main acc data =
eprintf "Answer was `%s'@." s;
acc
end)
acc
acc0
data.execs
in
if Queue.length keys = 1 then
let acc = if Queue.length keys = 1 then
let key = Queue.take keys in
let prv = Mstr.find key acc in
let acc = Mstr.remove key acc in
Mstr.add data.prover_id prv acc
else
acc in
(** If the accumulator has not been touched we warn
that we don't find the prover *)
if acc == acc0 then eprintf "Prover %s not found.@." data.prover_name;
acc
let run_auto_detection config =
......
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