Rob, I'm copying this to Poly/ML mailing list since I think there are issues here that may affect other users.
The handling of console interrupt (control-C, SIGINT) changed quite significantly in 5.1 as a result of changing from a single threaded model to multiple threads. It's complicated because there are significant differences in the way Mac OS X and Linux handle signals with multiple threads.
Since there may be Isabelle users reading this it's worth pointing out that Isabelle replaces the default Poly/ML SIGINT handler with its own handler using Signal.signal. This uses Thread.Thread.broadcastInterrupt to send an Interrupt exception to all the threads, effectively the same as using the "f" option in the default handler.
I removed the "s" option from the handler since ultimately this depended on the old "Process" mechanism for parallelism. The alternative top-level shell worked by having a second list of runnable processes and the effect of typing "s" in the control-C handler was to switch between these. With the current thread mechanism the run queue is handled by the kernel so this didn't really make sense and I couldn't see how to handle sub-shells with the new mechanism.
The other problems are to do with the way signals are handled when there are multiple threads. Even if there is only a single ML thread and the Thread structure is not used Poly/ML is actually running at least two threads. The "main thread" is responsible primarily for garbage collection and is normally blocked waiting the ML code, which runs on a separate thread. When control-C is pressed the operating system sends the SIGINT to one of these threads. In Mac OS X, in particular, it always sends the signal to the main thread. The ML thread continues to run in parallel.
While I was writing this I realised that there was a possible solution to the problems that this created and which you noticed. Previously the handler for SIGINT actually ran the loop that read from the terminal and looked at the "f", "c", "q", "t" etc codes. I've now changed this so that when SIGINT arrives it simply sets a flag. Some time later one of the ML threads (which one is indeterminate) runs the default console interrupt handler if an alternative one has not been set up. This allows the "t" (traceback) option to work since it is actually running on an ML thread. It also avoids the race conditions that arise if both the interrupt handler and the ML code are reading from the terminal at the same time, but only if the thread that runs the interrupt handler is the same as the one reading from the terminal. That will, of course, be the case if there is only one ML thread.
This is still quite messy. I would prefer to get rid of the default interrupt handler that reads from the terminal altogether and switch to requiring the user to set up a handler for SIGINT using the Signal structure.
Regards, David.
Rob Arthan wrote:
David,
Thanks for the prompt fix. In fact, I should confess that my current approach in ProofPower only uses the length of the hierarchy list and not the values of the strings in it, so I don't actually need the fix at the moment.
ProofPower now builds and tests on Poly/ML 5.1 on both Linux and Mac OS X, but I have some problems with keyboard interrupts. First of all two comments, I note that the s(witch) command is no longer available and it seems as if the t(race) command is never able to print a trace.
On both OSs the f(ail) and q(uit) command seem to behave differently from 4.2.0. There is also a separate problem on Mac OS X when an interrupt arrives while poly (or my executable with the read-eval-print loop tailored for ProofPower) is waiting for input rather than excecuting a function. I need to do some more investigation into the common problem, so the rest of this e-mail is about the Mac OS X-specific problem. (As I am using Mac OS X version 10.3.9 which is a bit long in the tooth, I am wondering whether Poly/ML 5.1 just isn't supported on it).
Here is the sort of thing that happens (this is copied out of Terminal with "\n"s added by me to show where I had to hit return to make something happen):
rda]- poly Poly/ML 5.1 Release
^C
=>?\n # ;\n Error: Value or constructor (?) has not been declared Found near ?
Static errors (pass2)
^C\n
^D\n
=>?\n Type q(uit - Exit from system) c(ontinue running) f(ail - Raise an exception) or t(race - Get a trace of calls) =>rda]-
On the last line of the above, I didn't type anything: the "=>" prompt appeared and I just waited a few seconds and then poly exited (which would also have happened if I hadn't typed the second "?" fairly quickly). It feels as if there are two separate threads responding to keyboard gestures in an uncoordinated way.
Regards,
Rob.