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 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

-- 
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 dfki.de

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

Geschaeftsfuehrung:
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.