BUGS in latest version of Proof General
This is a flattened outline file: click on a title to hide/reveal the leaf underneath it.
Click here to show whole body, or here to hide whole body.
Known Bugs and Workarounds for Proof General.
If the proof assistant goes into a loop displaying lots of information
Glitches in display handling, esp with multiple frames
Using C-g can leave script management in a mess (rare).
When proof-rsh-command is set to "ssh host", C-c C-c broken
In tty mode, the binding C-c C-RET has no effect.
Prover does not lock/may not notice dirty files
Problems with Isabelle
Issues with tracing mode
Problems with Coq
Multiple file handling and auto-compilation is incomplete
C-c C-a C-i on long intro lines breaks line the wrong way.
coqtags doesn't find all declarations.
LEGO Proof General Bugs
Click here to go back to the front page.
Web pages by
Please report issues
on PG trac.
Last modified 21 December 2017.