Proof General Stops Loading

[Chobbes]

I'm having this problem where occasionally proof general will stop loading for some files. It's hard to reproduce, but it often seems to happen when using helm-projectile to find new coq files to open. I.e., files which emacs did not have loaded into a buffer already, though I'm pretty sure this has also happened with helm-find-files. But this doesn't always happen.

Running coq-mode manually does not help either, the file stays in Fundamental mode. I've used debug-on-entry with coq-mode when this happens and found that the check that fails is in proof-site.el. It's some check that proof-assistant isn't already bound. I made a change to allow myself to force coq-mode to load anyway:

Chobbes@0115ca4

I don't think this is a proper fix, though, and I'm not really sure why this check is there to begin with so I'm nervous about doing this 😰. Also this causes this message to pop up when loading coq-mode sometimes.

helm-M-x: Macro defpacustom: Proof assistant setting auto-adapt-printing-width re-defined!

And then the buffer is still left in Fundamental mode, but calling coq-mode again works.

Do you have any idea what could be going on? I usually have some buffer with the proofs loaded about half way open, maybe some org-mode coq buffers, and some helm / helm projectile stuff going on for finding files. Maybe one of those things is interacting badly?

[Chobbes]

This just happened to me again with a freshly loaded emacs. It seems to have something to do with the fact that proof general loads for coq files in org-mode, because nothing else would have used proof general before I loaded the coq file.

[Matafou]

Sorry I didn’t get your point. What do you think org-mode has to do with?

[Chobbes]

I have a bunch of source blocks with coq code in my org files. org-mode opens these source blocks in ephemeral buffers with proof general, and I think this might be causing PG to set the proof-assistant inappropriately / get into some state that it shouldn't.