Commit d408fcc8 authored by David Hauzar's avatar David Hauzar Committed by MARCHE Claude
Browse files

Trying to debug saving why3.conf

parent e3ddf3b3
......@@ -78,7 +78,7 @@ let prover_keys =
List.fold_left add Sstr.empty
["name";"compile_time_support";
"exec";"version_switch";"version_regexp";
"version_ok";"version_old";"version_bad";"command";
"version_ok";"version_old";"version_bad";"command"; "command_steps";
"editor";"driver";"in_place";"message";"alternative";]
let load_prover kind (id,section) =
......@@ -97,7 +97,7 @@ let load_prover kind (id,section) =
versions_old = reg_map (get_stringl section ~default:[] "version_old");
versions_bad = reg_map (get_stringl section ~default:[] "version_bad");
prover_command = get_stringo section "command";
prover_command_steps = get_stringo section "commad_steps";
prover_command_steps = get_stringo section "command_steps";
prover_driver = get_string section ~default:"" "driver";
prover_editor = get_string section ~default:"" "editor";
prover_in_place = get_bool section ~default:false "in_place";
......@@ -379,10 +379,17 @@ let detect_exec env main data acc exec_name =
| Some prover_command ->
(** create the prover config *)
let c = make_command exec_name prover_command in
let c_steps = (match data.prover_command_steps with
| None -> None
| Some prover_command_steps ->
Some (make_command exec_name prover_command_steps)) in
(*
let c_steps = (match data.prover_command_steps with
| None -> ""
| Some prover_command_steps ->
(make_command exec_name prover_command_steps)) in *)
let prover = {Wc.prover_name = data.prover_name;
prover_version = ver;
prover_altern = data.prover_altern} in
......
......@@ -208,10 +208,12 @@ exception StepsCommandNotSpecified of string
let get_complete_command pc stepslimit =
let comm = if stepslimit < 0 then pc.command
else
else
match pc.command_steps with
| None -> raise (StepsCommandNotSpecified "The solver is used with step limit and the command for running the solver with steplimit is not specified.")
| Some command_steps -> command_steps in
(* pc.command_steps in *)
String.concat " " (comm :: pc.extra_options)
let set_limits m time mem running =
......@@ -711,9 +713,22 @@ let merge_config config filename =
{ config with main = main; provers = provers; strategies = strategies;
prover_shortcuts = shortcuts; editors = editors }
let debug = Debug.register_info_flag "whyconf"
~desc:"Print@ debugging@ messages@ about@ whyconf."
let debug_print_commands key prover =
Debug.dprintf debug "Prover name = %s@." key.prover_name;
Debug.dprintf debug "Prover commad = %s@." prover.command;
match prover.command_steps with
| None -> Debug.dprintf debug "Steps command not given."
| Some (comm_steps) ->Debug.dprintf debug "Prover commad steps = %s@." comm_steps
let save_config config =
let filename = config.conf_file in
if filename <> "" then begin
Debug.dprintf debug "Prover configurations:@.";
Mprover.iter debug_print_commands config.provers;
Sysutil.backup_file filename;
to_file filename config.config
end
......
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