Proof General Home

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.

Reporting bugs

General issues

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 David Aspinall. Please report issues on PG trac.
Last modified 21 December 2017.