Commit 395e8644 authored by Francois Bobot's avatar Francois Bobot

Whyconf centralize all the configuration (temporary solution)

parent b6641c8d
......@@ -42,11 +42,9 @@ let debug =
let config = Whyconf.read_config None
let timelimit = match config.timelimit with
| None -> 3
| Some t -> t
let timelimit = config.main.timelimit
let env = Env.create_env (Lexer.retrieve config.loadpath)
let env = Env.create_env (Lexer.retrieve config.main.loadpath)
let provers = Hashtbl.create 17
......
......@@ -42,42 +42,15 @@ let error ?loc e = match loc with
(* lib and shared dirs *)
(* are we executed with an implicit path or not ?
cmd -> yes (dirname = ".", is_implicit = yes)
/... -> no (dirname = "/...", is_implicit = no)
./t -> no (dirname = ".", is_implicit = no)
bin/t -> no (dirname = "bin", is_implicit = yes)
*)
(*
let implicit_path =
let s = Sys.argv.(0) in
Filename.is_implicit s &&
Filename.dirname s = Filename.current_dir_name
*)
let libdir =
(*
if implicit_path then
*)
try
Sys.getenv "WHY3LIB"
with Not_found -> Config.libdir
(*
else "."
*)
let datadir =
(*
if implicit_path then
*)
try
Sys.getenv "WHY3DATA"
with Not_found -> Config.datadir
(*
else "share"
*)
......@@ -130,19 +103,56 @@ type config_prover = {
name : string; (* "Alt-Ergo v2.95 (special)" *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
version : string; (* "v2.95" *)
editor : string;
}
type main = {
loadpath : string list; (* "/usr/local/share/why/theories" *)
timelimit : int;
memlimit : int;
running_provers_max : int;
}
type ide = {
window_width : int;
window_height : int;
tree_width : int;
task_height : int;
verbose : int;
default_editor : string;
}
type config = {
conf_file : string; (* "/home/innocent_user/.why.conf" *)
(*
loadpath : string list; (* "/usr/local/share/why/theories" *)
*)
timelimit : int option; (* default prover time limit in seconds *)
memlimit : int option; (* default prover memory limit in megabytes *)
running_provers_max : int option; (* max number of running prover processes *)
provers : config_prover Mstr.t; (* indexed by short identifiers *)
provers : config_prover Mstr.t; (* indexed by short identifiers *)
main : main;
ide : ide;
}
let default_main = {
loadpath = [Filename.concat Config.why_libdir "theories"];
timelimit = 10;
memlimit = 0;
running_provers_max = 2;
}
let default_ide =
{ window_width = 1024;
window_height = 768;
tree_width = 512;
task_height = 384;
verbose = 0;
default_editor = "";
}
let default_config =
{ conf_file = Filename.concat (Rc.get_home_dir ()) ".why.conf";
provers = Mstr.empty;
main = default_main;
ide = default_ide;
}
let to_string key = function
| Rc.RCstring s -> s
| v -> error (StringExpected (key,v))
......@@ -181,20 +191,24 @@ let load_prover dirname al =
let nam = ref None in
let cmd = ref None in
let drv = ref None in
let version = ref None in
let editor = ref "" in
let load (key, value) = match key with
| "name" -> set_string key nam value
| "command" -> set_string key cmd value
| "driver" -> set_string key drv value;
| "driver" -> set_string key drv value;
drv := option_map (absolute_filename dirname) !drv
| _ -> ()
(*
error (UnknownField key)
*)
| "version" -> set_string key version value
| "editor" -> editor := Rc.string value
| _ -> error (UnknownField key)
in
List.iter load al;
{ name = get_field "name" !nam;
command = get_field "command" !cmd;
driver = get_field "driver" !drv }
driver = get_field "driver" !drv;
version = get_field "version" !version;
editor = !editor;
}
let load_main dirname main al =
let lp = ref [] in
......@@ -207,20 +221,42 @@ let load_main dirname main al =
| "timelimit" -> set_int key tl value
| "memlimit" -> set_int key ml value
| "running_provers_max" -> set_int key rp value
| _ -> ()
(*
error (UnknownField key)
*)
| _ -> () (*error (UnknownField key)*)
in
List.iter load al;
{ main with
(*
loadpath = List.rev !lp;
*)
timelimit = !tl;
memlimit = !ml;
running_provers_max = !rp;
provers = Mstr.empty }
(* let none_if_null d = function None -> d | Some 0 -> None | v -> v in *)
{ loadpath = List.rev !lp;
timelimit = default_option main.timelimit !tl;
memlimit = default_option main.memlimit !ml;
running_provers_max = default_option main.running_provers_max !rp
}
let load_ide ide al =
let width = ref None in
let height = ref None in
let tree_width = ref None in
let task_height = ref None in
let verbose = ref None in
let default_editor = ref None in
let load (key, value) = match key with
| "window_width" -> set_int key width value
| "window_height" -> set_int key height value
| "tree_width" -> set_int key tree_width value
| "task_height" -> set_int key task_height value
| "verbose" -> set_int key verbose value
| "default_editor" -> set_string key default_editor value
| _ -> error (UnknownField key)
in
List.iter load al;
{ window_height = default_option ide.window_height !height;
window_width = default_option ide.window_width !width;
tree_width = default_option ide.tree_width !tree_width;
task_height = default_option ide.task_height !task_height;
verbose = default_option ide.verbose !verbose;
default_editor = default_option ide.default_editor !default_editor;
}
let read_config conf_file =
let filename = match conf_file with
......@@ -229,31 +265,29 @@ let read_config conf_file =
if Sys.file_exists "why.conf" then "why.conf" else
if Sys.file_exists ".why.conf" then ".why.conf" else
let f = Filename.concat (Rc.get_home_dir ()) ".why.conf" in
if Sys.file_exists f then f else
Filename.concat Config.libdir "why.conf"
if Sys.file_exists f then f else raise Not_found
end
in
let dirname = Filename.dirname filename in
let rc = try Rc.from_file filename with
| Failure "lexing" -> error SyntaxError
in
let main = ref {
conf_file = filename;
(*
loadpath = [];
*)
timelimit = None;
memlimit = None;
running_provers_max = None;
provers = Mstr.empty }
in
let provers = ref Mstr.empty in
let main = ref default_main in
let have_main = ref false in
let ide = ref default_ide in
let have_ide = ref false in
let load (key, al) = match key with
| "main" :: rest ->
if rest <> [] then error (ExtraParameters "main");
if !have_main then error (DuplicateSection "main");
main := load_main dirname !main al
| ["main"] when not !have_main ->
main := load_main dirname !main al;
have_main := true
| ["main"] when !have_main -> error (DuplicateSection "main")
| "main" :: _ -> error (ExtraParameters "main");
| ["ide"] when not !have_ide ->
ide := load_ide !ide al;
have_ide := true
| ["ide"] when !have_ide -> error (DuplicateSection "ide")
| "ide" :: _ -> error (ExtraParameters "ide");
| "prover" :: name :: rest ->
if rest <> [] then error (ExtraParameters ("prover " ^ name));
if Mstr.mem name !provers then error (DuplicateProver name);
......@@ -263,25 +297,196 @@ let read_config conf_file =
| [] -> assert false
in
List.iter load rc;
{ !main with provers = !provers }
{ conf_file = filename;
provers = !provers;
main = !main;
ide = !ide}
let read_config conf_file =
try read_config conf_file with Not_found -> default_config
let save_config config =
let ch = open_out config.conf_file in
let fmt = Format.formatter_of_out_channel ch in
fprintf fmt "[main]@\n";
(*
List.iter (fprintf fmt "library = \"%s\"@\n") config.loadpath;
*)
Util.option_iter (fprintf fmt "timelimit = %d@\n") config.timelimit;
Util.option_iter (fprintf fmt "memlimit = %d@\n") config.memlimit;
Util.option_iter (fprintf fmt "running_provers_max = %d@\n") config.running_provers_max;
List.iter (fprintf fmt "library = \"%s\"@\n") config.main.loadpath;
fprintf fmt "timelimit = %d@\n"
config.main.timelimit;
fprintf fmt "memlimit = %d@\n"
config.main.memlimit;
fprintf fmt "running_provers_max = %d@\n"
config.main.running_provers_max;
fprintf fmt "@.";
fprintf fmt "[ide]@\n";
fprintf fmt "window_width = %d@\n" config.ide.window_width;
fprintf fmt "window_height = %d@\n" config.ide.window_height;
fprintf fmt "tree_width = %d@\n" config.ide.tree_width;
fprintf fmt "task_height = %d@\n" config.ide.task_height;
fprintf fmt "verbose = %d@\n" config.ide.verbose;
fprintf fmt "default_editor = \"%s\"@\n" config.ide.default_editor;
fprintf fmt "@.";
let print_prover name prover =
fprintf fmt "[prover %s]@\n" name;
fprintf fmt "name = \"%s\"@\n" prover.name;
fprintf fmt "command = \"%s\"@\n" prover.command;
fprintf fmt "driver = \"%s\"@\n@." prover.driver;
fprintf fmt "version = \"%s\"@\n@." prover.version;
fprintf fmt "editor = \"%s\"@\n@." prover.editor;
in
Mstr.iter print_prover config.provers;
close_out ch
(* auto-detection of provers *)
type prover_kind = ATP | ITP
type prover_autodetection_data =
{ kind : prover_kind;
prover_id : string;
mutable prover_name : string;
mutable execs : string list;
mutable version_switch : string;
mutable version_regexp : string;
mutable versions_ok : string list;
mutable versions_old : string list;
mutable prover_command : string;
mutable prover_driver : string;
mutable prover_editor : string;
}
let default k id =
{ kind = k;
prover_id = id;
prover_name = "";
execs = [];
version_switch = "";
version_regexp = "";
versions_ok = [];
versions_old = [];
prover_command = "";
prover_driver = "";
prover_editor = "";
}
let load_prover d (key, value) =
match key with
| "name" -> d.prover_name <- Rc.string value
| "exec" -> d.execs <- Rc.string value :: d.execs
| "version_switch" -> d.version_switch <- Rc.string value
| "version_regexp" -> d.version_regexp <- Rc.string value
| "version_ok" -> d.versions_ok <- Rc.string value :: d.versions_ok
| "version_old" -> d.versions_old <- Rc.string value :: d.versions_old
| "command" -> d.prover_command <- Rc.string value
| "driver" -> d.prover_driver <- Rc.string value
| "editor" -> d.prover_editor <- Rc.string value
| s ->
eprintf "unknown key [%s] in autodetection data@." s;
exit 1
let load acc (key,l) =
match key with
| ["ATP" ; id] ->
let d = default ATP id in
List.iter (load_prover d) l;
d :: acc
| ["ITP" ; id] ->
let d = default ITP id in
List.iter (load_prover d) l;
d :: acc
| s :: _ ->
eprintf "unknown section [%s] in auto detection data@." s;
exit 1
| [] -> assert false
let read_auto_detection_data () =
try
let rc = Rc.from_file "prover-detection-data.conf" in
List.fold_left load [] rc
with
| Failure "lexing" ->
eprintf "Syntax error in prover-detection-data.conf@.";
exit 2
| Not_found ->
eprintf "prover-detection-data.conf not found@.";
exit 2
let provers_found = ref 0
let prover_tips_info = ref false
let make_command exec com =
let cmd_regexp = Str.regexp "%\\(.\\)" in
let replace s = match Str.matched_group 1 s with
| "e" -> exec
| c -> "%"^c
in
Str.global_substitute cmd_regexp replace com
let detect_prover acc data =
List.fold_left
(fun acc com ->
let out = Filename.temp_file "out" "" in
let cmd = com ^ " " ^ data.version_switch in
let c = cmd ^ " > " ^ out in
let ret = Sys.command c in
if ret <> 0 then
begin
eprintf "command '%s' failed@." cmd;
acc
end
else
let s =
try
let ch = open_in out in
let s = ref (input_line ch) in
while !s = "" do s := input_line ch done;
close_in ch;
Sys.remove out;
!s
with Not_found | End_of_file -> ""
in
let re = Str.regexp data.version_regexp in
if Str.string_match re s 0 then
let nam = data.prover_name in
let ver = Str.matched_group 1 s in
if List.mem ver data.versions_ok then
eprintf "Found prover %s version %s, OK.@." nam ver
else
begin
prover_tips_info := true;
if List.mem ver data.versions_old then
eprintf "Warning: prover %s version %s is quite old, please \
consider upgrading to a newer version.@."
nam ver
else
eprintf "Warning: prover %s version %s is not known to be \
supported, use it at your own risk!@." nam ver
end;
incr provers_found;
let c = make_command com data.prover_command in
Mstr.add data.prover_id
{name = data.prover_name;
version = ver;
command = c;
driver = Filename.concat Config.why_libdir data.prover_driver;
editor = data.prover_editor} acc
else
begin
prover_tips_info := true;
eprintf "Warning: found prover %s but name/version not \
recognized by regexp `%s'@."
data.prover_name data.version_regexp;
eprintf "Answer was `%s'@." s;
acc
end)
acc
data.execs
let run_auto_detection config =
let l = read_auto_detection_data () in
let detect = List.fold_left detect_prover Mstr.empty l in
let length = Mstr.fold (fun _ _ i -> i+1) detect 0 in
eprintf "%d provers detected.@." length;
{config with provers = detect}
......@@ -21,26 +21,44 @@
open Util
val libdir : string
val datadir : string
val sharedir : string (* For image, ... *)
type config_prover = {
name : string; (* "Alt-Ergo v2.95 (special)" *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
version : string; (* "v2.95" *)
editor : string; (* Interative theorem prover *)
}
type main = {
loadpath : string list; (* "/usr/local/share/why/theories" *)
timelimit : int; (* default prover time limit in seconds
(0 unlimited) *)
memlimit : int;
(* default prover memory limit in megabytes (0 unlimited)*)
running_provers_max : int;
(* max number of running prover processes *)
}
type ide = {
window_width : int;
window_height : int;
tree_width : int;
task_height : int;
verbose : int;
default_editor : string;
}
type config = {
conf_file : string; (* "/home/innocent_user/.why.conf" *)
(*
loadpath : string list; (* "/usr/local/share/why/theories" *)
*)
timelimit : int option; (* default prover time limit in seconds *)
memlimit : int option; (* default prover memory limit in megabytes *)
running_provers_max : int option; (* max number of running prover processes *)
provers : config_prover Mstr.t; (* indexed by short identifiers *)
main : main;
ide : ide;
}
val default_config : config
(** if conf_file is not given, tries the following:
"$WHY_CONFIG"; "./why.conf"; "./.why.conf";
"$HOME/.why.conf"; "$USERPROFILE/.why.conf" *)
......@@ -48,4 +66,5 @@ val read_config : string option -> config
val save_config : config -> unit
(** Replace the provers by autodetected one *)
val run_auto_detection : config -> config
open Format
open Why
open Util
open Whyconf
type prover_data =
{ prover_id : string;
......@@ -12,58 +14,22 @@ type prover_data =
mutable editor : string;
}
type t =
type t =
{ mutable window_width : int;
mutable window_height : int;
mutable tree_width : int;
mutable task_height : int;
mutable time_limit : int;
mutable mem_limit : int;
mutable verbose : int;
mutable max_running_processes : int;
mutable provers : prover_data list;
mutable default_editor : string;
env : Env.env;
mutable config : Whyconf.config;
}
let default =
{ window_width = 1024;
window_height = 768;
tree_width = 512;
task_height = 384;
time_limit = 2;
verbose = 0;
max_running_processes = 2;
provers = [];
default_editor = "";
}
let conf_file = Filename.concat (Rc.get_home_dir ()) ".why.conf"
let save_prover fmt p =
fprintf fmt "[prover %s]@\n" p.prover_id;
fprintf fmt "name = \"%s\"@\n" p.prover_name;
fprintf fmt "version = \"%s\"@\n" p.prover_version;
fprintf fmt "command = \"%s\"@\n" p.command;
fprintf fmt "driver = \"%s\"@\n" p.driver_name;
if p.editor <> "" then fprintf fmt "editor = \"%s\"@\n" p.editor;
fprintf fmt "@."
let save_config config =
let ch = open_out conf_file in
let fmt = formatter_of_out_channel ch in
fprintf fmt "[main]@\n";
fprintf fmt "width = %d@\n" config.window_width;
fprintf fmt "height = %d@\n" config.window_height;
fprintf fmt "tree_width = %d@\n" config.tree_width;
fprintf fmt "task_height = %d@\n" config.task_height;
fprintf fmt "time_limit = %d@\n" config.time_limit;
fprintf fmt "verbose = %d@\n" config.verbose;
fprintf fmt "max_processes = %d@\n" config.max_running_processes;
fprintf fmt "default_editor = \"%s\"@\n" config.default_editor;
fprintf fmt "@.";
List.iter (save_prover fmt) config.provers;
close_out ch
let load_main c (key, value) =
let load_main c (key, value) =
match key with
| "width" -> c.window_width <- Rc.int value
| "height" -> c.window_height <- Rc.int value
......@@ -73,79 +39,78 @@ let load_main c (key, value) =
| "verbose" -> c.verbose <- Rc.int value
| "max_processes" -> c.max_running_processes <- Rc.int value
| "default_editor" -> c.default_editor <- Rc.string value
| s ->
| s ->
eprintf "Warning: ignore unknown key [%s] in whyide config file@." s
let get_prover_data env id name ver c d e =
let f = Filename.concat Whyconf.datadir d in
let get_prover_data env id pr acc =
try
let dr = Driver.load_driver env f in
let dr = Driver.load_driver env pr.Whyconf.driver in
{ prover_id = id ;
prover_name = name;
prover_version = ver;
command = c;
driver_name = d;
driver = dr;
editor = e;
}
with
| Loc.Located(p,e) ->
eprintf "Syntax error %a in driver %s for prover %s (%s).@\nprover disabled@."
Loc.report_position p f name (Printexc.to_string e);
Printexc.print_backtrace stdout;
raise Not_found
prover_name = pr.Whyconf.name;
prover_version = pr.Whyconf.version;
command = pr.Whyconf.command;
driver_name = pr.Whyconf.driver;
driver = dr;
editor = pr.Whyconf.editor;
}::acc
with _e ->
eprintf "Failed to load driver %s for prover %s. prover disabled@."
pr.Whyconf.driver pr.Whyconf.name;
acc
| e ->
eprintf "Failed to load driver %s for prover %s (%s).@\nprover disabled@."
f name (Printexc.to_string e);
Printexc.print_backtrace stdout;
raise Not_found
let load_config config =
let env = Env.create_env (Lexer.retrieve config.main.loadpath) in
{ window_height = config.ide.Whyconf.window_height;
window_width = config.ide.Whyconf.window_width;