Commit d65e0492 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Use the "option=" option from extra configuration files.

parent a07b7fd3
...@@ -56,7 +56,8 @@ let rec goal whyconf env path dbgoal wgoal = ...@@ -56,7 +56,8 @@ let rec goal whyconf env path dbgoal wgoal =
let driver, extra, command = let driver, extra, command =
try try
let p = Mstr.find prover_name (Whyconf.get_provers whyconf) in let p = Mstr.find prover_name (Whyconf.get_provers whyconf) in
p.Whyconf.driver, p.Whyconf.extra_drivers, p.Whyconf.command p.Whyconf.driver, p.Whyconf.extra_drivers,
String.concat " " (p.Whyconf.command :: p.Whyconf.extra_options)
with with
(* TODO add exceptions pehaps inside rc.ml in fact*) (* TODO add exceptions pehaps inside rc.ml in fact*)
| Not_found -> | Not_found ->
......
...@@ -76,7 +76,8 @@ let read_tools absf wc map (name,section) = ...@@ -76,7 +76,8 @@ let read_tools absf wc map (name,section) =
let provers = get_stringl ~default:[] section "prover" in let provers = get_stringl ~default:[] section "prover" in
let find_provers s = let find_provers s =
try let p = Mstr.find s (get_provers wc) in try let p = Mstr.find s (get_provers wc) in
s, p.driver, p.extra_drivers, p.command s, p.driver, p.extra_drivers,
String.concat " " (p.command :: p.extra_options)
with with
(* TODO add exceptions pehaps inside rc.ml in fact*) (* TODO add exceptions pehaps inside rc.ml in fact*)
| Not_found -> eprintf "Prover %s not found.@." s; exit 1 in | Not_found -> eprintf "Prover %s not found.@." s; exit 1 in
......
...@@ -894,7 +894,7 @@ let whytac s gl = ...@@ -894,7 +894,7 @@ let whytac s gl =
try try
tr_goal gl; tr_goal gl;
let cp, drv = get_prover s in let cp, drv = get_prover s in
let command = cp.command in let command = String.concat " " (cp.command :: cp.extra_options) in
if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task; if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task; if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
let res = Driver.prove_task ~command ~timelimit drv !task () () in let res = Driver.prove_task ~command ~timelimit drv !task () () in
......
...@@ -43,7 +43,7 @@ let get_prover_data env id pr acc = ...@@ -43,7 +43,7 @@ let get_prover_data env id pr acc =
{ prover_id = id ; { prover_id = id ;
prover_name = pr.Whyconf.name; prover_name = pr.Whyconf.name;
prover_version = pr.Whyconf.version; prover_version = pr.Whyconf.version;
command = pr.Whyconf.command; command = String.concat " " (pr.Whyconf.command :: pr.Whyconf.extra_options);
driver_name = pr.Whyconf.driver; driver_name = pr.Whyconf.driver;
driver = dr; driver = dr;
editor = pr.Whyconf.editor; editor = pr.Whyconf.editor;
......
...@@ -351,7 +351,7 @@ let () = try ...@@ -351,7 +351,7 @@ let () = try
| Not_found -> eprintf "Prover '%s' not found in %s@." | Not_found -> eprintf "Prover '%s' not found in %s@."
s (Whyconf.get_conf_file config); exit 1 s (Whyconf.get_conf_file config); exit 1
in in
opt_command := Some prover.command; opt_command := Some (String.concat " " (prover.command :: prover.extra_options));
opt_driver := Some (prover.driver, prover.extra_drivers) opt_driver := Some (prover.driver, prover.extra_drivers)
| None -> | None ->
() ()
......
Supports Markdown
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