From: Claudio Sacerdoti Coen Date: Fri, 30 Dec 2022 21:27:33 +0000 (+0100) Subject: Worker thread killing fixed X-Git-Tag: make_still_working~11 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d7aca3eacb4bd8dc56223098f92e5370c82f92ff;p=helm.git Worker thread killing fixed In old Ocaml it used to work catching a Unix signal that was raised at the end of each timeslice. It works no more in Ocaml5. - we now use a fixed timer (every 1s) to trigger the Unix signal - the signal is usually caught by the non-worker thread and for some reason blocking the signal interferes with Gtk - solution: if the signal is caught by the non-worker thread, the thread goes to sleep for 3s to let the worker thread catch the signal Most of the time the trick works, even if some delay is introdued. --- diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index af5ea5805..88f5cb380 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -599,6 +599,8 @@ class gui () = let source_view = script#source_view in let thread_main = fun () -> + ignore (Thread.sigmask Unix.SIG_UNBLOCK [Sys.sigint]); + ignore (Thread.sigmask Unix.SIG_UNBLOCK [Sys.sigvtalrm]); lock_world (); let saved_use_library= !MultiPassDisambiguator.use_library in try @@ -630,18 +632,22 @@ class gui () = with Sys.Break as e -> notify_exn source_view e); unlock_world () in - (*thread_main ();*) worker_thread := Some (Thread.create thread_main ()) in let kill_worker = - (* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *) let interrupt = ref None in let old_callback = ref (function _ -> ()) in let force_interrupt n = - (* This function is called just before the thread's timeslice ends *) + (* This function is called every 1s (see Unix.setitimer call above) *) !old_callback n; if Some(Thread.id(Thread.self())) = !interrupt then - (interrupt := None; raise Sys.Break) in + (interrupt := None; raise Sys.Break) + else if !interrupt <> None then + (* Code executed in the non-worker thread; delay it to let the + worker thread catch the signal *) + Thread.delay 3.; + in + ignore (Unix.setitimer Unix.ITIMER_VIRTUAL {Unix.it_interval = 1.; it_value = 1.}); let _ = match Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) with Sys.Signal_handle f -> old_callback := f