From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 8B8EDD45F for ; Wed, 2 Nov 2005 13:59:57 +0100 (CET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id jA2CxtBg011277; Wed, 2 Nov 2005 13:59:56 +0100 Received: from localhost (suiren [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.13.1/8.13.1) with ESMTP id jA2Cxrsh009581; Wed, 2 Nov 2005 21:59:54 +0900 (JST) Date: Wed, 02 Nov 2005 22:00:53 +0900 (JST) Message-Id: <20051102.220053.101871063.garrigue@math.nagoya-u.ac.jp> To: Julien.Narboux@inria.fr Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] The best way to circumvent the lack of Thread.kill ? From: Jacques Garrigue In-Reply-To: <4368A16B.4050703@inria.fr> References: <43688C4C.2080606@inria.fr> <20051102105419.GB5067@furbychan.cocan.org> <4368A16B.4050703@inria.fr> X-Mailer: Mew version 4.2 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 4368B84B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 byterun:01 byterun:01 otherlibs:01 labltk:01 bytecode:01 ...:98 theorem:01 workaround:01 jacques:01 jacques:01 thread:02 thread:02 native:02 native:02 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.4 required=5.0 tests=DNS_FROM_RFC_ABUSE autolearn=disabled version=3.0.3 From: Julien Narboux > >How about forking off the theorem prover as a separate process? You > >can communicate the result back to the main program using either a > >status code or a pipe (depending on how complex the result structure > >is). The interrupt button just kills the forked process. > > > Yes, but the problem is that under the native windows port (see > http://caml.inria.fr/pub/docs/manual-ocaml/manual035.html) : > > "kill, pause not implemented (no inter-process signals in Windows)" The workaround I found a long time ago is to embed a thread in the forked process that waits for "signals" on a pipe. If you look at byterun/startup.c and byterun/win32.c you will see that it is started when there is a CAMLSIGPIPE in the environment. This is used by otherlibs/labltk/browser/shell.ml on windows. This already works on any bytecode application. For native code, you could just link that bit of C code, and start it by hand. Another way to do it, which is used by ocamlwin, is to send SIGINT through then win32 function GenerateConsoleCtrlEvent. But this will just interrupt, not kill. And I didn't know that function at that time... Jacques Garrigue