Commit 72f9215b authored by MARCHE Claude's avatar MARCHE Claude
Browse files

debug mode

parent 41a11117
...@@ -16,6 +16,7 @@ type t = ...@@ -16,6 +16,7 @@ type t =
mutable tree_width : int; mutable tree_width : int;
mutable task_height : int; mutable task_height : int;
mutable time_limit : int; mutable time_limit : int;
mutable verbose : int;
mutable max_running_processes : int; mutable max_running_processes : int;
mutable provers : prover_data list; mutable provers : prover_data list;
} }
...@@ -26,6 +27,7 @@ let default = ...@@ -26,6 +27,7 @@ let default =
tree_width = 512; tree_width = 512;
task_height = 384; task_height = 384;
time_limit = 2; time_limit = 2;
verbose = 0;
max_running_processes = 2; max_running_processes = 2;
provers = []; provers = [];
} }
...@@ -47,6 +49,7 @@ let save_config config = ...@@ -47,6 +49,7 @@ let save_config config =
fprintf fmt "tree_width = %d@\n" config.tree_width; fprintf fmt "tree_width = %d@\n" config.tree_width;
fprintf fmt "task_height = %d@\n" config.task_height; fprintf fmt "task_height = %d@\n" config.task_height;
fprintf fmt "time_limit = %d@\n" config.time_limit; 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 "max_processes = %d@\n" config.max_running_processes;
fprintf fmt "@."; fprintf fmt "@.";
List.iter (save_prover fmt) config.provers; List.iter (save_prover fmt) config.provers;
...@@ -59,6 +62,7 @@ let load_main c (key, value) = ...@@ -59,6 +62,7 @@ let load_main c (key, value) =
| "tree_width" -> c.tree_width <- Rc.int value | "tree_width" -> c.tree_width <- Rc.int value
| "task_height" -> c.task_height <- Rc.int value | "task_height" -> c.task_height <- Rc.int value
| "time_limit" -> c.time_limit <- Rc.int value | "time_limit" -> c.time_limit <- Rc.int value
| "verbose" -> c.verbose <- Rc.int value
| "max_processes" -> c.max_running_processes <- Rc.int value | "max_processes" -> c.max_running_processes <- Rc.int value
| s -> | s ->
eprintf "Warning: ignore unknown key [%s] in whyide config file@." s eprintf "Warning: ignore unknown key [%s] in whyide config file@." s
...@@ -240,14 +244,19 @@ let preferences c = ...@@ -240,14 +244,19 @@ let preferences c =
let vbox = dialog#vbox in let vbox = dialog#vbox in
let notebook = GPack.notebook ~packing:vbox#add () in let notebook = GPack.notebook ~packing:vbox#add () in
(** page 1 **) (** page 1 **)
let label1 = GMisc.label ~text:"Provers" () in let label1 = GMisc.label ~text:"General" () in
let page1 = let page1 =
GPack.vbox ~homogeneous:false ~packing: GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label1#coerce w)) () (fun w -> ignore(notebook#append_page ~tab_label:label1#coerce w)) ()
in in
(* debug mode ? *) (* debug mode ? *)
let _debugmode = let debugmode =
GButton.check_button ~label:"debug" ~packing:page1#add () GButton.check_button ~label:"debug" ~packing:page1#add ()
~active:(c.verbose > 0)
in
let (_ : GtkSignal.id) =
debugmode#connect#toggled ~callback:
(fun () -> c.verbose <- 1 - c.verbose)
in in
(* timelimit ? *) (* timelimit ? *)
let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
...@@ -270,18 +279,14 @@ let preferences c = ...@@ -270,18 +279,14 @@ let preferences c =
(fun () -> c.max_running_processes <- nb_processes_spin#value_as_int) (fun () -> c.max_running_processes <- nb_processes_spin#value_as_int)
in in
(** page 2 **) (** page 2 **)
let label2 = GMisc.label ~text:"Misc" () in let label2 = GMisc.label ~text:"Provers" () in
let _page2 = GMisc.label ~text:"contents of page 2" let _page2 = GMisc.label ~text:"This page should display detected provers"
~packing:(fun w -> ignore(notebook#append_page ~tab_label:label2#coerce w)) () ~packing:(fun w -> ignore(notebook#append_page ~tab_label:label2#coerce w)) ()
in in
(*
let (_ : GtkSignal.id) =
notebook#connect#switch_page
~callback:(fun i -> prerr_endline ("Page switch to " ^ string_of_int i))
in
*)
dialog#add_button "Close" `CLOSE ; dialog#add_button "Close" `CLOSE ;
let ( _ : GWindow.Buttons.about) = dialog#run () in let ( _ : GWindow.Buttons.about) = dialog#run () in
eprintf "saving IDE config file@.";
save_config c;
dialog#destroy () dialog#destroy ()
......
...@@ -15,6 +15,7 @@ type t = ...@@ -15,6 +15,7 @@ type t =
mutable tree_width : int; mutable tree_width : int;
mutable task_height : int; mutable task_height : int;
mutable time_limit : int; mutable time_limit : int;
mutable verbose : int;
mutable max_running_processes : int; mutable max_running_processes : int;
mutable provers : prover_data list; mutable provers : prover_data list;
} }
......
...@@ -17,8 +17,6 @@ ...@@ -17,8 +17,6 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
let pname = "[Why Ide]"
let () = ignore (GtkMain.Main.init ()) let () = ignore (GtkMain.Main.init ())
open Format open Format
...@@ -35,13 +33,13 @@ let config = ...@@ -35,13 +33,13 @@ let config =
Whyconf.read_config None Whyconf.read_config None
with with
| Not_found -> | Not_found ->
eprintf "%s no config file found.@." pname; eprintf "no config file found.@.";
exit 1 exit 1
| e -> | e ->
eprintf "%a@." Exn_printer.exn_printer e; eprintf "%a@." Exn_printer.exn_printer e;
exit 1 exit 1
let () = eprintf "%s Load path is: %a@." pname let () = eprintf "Load path is: %a@."
(Pp.print_list Pp.comma Pp.string) config.loadpath (Pp.print_list Pp.comma Pp.string) config.loadpath
(* (*
...@@ -65,12 +63,8 @@ let set_file f = match !file with ...@@ -65,12 +63,8 @@ let set_file f = match !file with
| Some _ -> | Some _ ->
raise (Arg.Bad "only one file") raise (Arg.Bad "only one file")
| None -> | None ->
(*
if not (Filename.check_suffix f ".why") then
raise (Arg.Bad ("don't know what to do with " ^ f));
*)
if not (Sys.file_exists f) then begin if not (Sys.file_exists f) then begin
Format.eprintf "%s %s: no such file@." pname f; Format.eprintf "%s: no such file@." f;
exit 1 exit 1
end; end;
file := Some f file := Some f
...@@ -113,7 +107,7 @@ let env = Why.Env.create_env (Why.Lexer.retrieve config.loadpath) ...@@ -113,7 +107,7 @@ let env = Why.Env.create_env (Why.Lexer.retrieve config.loadpath)
(********************************) (********************************)
let gconfig = let gconfig =
eprintf "%s reading IDE config file@." pname; eprintf "reading IDE config file@.";
read_config env config read_config env config
...@@ -293,7 +287,7 @@ end ...@@ -293,7 +287,7 @@ end
(***************) (***************)
let exit_function () = let exit_function () =
eprintf "%s saving IDE config file@." pname; eprintf "saving IDE config file@.";
save_config gconfig; save_config gconfig;
GMain.quit () GMain.quit ()
...@@ -478,7 +472,7 @@ let rec prover_on_goal p g = ...@@ -478,7 +472,7 @@ let rec prover_on_goal p g =
in in
callback Scheduler.Scheduled 0.0 ""; callback Scheduler.Scheduled 0.0 "";
Scheduler.schedule_proof_attempt Scheduler.schedule_proof_attempt
~debug:false ~timelimit:gconfig.time_limit ~memlimit:0 ~debug:(gconfig.verbose > 0) ~timelimit:gconfig.time_limit ~memlimit:0
~prover:p.prover_id ~command:p.command ~driver:p.driver ~prover:p.prover_id ~command:p.command ~driver:p.driver
~callback ~callback
g.Model.task; g.Model.task;
......
...@@ -91,7 +91,7 @@ let event_handler () = ...@@ -91,7 +91,7 @@ let event_handler () =
!async (fun () -> callback Running 0.0 "") (); !async (fun () -> callback Running 0.0 "") ();
try try
let call_prover : unit -> Call_provers.prover_result = let call_prover : unit -> Call_provers.prover_result =
if false && debug then if debug then
Format.eprintf "Task for prover: %a@." Format.eprintf "Task for prover: %a@."
(Driver.print_task driver) goal; (Driver.print_task driver) goal;
Driver.prove_task ~command ~timelimit ~memlimit driver goal Driver.prove_task ~command ~timelimit ~memlimit driver goal
......
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