The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hello,

I'm wondering if someone can give me some pointers on how to interact with coqtop from another program. If I run coqtop from the console and I press Cntrl+C, coq traps the error and prints "User Interrupt", but if I open the process using python and send it sigint (what is the effect of Cntrl+c) it kills the process.

p = subprocess.Popen(['coqtop.opt', '-emacs'],

                     stdin=subprocess.PIPE)

p.stdin.write('Goal True.\n')

p.stdin.flush()

p.stdin.write('auto.\n')

p.stdin.flush()

p.stdin.write('Qed.\n')

p.stdin.flush()

p.send_signal(2)

p.wait()

If I comment out the send_signal line then I get what I expect; but with the send_signal line, the process is killed and p.wait() returns with an error saying that there is no process running for p. I looked at the proof-general code and it seems to just be calling '(interrupt-process)' which supposedly just sends signal 2.

Thanks.

--
gregory malecha