Commit 48685ba9 authored by François Bobot's avatar François Bobot
Browse files

Autodetection: new semantic of provers-detection-data.conf

Don't use anymore the family argument.

1) For every block, for every executable call the prover using the
version switch and add the prover to the configuration if the version
match one of the version_ok or version_old but none of the version_bad
2) We consider that an executable name which appears in a block, but
which version isn't a version_ok, version_old or version_bad has an
unknown version
3) For every executable which have an unknown version, we add the
prover using the first block that contains it.

So the order of the block is used only when the version of an
executable appears in none of the block.

A block with more than one exec fields is now the same thing than if
you split the block into blocks containing one field.

New message field that allows to print a message when a prover is
detected. If a message is not present, we print ", Ok." if the version
is good (version_good) and not old, and " (it is an old version)." if
the version is old (version_old).

The field command can be missing in a block, in that case the block
defines a version known to be buggy: no prover config is generated.
parent 36d297f2
[ATP alt-ergo-model]
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.95-dev"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
version_ok = "0.95-dev"
version_bad = "0.94"
version_bad = "0.93.1"
version_bad = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
version_bad = "0.92.1"
version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timelimit %t -model %f"
driver = "drivers/alt_ergo_model.drv"
editor = "altgr-ergo"
......@@ -26,15 +16,6 @@ exec = "alt-ergo-0.94"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.94"
version_bad = "0.93.1"
version_bad = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
version_bad = "0.92.1"
version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/alt_ergo.drv"
editor = "altgr-ergo"
......@@ -48,13 +29,6 @@ version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.93.1"
version_ok = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
version_bad = "0.92.1"
version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/alt_ergo_0.93.drv"
......@@ -81,7 +55,7 @@ version_old = "0.8"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/alt_ergo_bare.drv"
[ATP cvc3-2.4]
[ATP cvc3]
name = "CVC3"
exec = "cvc3"
exec = "cvc3-2.4.1"
......@@ -90,21 +64,17 @@ version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
version_ok = "2.4.1"
version_old = "2.4"
version_bad = "2.2"
version_bad = "2.1"
# the -timeout option is unreliable in CVC3 2.4.1
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/cvc3.drv"
[ATP cvc3-2.2]
[ATP cvc3]
name = "CVC3"
exec = "cvc3"
exec = "cvc3-2.2"
exec = "cvc3-2.1"
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
version_bad = "2.4.1"
version_bad = "2.4"
version_ok = "2.2"
version_old = "2.1"
# we pass time 0 to why3-cpulimit to avoid race
......@@ -157,7 +127,7 @@ version_old = "0.11.2"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"
[ATP gappa016dev]
[ATP gappa]
name = "Gappa+dev"
exec = "gappa-0.16.0+dev"
version_switch = "--version"
......@@ -166,7 +136,7 @@ version_ok = "0.16.0"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"
[ATP gappa015]
[ATP gappa]
name = "Gappa"
exec = "gappa-0.15.1"
version_switch = "--version"
......@@ -175,7 +145,7 @@ version_ok = "0.15.1"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"
[ATP gappa014]
[ATP gappa]
name = "Gappa"
exec = "gappa-0.14.1"
version_switch = "--version"
......@@ -226,27 +196,17 @@ version_regexp = "Version: \\([^ \n\r]+\\)"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
driver = "drivers/verit.drv"
[ATP z3-4]
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-4.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.0"
version_bad = "3.2"
version_bad = "3.1"
version_bad = "3.0"
version_bad = "2.19"
version_bad = "2.18"
version_bad = "2.17"
version_bad = "2.16"
version_bad = "2.2"
version_bad = "2.1"
version_bad = "1.3"
driver = "drivers/z3.drv"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"
[ATP z3-3]
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-3.2"
......@@ -254,22 +214,14 @@ exec = "z3-3.1"
exec = "z3-3.0"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_bad = "4.0"
version_ok = "3.2"
version_old = "3.1"
version_old = "3.0"
version_bad = "2.19"
version_bad = "2.18"
version_bad = "2.17"
version_bad = "2.16"
version_bad = "2.2"
version_bad = "2.1"
version_bad = "1.3"
driver = "drivers/z3.drv"
# the -T is unreliable in Z3 3.2
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 %f"
[ATP z3-2]
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-2.19"
......@@ -278,17 +230,10 @@ exec = "z3-2.17"
exec = "z3-2.16"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_bad = "4.0"
version_bad = "3.2"
version_bad = "3.1"
version_bad = "3.0"
version_ok = "2.19"
version_old = "2.18"
version_old = "2.17"
version_old = "2.16"
version_bad = "2.2"
version_bad = "2.1"
version_bad = "1.3"
driver = "drivers/z3.drv"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -smt2 -rs:42 \
PHASE_SELECTION=0 \
......@@ -310,7 +255,7 @@ DELAY_UNITS_THRESHOLD=16 \
#ASYNC_COMMANDS=false
#NNF_SK_HACK=true
[ATP z3-2]
[ATP z3]
name = "Z3"
exec = "z3"
exec = "z3-2.2"
......@@ -318,9 +263,6 @@ exec = "z3-2.1"
exec = "z3-1.3"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_bad = "3.2"
version_bad = "3.1"
version_bad = "3.0"
version_old = "2.2"
version_old = "2.1"
version_old = "1.3"
......@@ -337,6 +279,15 @@ version_ok = "8.3pl3"
version_ok = "8.3pl2"
version_ok = "8.3pl1"
version_ok = "8.3"
command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv"
editor = "coqide"
[ITP coq]
name = "Coq"
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_old = "8.2pl2"
version_old = "8.2pl1"
version_old = "8.2"
......
......@@ -70,7 +70,7 @@ let option_list = Arg.align [
(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";
"--install-plugin", Arg.String add_plugin,
......
......@@ -18,10 +18,39 @@
(* *)
(**************************************************************************)
(*****
1) For every block, for every executable call the prover using the
version switch and add the prover to the configuration if the version
match one of the version_ok or version_old but none of the version_bad
2) We consider that an executable name which appears in a block, but
which version isn't a version_ok, version_old or version_bad has an
unknown version
3) For every executable which have an unknown version, we add the
prover using the first block that contains it.
Don't use the family argument except when you add manualy one prover.
So the order of the block is used only when the version of an
executable appears in none of the block.
A block with more than one exec fields is now the same thing than if you
split the block into blocks containing one fields.
New message field that allows to print a message when a prover is
detected. If a message is not present, we print ", Ok." if the version
is good (version_good) and not old, and " (it is an old version)." if
the version is old (version_old).
The field command can be missing in a block, in that case the block
defines a version known to be buggy: no prover config is generated.
*)
open Format
open Util
open Ident
open Whyconf
module Wc = Whyconf
open Rc
let debug = Debug.register_flag "autodetect"
......@@ -33,16 +62,19 @@ type prover_autodetection_data =
{ kind : prover_kind;
prover_id : string;
prover_name : string;
prover_altern : string;
execs : string list;
version_switch : string;
version_regexp : string;
versions_ok : string list;
versions_old : string list;
versions_bad : string list;
prover_command : string;
(** If none it's a fake prover (very bad version) *)
prover_command : string option;
prover_driver : string;
prover_editor : string;
prover_in_place : bool;
message : string option;
}
let prover_keys =
......@@ -50,23 +82,25 @@ let prover_keys =
List.fold_left add Sstr.empty
["name";"exec";"version_switch";"version_regexp";
"version_ok";"version_old";"version_bad";"command";
"editor";"driver";"in_place"]
"editor";"driver";"in_place";"message"]
let load_prover kind (id,section) =
check_exhaustive section prover_keys;
{ kind = kind;
prover_id = id;
prover_name = get_string section "name";
prover_altern = get_string section ~default:"" "altern";
execs = get_stringl section "exec";
version_switch = get_string section ~default:"" "version_switch";
version_regexp = get_string section ~default:"" "version_regexp";
versions_ok = get_stringl section ~default:[] "version_ok";
versions_old = get_stringl section ~default:[] "version_old";
versions_bad = get_stringl section ~default:[] "version_bad";
prover_command = get_string section "command";
prover_command = get_stringo section "command";
prover_driver = get_string section "driver";
prover_editor = get_string section ~default:"" "editor";
prover_in_place = get_bool section ~default:false "in_place";
message = get_stringo section "message";
}
let editor_keys =
......@@ -94,7 +128,7 @@ let read_auto_detection_data main =
"provers-detection-data.conf" in
try
let rc = Rc.from_file filename in
load rc
List.rev (load rc)
with
| Failure "lexing" ->
Loc.errorm "Syntax error in provers-detection-data.conf@."
......@@ -103,8 +137,6 @@ let read_auto_detection_data main =
let provers_found = ref 0
let prover_tips_info = ref false
let read_editors main =
let filename = Filename.concat (Whyconf.datadir main)
"provers-detection-data.conf" in
......@@ -138,9 +170,24 @@ let sanitize_exec =
in
sanitizer first rest
let detect_exec main data com =
type env =
{
(** memoization of (exec_name,version_switch)
-> Some output | None doesn't exists *)
prover_output : ((string * string),string option) Hashtbl.t;
(** existing executable table:
exec_name -> | Some prover_config unknown version (neither good or bad)
| None there is a good version *)
prover_unknown_version : (string, config_prover option) Hashtbl.t;
}
let create_env () =
{ prover_output = Hashtbl.create 10;
prover_unknown_version = Hashtbl.create 10 }
let ask_prover_version exec_name version_switch =
let out = Filename.temp_file "out" "" in
let cmd = sprintf "%s %s" com data.version_switch in
let cmd = sprintf "%s %s" exec_name version_switch in
let c = sprintf "(%s) > %s 2>&1" cmd out in
Debug.dprintf debug "Run : %s@." c;
let ret = Sys.command c in
......@@ -150,92 +197,167 @@ let detect_exec main data com =
None
end
else
let s =
try
let ch = open_in out in
let c = Sysutil.channel_contents ch in
close_in ch;
Sys.remove out;
c
with Not_found | End_of_file -> ""
in
let re = Str.regexp data.version_regexp in
try
let ch = open_in out in
let c = Sysutil.channel_contents ch in
close_in ch;
Sys.remove out;
Some c
with Not_found | End_of_file -> Some ""
let ask_prover_version env exec_name version_switch =
try
Hashtbl.find env.prover_output (exec_name,version_switch)
with Not_found ->
let res = ask_prover_version exec_name version_switch in
Hashtbl.replace env.prover_output (exec_name,version_switch) res;
res
let check_version (version : string) schema = schema = version
let known_version env exec_name =
Hashtbl.replace env.prover_unknown_version exec_name None
let unknown_version env exec_name prover_config =
if not (Hashtbl.mem env.prover_unknown_version exec_name)
then Hashtbl.replace env.prover_unknown_version exec_name (Some prover_config)
let empty_alt s = if s = "" then "alt" else s
let find_prover_altern provers prover_id =
if not (Mprover.mem prover_id provers) then prover_id
else
let prover_id =
{prover_id with
Wc.prover_altern = empty_alt prover_id.Wc.prover_altern} in
if not (Mprover.mem prover_id provers) then prover_id
else
let rec aux n =
let prover_id_n = {prover_id with
Wc.prover_altern = sprintf "%s_%i"
(empty_alt prover_id.Wc.prover_altern) n} in
if Mprover.mem prover_id_n provers
then aux (n+1)
else prover_id_n in
(** start with 2 in order to have toto_alt, toto_alt2,
toto_alt3,... and not toto_alt, toto_alt1 which can be
confusing *)
aux 2
let add_prover_with_uniq_id prover provers =
(** find an unique prover triplet *)
let prover_id = find_prover_altern provers prover.Wc.prover in
let prover = {prover with Wc.prover = prover_id} in
(** find an unique id *)
let test id _ p = p.Wc.id = id in
if not (Mprover.exists (test prover.Wc.id) provers)
then Mprover.add prover.Wc.prover prover provers
else
let rec aux i =
let prover_id = sprintf "%s_%i" prover.Wc.id i in
if not (Mprover.exists (test prover_id) provers)
then Mprover.add prover.Wc.prover
{prover with id = prover_id} provers
else aux (i+1) in
aux 2
let detect_exec env main data acc exec_name =
let s = ask_prover_version env exec_name data.version_switch in
match s with
| None -> acc
| Some s ->
let re = Str.regexp data.version_regexp in
let ver =
try
ignore (Str.search_forward re s 0);
let nam = data.prover_name in
let ver = Str.matched_group 1 s in
if List.mem ver data.versions_bad then
None
else begin
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;
let c = make_command com data.prover_command in
let prover = {Whyconf.prover_name = data.prover_name;
prover_version = ver;
prover_altern = ""} in
Some {prover = prover;
id = data.prover_id;
command = c;
driver = Filename.concat (datadir main) data.prover_driver;
editor = data.prover_editor;
in_place = data.prover_in_place;
interactive = (match data.kind with ITP -> true | ATP -> false);
extra_options = [];
extra_drivers = [] }
end
Str.matched_group 1 s
with Not_found ->
begin
prover_tips_info := true;
eprintf "Warning: found prover %s but name/version not \
Debug.dprintf debug "Warning: found prover %s but name/version not \
recognized by regexp `%s'@."
data.prover_name data.version_regexp;
eprintf "Answer was `%s'@." s;
None
Debug.dprintf debug "Answer was `%s'@." s;
""
end
in
(** bad mean here not good, it's not the same thing than a version
of a prover with known problems *)
let bad = List.exists (check_version ver) data.versions_bad in
if bad then (known_version env exec_name; acc)
else
let good = List.exists (check_version ver) data.versions_ok in
let old = List.exists (check_version ver) data.versions_old in
match data.prover_command with
| None ->
(** Empty prover *)
if good || old then begin (** Known version with error *)
known_version env exec_name;
eprintf "Found prover %s version %s%s@."
data.prover_name ver
(def_option
". This version of the prover is known to have problems."
data.message);
acc
end
else (** it's not a known bad version *) acc
let detect_prover main acc l =
try
let detect_execs data =
try Some (Util.list_first (detect_exec main data) data.execs)
with Not_found -> None
in
let prover = Util.list_first detect_execs l in
Mprover.add prover.prover prover acc
with Not_found ->
eprintf "Prover %s not found.@." (List.hd l).prover_id;
acc
(* does not work
List.fold_left
(fun acc data ->
List.fold_left
(fun acc e ->
eprintf "Trying executable %s@." e;
match detect_exec main data e with
| None -> acc
| Some prover -> Mstr.add prover_id prover acc)
acc data.execs)
acc l
*)
| Some prover_command ->
(** create the prover config *)
let c = make_command exec_name prover_command in
let prover = {Wc.prover_name = data.prover_name;
prover_version = ver;
prover_altern = data.prover_altern} in
let prover_config =
{prover = prover;
id = data.prover_id;
command = c;
driver = Filename.concat (datadir main) data.prover_driver;
editor = data.prover_editor;
in_place = data.prover_in_place;
interactive = (match data.kind with ITP -> true | ATP -> false);
extra_options = [];
extra_drivers = [] } in
if good || old then begin
eprintf "Found prover %s version %s%s@."
data.prover_name ver
(def_option (if old then " (it is an old version)." else ", Ok.")
data.message);
known_version env exec_name;
add_prover_with_uniq_id prover_config acc
end
else (unknown_version env exec_name prover_config; acc)
let detect_prover env main acc data =
List.fold_left (detect_exec env main data) acc data.execs
(** add the prover unknown *)
let detect_unknown env detected =
Hashtbl.fold (fun _ pc acc ->
match pc with
| None -> acc
| Some prover_config ->
let prover = prover_config.prover in
eprintf "Warning: prover %s version %s is not known to be \
supported, use it at your own risk!@."
prover.Wc.prover_name prover.prover_version;
add_prover_with_uniq_id prover_config acc)
env.prover_unknown_version detected
let run_auto_detection config =
let main = get_main config in
let l = read_auto_detection_data main in
let cmp p q = String.compare p.prover_id q.prover_id in
let l = Util.list_part cmp l in
let detect = List.fold_left (detect_prover main) Mprover.empty l in
let length = Mprover.cardinal detect in
eprintf "%d provers detected.@." length;
let env = create_env () in
let detect = List.fold_left (detect_prover env main) Mprover.empty l in
let length_detected = Mprover.cardinal detect in
let detect = detect_unknown env detect in
let length_unsupported_version = Mprover.cardinal detect - length_detected in
eprintf
"%d provers detected and %d provers detected with unsupported version@."
length_detected length_unsupported_version;
set_provers (set_editors config (read_editors main)) detect
let list_prover_ids () =
......@@ -245,34 +367,49 @@ let list_prover_ids () =
let s = List.fold_left (fun s p -> Sstr.add p.prover_id s) Sstr.empty l in
Sstr.elements s
let get_altern id path =
let alt = Filename.basename path in
let get_suffix id alt =
let ilen = String.length id in
let alen = String.length alt in
let rec get_suffix i =
let rec aux i =
if i = alen then "alt" else
if i = ilen then String.sub alt i (alen-i) else
if id.[i] = alt.[i] then get_suffix (i+1) else
if id.[i] = alt.[i] then aux (i+1) else
String.sub alt i (alen-i)
in
get_suffix 0
aux 0
let get_altern id path =
let alt = Filename.basename path in
get_suffix id alt
let add_prover_binary config id path =
let main = get_main config in
let l = read_auto_detection_data main in
let l = List.filter (fun p -> p.prover_id = id) l in
if l = [] then Loc.errorm "Unknown prover id: %s" id;
let p = try
Util.list_first (fun d -> detect_exec main d path) (List.rev l)
with Not_found ->
Loc.errorm "File %s does not correspond to the prover id %s" path id
in