Re: [isabelle] Interrupt Isabelle with signal

Hi Florian,

On Wed, Jul 11, 2007 at 05:30:53PM +0200, Florian Funke wrote:
> 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).

  I have made the same observation when writing a similar program; I use
Perl with the library to remote-control Isabelle. While
sending SIGINT does not come through to Isabelle (maybe it gets stuck in
lib/scripts/, but I haven't investigated closely), sending a
control-C character seems to interrupt the Isabelle process. Here is a
short example:

    use Expect;

    my $isabelle = Expect->new();

    $isabelle->spawn('/usr/local/Isabelle/bin/isabelle', 'HOL' );


    $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


  (Be aware that this program doesn't really synchronize with Isabelle
prompts etc. but it should).

  Hope this helps


Dr. Mark A. Hillebrand
German Research Center for Artificial Intelligence
Saarbruecken, Germany
Building E1 1, Room 4.06
Phone: +49 (0)681 302 57379    Fax: +49 (0)681 302 4290
Email: mah at

Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH Trippstadter
Strasse 122, D-67663 Kaiserslautern, Germany

Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff

Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes

Amtsgericht Kaiserslautern, HRB 2313

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.