...
  View open merge request
Commits (8)
This diff is collapsed.
This diff is collapsed.
......@@ -9,6 +9,10 @@
(* *)
(********************************************************************)
val debug: Debug.flag
val info: Debug.flag
val is_config_command: bool ref
(** Lists prover family names from detection config *)
val list_prover_families : unit -> string list
......@@ -16,5 +20,13 @@ val list_prover_families : unit -> string list
val add_prover_binary :
Whyconf.config -> string -> string -> string -> Whyconf.config
type autodetection_result
(** Detect the provers *)
val run_auto_detection : Whyconf.config -> autodetection_result
(** Replace the provers by autodetected one *)
val run_auto_detection : Whyconf.config -> Whyconf.config
val generate_builtin_config : autodetection_result -> Whyconf.config -> Whyconf.config
(** Replace the output of provers with the current one *)
val generate_detected_config : autodetection_result -> Whyconf.detected_prover list
This diff is collapsed.
......@@ -40,7 +40,9 @@ val read_config : string option -> config
Windows) is checked for existence:
- if present, the content is parsed and returned,
- otherwise, we return the built-in default_config with a
default configuration filename. *)
default configuration filename.
*)
val merge_config : config -> string -> config
(** [merge_config config filename] merge the content of [filename]
......@@ -69,11 +71,19 @@ val get_main : config -> main
val set_main : config -> main -> config
(** [set_main config main] replace the main section by the given one *)
val set_stdlib: bool -> config -> config
(** Set if the standard library should be added to loadpath *)
val set_autoplugins: bool -> config -> config
(** Set if the plugins in the default path should be loaded *)
val set_autoprovers: bool -> config -> config
(** Set if the provers, strategies, ... must be created at startup *)
val libdir: main -> string
val datadir: main -> string
val loadpath: main -> string list
val set_loadpath : main -> string list -> main
val default_loadpath : string list
val timelimit: main -> int
val memlimit: main -> int
val running_provers_max: main -> int
......@@ -122,6 +132,7 @@ type config_prover = {
interactive : bool; (* Interactive theorem prover *)
extra_options: string list;
extra_drivers: string list;
added_at_startup : bool; (* added at startup or present in the user configuration *)
}
val get_complete_command : config_prover -> with_steps:bool -> string
......@@ -204,6 +215,15 @@ val get_strategies : config -> config_strategy Mstr.t
val add_strategy : config -> config_strategy -> config
(** detected provers *)
type detected_prover = {
exec_name : string;
output : string;
}
val set_detected_provers: config -> detected_prover list -> config
val get_detected_provers: config -> detected_prover list
(** filter prover *)
type filter_prover
......@@ -287,3 +307,11 @@ val unknown_to_known_provers :
config_prover Mprover.t -> prover ->
prover list * prover list * prover list
(** return others, same name, same version *)
(** */ *)
(** Internal, recursive functionality with Autodetection *)
val provers_from_detected_provers: (config -> config) ref
(** */ *)
......@@ -24,6 +24,7 @@ let usage_msg =
let conf_file = ref None
let autoprovers = ref false
let autoplugins = ref false
let provers_at_startup = ref true
let resetloadpath = ref false
(* When no arguments are given, activate the fallback to auto mode on error.
......@@ -62,7 +63,9 @@ let option_list = Arg.align [
[Arg.Set_string id;
Arg.Set_string shortcut;
Arg.String (fun name -> Queue.add (!id, !shortcut, name) prover_bins)]),
"<id> <shortcut> <file> add a new prover executable";
"<id><shortcut><file> add a new prover executable";
"--no-builtin-provers-at-statup", Arg.Unit (fun () -> provers_at_startup := false; autoprovers := true),
" write in .why3.conf the parameter of the provers";
"--list-prover-families", Arg.Set opt_list_prover_families,
" list known prover families";
"--install-plugin", Arg.String add_plugin,
......@@ -105,25 +108,6 @@ let install_plugin main p =
if p <> target then Sysutil.copy_file p target;
Whyconf.add_plugin main (Filename.chop_extension target)
let plugins_auto_detection config =
let main = get_main config in
let main = set_plugins main [] in
let dir = Whyconf.pluginsdir main in
let main =
if Sys.file_exists dir then
let files = Sys.readdir dir in
let fold main p =
if p.[0] == '.' then main else
let p = Filename.concat dir p in
try
install_plugin main p
with Exit -> main
in
Array.fold_left fold main files
else main
in
set_main config main
(* Activate the fallback to auto mode on error *)
let auto_fallback () =
if auto_fb then begin
......@@ -136,6 +120,7 @@ let main () =
Arg.parse option_list anon_file usage_msg;
let opt_list = ref false in
Autodetection.is_config_command := true;
(* Debug flag *)
Debug.Args.set_flags_selected ();
......@@ -176,17 +161,27 @@ let main () =
auto_fallback ();
let config =
if !resetloadpath then
set_main config (set_loadpath (get_main config) default_loadpath)
(** temporary 13/06/18 after introduction of --no-stdlib *)
set_main config (set_loadpath (get_main config) [])
else config
in
let config =
if !autoprovers
then Autodetection.run_auto_detection config
then
let config = Whyconf.set_provers config Mprover.empty in
let config = Whyconf.set_autoprovers !provers_at_startup config in
let env = Autodetection.run_auto_detection config in
if !provers_at_startup then
let detected_provers = Autodetection.generate_detected_config env in
Whyconf.set_detected_provers config detected_provers
else
Autodetection.generate_builtin_config env config
else config
in
let config =
if !autoplugins
then plugins_auto_detection config
if !autoplugins then
(** temporary 13/06/18 after introduction of --no-auto-plugins *)
set_main config (set_plugins (get_main config) [])
else config
in
if !save then begin
......
......@@ -17,7 +17,7 @@ type rc_value =
| RCint of int
| RCbool of bool
| RCfloat of float
| RCstring of string
| RCstring of string * bool (** escape eol *)
| RCident of string
(* exception SyntaxError *)
......@@ -154,10 +154,11 @@ val get_stringl : ?default:string list -> section -> string -> string list
val get_stringo : section -> string -> string option
val set_string : ?default:string -> section -> string -> string -> section
(** Same as {!set_int} but on string *)
val set_string : ?escape_eol:bool -> ?default:string -> section -> string -> string -> section
(** Same as {!set_int} but on string. [escape_eol] indicates if special
character should be escaped *)
val set_stringl : ?default:string list ->
val set_stringl : ?escape_eol:bool -> ?default:string list ->
section -> string -> string list -> section
(** Same as {!set_intl} but on string *)
......
......@@ -25,7 +25,7 @@ type rc_value =
| RCint of int
| RCbool of bool
| RCfloat of float
| RCstring of string
| RCstring of string * bool
| RCident of string
......@@ -84,7 +84,10 @@ let print_rc_value fmt = function
| RCint i -> fprintf fmt "%d" i
| RCbool b -> fprintf fmt "%B" b
| RCfloat f -> fprintf fmt "%f" f
| RCstring s -> fprintf fmt "\"%s\"" (escape_string s)
| RCstring (s,false) ->
fprintf fmt "\"%s\"" (escape_string s)
| RCstring (s,true) ->
fprintf fmt "\"%s\"" (String.escaped s)
| RCident s -> fprintf fmt "%s" s
let () = Exn_printer.register (fun fmt e -> match e with
......@@ -246,10 +249,10 @@ let rbool k = function
let wbool b = RCbool b
let rstring k = function
| RCident s | RCstring s -> s
| RCident s | RCstring (s,_) -> s
| v -> raise (StringExpected (k,v))
let wstring s = RCstring s
let wstring ?(escape_eol=false) s = RCstring (s,escape_eol)
let get_int = get_value rint
let get_intl = get_valuel rint
......@@ -267,8 +270,8 @@ let set_booll = set_valuel wbool
let get_string = get_value rstring
let get_stringl = get_valuel rstring
let get_stringo = get_valueo rstring
let set_string = set_value wstring
let set_stringl = set_valuel wstring
let set_string ?escape_eol ?default s = set_value (wstring ?escape_eol) ?default s
let set_stringl ?escape_eol ?default s = set_valuel (wstring ?escape_eol) ?default s
let check_exhaustive section keyl =
let test k _ = if Sstr.mem k keyl then ()
......@@ -340,7 +343,7 @@ and value key = parse
record lexbuf }
| '"'
{ Buffer.clear buf;
string_val key lexbuf }
string_val key false lexbuf }
| "true"
{ push_field key (RCbool true);
record lexbuf }
......@@ -355,24 +358,24 @@ and value key = parse
| _ as c
{ syntax_error ("invalid value starting with " ^ String.make 1 c) }
and string_val key = parse
and string_val key escape_eol = parse
| '"'
{ push_field key (RCstring (Buffer.contents buf));
{ push_field key (RCstring (Buffer.contents buf,escape_eol));
record lexbuf
}
| [^ '\\' '"'] as c
{ Buffer.add_char buf c;
string_val key lexbuf }
string_val key escape_eol lexbuf }
| '\\' (['\\' '"' 'n' 'r' 't'] as c)
{ Buffer.add_char buf
(match c with 'n' -> '\n' | 'r' -> '\r' | 't' -> '\t' | _ -> c);
string_val key lexbuf }
string_val key (escape_eol || c = 'n') lexbuf }
| '\\' '\n'
{ string_val key lexbuf }
{ string_val key escape_eol lexbuf }
| '\\' (_ as c)
{ Buffer.add_char buf '\\';
Buffer.add_char buf c;
string_val key lexbuf }
string_val key escape_eol lexbuf }
| eof
{ syntax_error "unterminated string" }
......