PG
PG copied to clipboard
ProofGeneral
Proof General Stops Loading
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:
https://github.com/Chobbes/PG/commit/0115ca4a11aad3cba5986d120905ca9f3e6de3f3
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 :cold_sweat:. 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?
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.
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.