Stuck at "Retracting buffer" after type class resolution diverges

Question

When using typeclasses, Coq sometimes diverges. When this happens under Proof General, Emacs also hangs.

The best way I know to recover is to interrupt emacs (C-g) and restart Coq (C-c C-x). But, instead of just killing the Coq process, this puts me in a mode where Emacs is again hung, displaying "Retracting buffer..." for a quite long time (sometimes so long that I give up and just start a whole new emacs!).

Why?

Is there a better way? (And: Is there an easy first step for viewing what is diverging in the first place when this happens?)

Answer 1

If emacs is hung on anything other than garbage collection, you can generally interrupt it with C-g. If C-c C-x / C-c C-c don't work, you can kill the coqtop process from process manager / from the command line with pkill coqtop.

This happens because coqtop has some loops where it does not check for interrupt, or does not check often enough, and so it does not catch the interrupt from PG in a timely manner.

Additionally, as mentioned in other answers, Set Typeclasses Debug will give you a very verbose log of typeclass resolution in the *response* and *coq* buffers.