Commit 78437f58 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

why-ide avec plusieurs prouveurs

parent c81ddd02
...@@ -185,6 +185,7 @@ let find_prover s = ...@@ -185,6 +185,7 @@ let find_prover s =
| Some p -> p | Some p -> p
let alt_ergo = find_prover "Alt-Ergo" let alt_ergo = find_prover "Alt-Ergo"
let simplify = find_prover "simplify"
let z3 = find_prover "Z3" let z3 = find_prover "Z3"
...@@ -272,7 +273,7 @@ module Ide_goals = struct ...@@ -272,7 +273,7 @@ module Ide_goals = struct
Ident.Hid.add goal_table id (g,row); Ident.Hid.add goal_table id (g,row);
model#set ~row ~column:name_column name; model#set ~row ~column:name_column name;
model#set ~row ~column:id_column id; model#set ~row ~column:id_column id;
model#set ~row ~column:status_column `REMOVE; (* model#set ~row ~column:status_column `REMOVE; *)
) )
tasks tasks
...@@ -324,17 +325,20 @@ let count = ref 0 ...@@ -324,17 +325,20 @@ let count = ref 0
let async f = GtkThread.async f () let async f = GtkThread.async f ()
let prover_on_all_goals ~(model:GTree.tree_store) p () = let prover_on_all_goals ~(model:GTree.tree_store) ~(view:GTree.view) p () =
Ident.Hid.iter Ident.Hid.iter
(fun id (g,row) -> (fun id (g,row) ->
Format.eprintf "running %s on goal %s@." (Db.prover_name p.prover) let name = Db.prover_name p.prover in
id.Ident.id_string; Format.eprintf "running %s on goal %s@." name id.Ident.id_string;
let prover_row = model#append ~parent:row () in
model#set ~row:prover_row ~column:Ide_goals.name_column name;
view#expand_row (model#get_path row);
incr count; incr count;
let c = !count in let c = !count in
let callback result = let callback result =
printf "Scheduled task #%d: status set to %a@." c printf "Scheduled task #%d: status set to %a@." c
Db.print_status result; Db.print_status result;
model#set ~row ~column:Ide_goals.status_column (stock_of_result result); model#set ~row:prover_row ~column:Ide_goals.status_column (stock_of_result result);
in in
Scheduler.schedule_proof_attempt Scheduler.schedule_proof_attempt
~async ~async
...@@ -383,8 +387,12 @@ let main () = ...@@ -383,8 +387,12 @@ let main () =
tools_factory#add_image_item ~key:GdkKeysyms._A tools_factory#add_image_item ~key:GdkKeysyms._A
~label:"Alt-Ergo on all goals" ~label:"Alt-Ergo on all goals"
~callback:(fun () -> ~callback:(fun () ->
prover_on_all_goals ~model:goals_model alt_ergo ()(*; prover_on_all_goals ~model:goals_model ~view:goals_view
prover_on_all_goals ~model:goals_model z3 ()*)) () alt_ergo ();
prover_on_all_goals ~model:goals_model ~view:goals_view
simplify ();
prover_on_all_goals ~model:goals_model ~view:goals_view
z3 ()) ()
in in
let _ = let _ =
tools_factory#add_image_item ~key:GdkKeysyms._E tools_factory#add_image_item ~key:GdkKeysyms._E
......
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