Jacques Garrigue wrote:

>From: Julien Narboux <Julien.Narboux@inria.fr>
>
>  
>
>>>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
>  
>
I will try that thanks a lot for your answer.

Julien Narboux