Commit 1ffc8925 authored by François Bobot's avatar François Bobot
Browse files

Add some Thread.create, GtkThread.sync or async :

Execute modifications of the gui or accesses to
the database inside the thread of gtk using GtkThread.sync or async

Everything else is inside another thread
(yes also the access to the model...).

Don't add proof attempt one by one (one lock each time)

Scheduler : the proof_attempt are added 8 by 8 (if max_running_provers is 2)
parent bfb2abe8
......@@ -66,18 +66,21 @@ end
let call s callback tool prob =
(** Prove goal *)
let call cb task =
schedule_proof_attempt ~debug:(Debug.test_flag debug)
let call q cb task =
Queue.add (create_proof_attempt ~debug:(Debug.test_flag debug)
~timelimit:(tool.ttime) ~memlimit:(tool.tmem)
~command:(tool.tcommand) ~driver:(tool.tdriver)
~callback:cb task in
let iter pval i task =
~callback:cb task) q in
let iter q pval i task =
MTask.start s;
let cb res = callback pval i task res;
match res with Done _ | InternalFailure _ -> MTask.stop s | _ -> () in
call cb task; succ i in
call q cb task; succ i in
let trans_cb pval tl =
ignore (List.fold_left (iter pval) 0 (List.rev tl)); MTask.stop s in
let q = Queue.create () in
ignore (List.fold_left (iter q pval) 0 (List.rev tl));
transfer_proof_attempts q;
MTask.stop s in
(** Apply trans *)
let iter_task (pval,task) =
MTask.start s;
......@@ -899,7 +899,8 @@ let callback_of_callback callback = function
Model.HighFailure in
callback res r.Call_provers.pr_time r.Call_provers.pr_output
let redo_external_proof g a =
(* q is a queue of proof attempt where to put the new one *)
let redo_external_proof q g a =
let p = a.Model.prover in
let callback result time output =
a.Model.output <- output;
......@@ -915,66 +916,70 @@ let redo_external_proof g a =
Db.set_status a.Model.proof_db db_res time
callback Model.Scheduled 0.0 "";
GtkThread.sync (callback Model.Scheduled 0.0) "";
let old = if a.Model.edited_as = "" then None else
eprintf "Info: proving using edited file %s@." a.Model.edited_as;
(Some (open_in a.Model.edited_as))
~debug:(gconfig.verbose > 0) ~timelimit:gconfig.time_limit ~memlimit:0
?old ~command:p.command ~driver:p.driver
~callback:(callback_of_callback callback)
g.Model.task q
let rec prover_on_goal p g =
let rec prover_on_goal q p g =
let id = p.prover_id in
let a =
try Hashtbl.find g.Model.external_proofs id
with Not_found ->
GtkThread.sync (fun () ->
let db_prover = Db.prover_from_name id in
let db_pa = Db.add_proof_attempt g.Model.goal_db db_prover in
Helpers.add_external_proof_row ~obsolete:false ~edit:""
g p db_pa Model.Scheduled 0.0
g p db_pa Model.Scheduled 0.0) ()
redo_external_proof g a;
redo_external_proof q g a;
(fun t -> List.iter (prover_on_goal p) t.Model.subgoals)
(fun t -> List.iter (prover_on_goal q p) t.Model.subgoals)
let rec prover_on_goal_or_children p g =
let rec prover_on_goal_or_children q p g =
if not g.Model.proved then
match g.Model.transformations with
| [] -> prover_on_goal p g
| [] -> prover_on_goal q p g
| l ->
List.iter (fun t ->
List.iter (prover_on_goal_or_children p)
List.iter (prover_on_goal_or_children q p)
t.Model.subgoals) l
let prover_on_selected_goal_or_children pr row =
let prover_on_selected_goal_or_children q pr row =
let row = filter_model#get_iter row in
match filter_model#get ~row ~column:Model.index_column with
| Model.Row_goal g ->
prover_on_goal_or_children pr g
prover_on_goal_or_children q pr g
| Model.Row_theory th ->
List.iter (prover_on_goal_or_children pr) th.Model.goals
List.iter (prover_on_goal_or_children q pr) th.Model.goals
| Model.Row_file file ->
(fun th ->
List.iter (prover_on_goal_or_children pr) th.Model.goals)
List.iter (prover_on_goal_or_children q pr) th.Model.goals)
| Model.Row_proof_attempt a ->
prover_on_goal_or_children pr a.Model.proof_goal
prover_on_goal_or_children q pr a.Model.proof_goal
| Model.Row_transformation tr ->
List.iter (prover_on_goal_or_children pr) tr.Model.subgoals
List.iter (prover_on_goal_or_children q pr) tr.Model.subgoals
let prover_on_selected_goals pr =
(prover_on_selected_goal_or_children pr)
ignore (Thread.create (fun pr ->
let q = Queue.create () in
(prover_on_selected_goal_or_children q pr)
Scheduler.transfer_proof_attempts q ) pr)
......@@ -243,6 +243,26 @@ let schedule_proof_attempt ~debug ~timelimit ~memlimit ?old
Condition.signal queue_condition;
Mutex.unlock queue_lock
let create_proof_attempt ~debug ~timelimit ~memlimit ?old
~command ~driver ~callback
goal =
let transfer_proof_attempts q =
Mutex.lock queue_lock;
Queue.transfer q prover_attempts_queue;
Condition.signal queue_condition;
Mutex.unlock queue_lock
let schedule_some_proof_attempts ~debug ~timelimit ~memlimit ?old
~command ~driver ~callback
goal q =
(debug,timelimit,memlimit,old,command,driver,callback,goal) q;
if Queue.length q >= !maximum_running_proofs * coef_buf * 2 then
transfer_proof_attempts q
let edit_proof ~debug ~editor ~file ~driver ~callback goal =
Mutex.lock queue_lock;
Queue.push (debug,editor,file,driver,callback,goal) proof_edition_queue;
......@@ -67,6 +67,31 @@ val schedule_proof_attempt :
type attempt
val create_proof_attempt : debug:bool -> timelimit:int -> memlimit:int ->
?old:in_channel ->
command:string -> driver:Driver.driver ->
callback:(proof_attempt_status -> unit) ->
Task.task -> attempt
val transfer_proof_attempts : attempt Queue.t -> unit
(** same as the iteration of {!schedule_proof_attempt} but runs in
constant time. The given queue is cleared. *)
val schedule_some_proof_attempts :
debug:bool -> timelimit:int -> memlimit:int ->
?old:in_channel ->
command:string -> driver:Driver.driver ->
callback:(proof_attempt_status -> unit) ->
Task.task -> attempt Queue.t -> unit
(** a middle between schedule_proof_attempts and
transfer_proof_attempts, use an heuristics to send sometimes the
proof_attemps. dont forget to use transfer_proof_attempts at the
end in order to flush the queue.
val apply_transformation :
callback:(Why.Task.task -> unit) ->
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