Proof General immediately starts processing the file as soon as I open it

[megacz]

Proof General immediately starts processing my script as soon as I open it in Emacs (and enter proof-mode). I do not want this; some of my proofs cause Coq to crash or hang instantly upon loading, and once it crashes/hangs the region that caused the problem is locked. Please tell me how to disable this behavior.

[megacz]

Here is some more information....

I have the following lines in my .emacs file:

(add-hook 'proof-mode-hook (lambda ()

(define-key proof-mode-map "\C-c\C-a" 'proof-retract-until-point-interactive) ))

If I remove them, PG no longer immediately starts processing my script as soon as I open it. Is this to be expected?

[David Aspinall]

I can't reproduce this, even adding your key binding.

It sounds like you have inadvertently turned on the new "automatic sending" feature, see here:

http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-latest/doc/ProofGeneral/ProofGeneral_4.html#Automatic-processing

This can be turned on and off with the key "C-c >". Perhaps something else is going wrong with your key bindings to mix these up somehow? Check also that you haven't saved the customize option (look for proof-autosend-enable in .emacs).

Please reopen if you still find there's a problem.

[megacz]

Nope, the bug is definitely there. It occurs even if these are the ONLY lines in my .emacs file (everything else is gone)

(load-file "/opt/local/share/ProofGeneral/generic/proof-site.el") (add-hook 'proof-mode-hook (lambda ()

(define-key proof-mode-map "\C-c\C-a" 'proof-retract-until-point-interactive) (proof-electric-terminator-toggle t) (set-process-query-on-exit-flag (get-buffer-process (proof-process-buffer)) nil) ))

Removing the second-to-last line seems to help. But that shouldn't have any effect.

Try this using tty emacs and a PG4.0 installation based on my Portfile to replicate what I'm seeing.

[David Aspinall]

Yes, I can repeat the effect with your .emacs, but it is buggy. In particular, you are calling proof-process-buffer which is a function that processes the buffer! So no wonder you are seeing the buffer getting processed as soon as proof mode is engaged.

Your customization should look like this instead:

(load-file "/opt/local/share/ProofGeneral/generic/proof-site.el")

(add-hook 'proof-mode-hook
          (lambda ()
            (define-key proof-mode-map "\C-c\C-a"
              'proof-retract-until-point-interactive)
            (proof-electric-terminator-toggle t)))

(add-hook 'proof-shell-mode-hook
          (lambda ()
            (set-process-query-on-exit-flag
             (get-buffer-process (current-buffer)) nil)))

[megacz]

Clearly I am not cut out for programming in languages with side effects.