[Openmcl-devel] interrupt signal on windows

[harshrc]

Hello,

In CCL running on Linux(x86), if one continually presses Ctrl-C 
(keyboard interrupt), then
you see ? , 1> , 2> , 3> and so on nested debug levels, (quit) will exit 
completely.

In CCL running on Windows, the above consistent behavior is not 
obtained, instead
you see ? , ? , 1> , 2> , 3> , 2> , 3> ..., and (quit), followed by 
another (quit) will
exit completely.

Is this a bug in CCL Windows implementation?

I maintain ACL2 Sedan, and I have noticed that the first interrupt(to 
interrupt a long
proof or execution) works correctly, but the second interrupt (i.e 
rerunning the above
long running computation and re-interrupting) does not work as expected 
and in fact
ACL2(built with CCL) becomes a runaway process which I need to kill 
explicitly using
Windows Task Manager. And I suspect that perhaps the above Ctrl-C 
behavior of CCL on
Windows is whats causing this problem in ACL2 Sedan. ACL2 Sedan running 
on Linux with
CCL works perfectly, i.e. this is a windows-specific issue.

Any feedback would be helpful.

thanks
/harsh