search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
488 stars 86 forks source link

Proof General Stops Loading #400

Open Chobbes opened 5 years ago

Chobbes commented 5 years ago

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?

Chobbes commented 5 years ago

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 commented 5 years ago

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

Chobbes commented 5 years ago

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.