The same thing can be done in Windows by running the Task Manager and ending the tlapm process.
However, all the backend provers are run with timeouts. If tlapm spends a long time running without producing any console output, then something is wrong. There was a version of tlapm that caused running the prover on even a part of a long proof to take a long time. That problem should have been fixed, but possibly not in the released version. However, that time was spent generating the proof obligations, before it starts proving them. If you can find a short example in which tlapm hangs after it has begun proving obligations, we would appreciate seeing it.
Thanks,
Leslie
On Tuesday, September 30, 2014 4:40:01 AM UTC-7, fl wrote:
Ctrl-G, Ctrl-G in toolbox sometimes ends in a somewhat long loop. Not an endless one but
a very long one anyway.
Those who use a linux box may want to open a terminal, run "top" and type "kill + the job number of tlapm".
For instance "k 6666". (No connection with the Da Vinci Code.)
That works pretty well, simply "toolbox" launches a window announcing that "tlapm" has crashed.
Which is true.
--
FL