Email Gateway (Aug 18 2022 at 10:38): Email Gateway (Aug 18 2022 at 10:38):From: Florian Funke <funke@informatik.uni-tuebingen.de>
Hi all,
I'm working on a program that starts Isabelle and communicates with the
Isabelle process (in Isar interaction mode) using its standard output and
input stream. Now I'd like to be able to cancel commands I've sent to
Isabelle (e.g. because their execution doesn't terminate). The
ProofGeneral seems to have this capability and uses
comint-interrupt-subjob in the proof-interrupt-process function. But when
I try to send a SIGINT signal to the isabelle-process, it doesn't have any
impact, however sending SIGINT to the poly process that isabelle starts
("poly-driver") manually, causes Isabelle to cancel the execution of the
current command (which is what I'm trying to do from within my program).
This is a problem, since I do not have a chance to get the process ID of
this poly-driver process that Isabelle spawns and therefore cannot send
signals to it (I do have Isabelle's PID, of cause). In the Isabelle System
Manual, I couldn't find out if there is a way to send signals to the
Isabelle process directly, neither how the ProofGeneral deals with this
problem.
-- Florian
Email Gateway (Aug 18 2022 at 10:38):From: Makarius <makarius@sketis.net>
Peeking at comint.el reveals that emacs signals the whole process group of
the controlling pty here. I've managed to imitate this behaviour in the
shell using kill with negated PID like this:
kill -INT -- -4711
Also note that the Isabelle/Isar toplevel ignores any INT signals unless
it actually runs a command. To test kills more easily you may use the raw
ML toplevel, which reports something like ``Compilation interrupted''.
Makarius
Email Gateway (Aug 18 2022 at 10:39):From: "Mark A. Hillebrand" <mah@dfki.de>
Hi Florian,
I have made the same observation when writing a similar program; I use
Perl with the Expect.pm library to remote-control Isabelle. While
sending SIGINT does not come through to Isabelle (maybe it gets stuck in
lib/scripts/feeder.pl, but I haven't investigated closely), sending a
control-C character seems to interrupt the Isabelle process. Here is a
short example:
#!/usr/bin/perl
use Expect;
my $isabelle = Expect->new();
$isabelle->spawn('/usr/local/Isabelle/bin/isabelle', 'HOL' );
#$isabelle->raw_pty(1);
$isabelle->log_file("log.txt");
#$isabelle->log_stdout(1);
#$isabelle->exp_internal(1);
$isabelle->send(qq(use_thy "~~/HOL/Library/Word";\n));
sleep 1; # keep loading for a bit
$isabelle->send("\cC"); # interrupt
sleep 1; # wait another bit
$isabelle->send("quit();\n");
$isabelle->soft_close;
(Be aware that this program doesn't really synchronize with Isabelle
prompts etc. but it should).
Hope this helps
Mark
Last updated: May 03 2024 at 12:27 UTC