From f20fce1259563f2081fadc62ccab1304bb8161d5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Aug 2015 19:00:59 +0200 Subject: Rich printing of messages. --- stm/asyncTaskQueue.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm/asyncTaskQueue.ml') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index e3fb0b607a..e525031e63 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -297,7 +297,7 @@ module Make(T : Task) = struct let slave_feeder oc fb = Marshal.to_channel oc (RespFeedback fb) []; flush oc in Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); - Pp.log_via_feedback (); + Pp.log_via_feedback (fun msg -> Richpp.repr (Richpp.richpp_of_pp msg)); Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- stm/asyncTaskQueue.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'stm/asyncTaskQueue.ml') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index e525031e63..863bab7cc9 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -60,9 +60,7 @@ module Make(T : Task) = struct type more_data = | MoreDataUnivLevel of Univ.universe_level list - - let request_expiry_of_task (t, c) = T.request_of_task t, c - + let slave_respond (Request r) = let res = T.perform r in Response res -- cgit v1.2.3 From e5f5ea2da95297fefe1afebfe303c5d5ba7d41aa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Jan 2016 15:38:34 +0100 Subject: workers: purge short version of -load-vernac too (fix #4458) --- stm/asyncTaskQueue.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'stm/asyncTaskQueue.ml') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index e3fb0b607a..222f02c007 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -125,8 +125,9 @@ module Make(T : Task) = struct "-async-proofs-worker-priority"; Flags.string_of_priority !Flags.async_proofs_worker_priority] | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl - | ("-async-proofs" |"-toploop" |"-vi2vo" |"-compile" - |"-load-vernac-source" |"-compile-verbose" + | ("-async-proofs" |"-toploop" |"-vi2vo" + |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" + |"-compile" |"-compile-verbose" |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl -> set_slave_opt tl | x::tl -> x :: set_slave_opt tl in -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- stm/asyncTaskQueue.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm/asyncTaskQueue.ml') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 222f02c007..cc97326047 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* CEphemeron. Fixes compilation of Coq with OCaml 4.03 beta 1. --- stm/asyncTaskQueue.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm/asyncTaskQueue.ml') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index cc97326047..5f018ec39d 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -314,7 +314,7 @@ module Make(T : Task) = struct let response = slave_respond request in report_status "Idle"; marshal_response (Option.get !slave_oc) response; - Ephemeron.clear () + CEphemeron.clear () with | MarshalError s -> pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 -- cgit v1.2.3 From 45e43916a7ce756b617b7ba3f8062f7956872fb3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 15 Mar 2016 17:10:16 +0100 Subject: Tentative fix for bug #4614: "Fully check the document" is uninterruptable. The SIGINT sent to the master coqtop process was lost in a watchdog thread, so that the STM resulted in an inconsistent state. This patch catches gracefully the exception and kills the task as if it were normally cancelled. Note that it probably won't work on non-POSIX architectures, but it does not really matter because interrupt was already badly handled anyway. --- stm/asyncTaskQueue.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'stm/asyncTaskQueue.ml') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 5f018ec39d..8649a14c54 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -184,6 +184,13 @@ module Make(T : Task) = struct let () = Unix.sleep 1 in kill_if () in + let kill_if () = + try kill_if () + with Sys.Break -> + let () = stop_waiting := true in + let () = TQueue.broadcast queue in + Worker.kill proc + in let _ = Thread.create kill_if () in try while true do -- cgit v1.2.3