I am seeing non-deterministic behaviour in the way keyboard interrupts are handled in the REPL. Some unknown factor seems to be causing some instances of poly to ignore them while other instances do what I would expect:
Here in one terminal window, no matter how long I wait, there is no response to a Ctrl-C:
rda]- poly Poly/ML 5.9.2 Release
([
# ^C
In another terminal window, I see what I would expect:
rda]- poly Poly/ML 5.9.2 Release
([
# ^CCompilation interrupted
I see exactly the same behaviour if I send the signal from another terminal window using kill -INT.
This is all on Mac OS Sequoia 15.3.2. I don’t recall having any problems like this on older releases of Poly/ML say prior to 15.9, though I can’\t say exactly when it started. The behaviour I would expect is very useful as, if you’ve mistakenly copied in some badly formed input, it can be quite fiddly to work out how to continue the input to get back to the top-level prompt of the REPL without accidentally executing something you don’t want to be executed.
Any suggestions?
Rob.