-*- outline -*- * Known Bugs and Workarounds for Proof General. Contact: mailto:da+pg-bugs@inf.ed.ac.uk For latest, see: http://proofgeneral.inf.ed.ac.uk/BUGS See also FAQ: http://proofgeneral.inf.ed.ac.uk/FAQ Generic bugs are listed here, which may affect all of the supported provers. See lego/BUGS coq/BUGS, etc, for specific bug lists for each of the provers supported. The bugs here are split into problems which apply for all Emacs versions, and those which only apply to particular versions. NB: some issues which affect PG but which are not necessarily bugs in PG are mentioned in the FAQ. * Reporting bugs If you have a problem that is not mentioned here, please contact me at the address above. Please describe your problem carefully, include a short demonstration file and tell me the exact version of Emacs and Proof General that you are using. You can use the menu command Proof General -> Help -> Send Bug Report to conveniently include the proper version numbers in your message. * Generic problems, for all Emacs versions ** X-Symbol support removed from "secondary" provers (HOL, ACL2, LEGO, Twelf) If anyone was actually using this, please let me know. It should be very easy to revive by copying coq/x-symbol-coq.el (although a generic version might be desirable). ** Visibility control doesn't distinguish theorems with same name. If you have more than one theorem with the same name in a buffer, their proof visibilities are controlled together. ** If the proof assistant goes into a loop displaying lots of information It may be difficult or impossible to interrupt it, because Emacs doesn't get a chance to process the C-c C-c keypress or "Stop" button push (or anything else). In this situation, you will need to send an interrupt to the (e.g.) Isabelle process from another shell. If that doesn't stop things, you can try 'kill -FPE '. This problem can happen with looping rewrite rules in the Isabelle simplifier, when tracing rewriting. It seems to be worse on certain architectures, and slower machines. Behaviour seems better on Emacs than XEmacs. ** Glitches in display handling, esp with multiple frames Unfortunately the handling of the display is very difficult to manage because the API provided by Emacs is quirky, buggy, and varies between versions. If the eager display/tear-down of frames is annoying you, you may customize the variable `proof-shell-fiddle-frames' to nil to reduce it a bit. To prevent eagerly displaying new frames at on starting the shell, you can also add a mode hook to set `proof-eagerly-raise' e.g.: (add-hook 'proof-goals-mode-hook (lambda () (setq proof-eagerly-raise nil))) (add-hook 'proof-response-mode-hook (lambda () (setq proof-eagerly-raise nil))) This causes the previous behaviour as in PG 3.4: frames are only created as text is displayed in them. (This is the default for the trace buffer). Generally, the best way of working with multiple frames is to try not to stop/start the proof assistant too much (this involves killing buffers, which spoils the frame/buffer correspondence). If you find other particularly annoying behaviour, please do report it, but give a careful description of how to reproduce, what happened, and what you expected to happen. Probably you will just have to work around the issue. For future versions of PG the multiple frame handling code will probably be custom written (rather than using `special-display-regexps'). ** Toolbar enablers unreliable on some platforms. Occasionally the buttons are disabled/enabled when they shouldn't be. An extra click on the toolbar may solve this. If you have problems, please customize `proof-toolbar-use-button-enablers' to nil to disable the enablers. ** Using C-g can leave script management in a mess (rare). The code is not fully protected from Emacs interrupts. Workaround: Don't type C-g while script management is processing. If you do, use proof-restart-scripting to be sure of synchronizing. ** Outline-mode does not work in processed proof script files Because of read-only restrictions of the protected region. This is an inherent problem with outline because it works by modifying the buffer. Workaround: none, nevermind. (If it's hugely needed we could support modified outline commands). ** When proof-rsh-command is set to "ssh host", C-c C-c broken The whole process may be killed instead of interrupted. This isn't a bug in Proof General, but the behaviour of ssh. Try using rsh instead, it is said to forward signals to the remote command. ** In tty mode, the binding C-c C-RET has no effect. Workaround: manually bind C-c RET to 'proof-goto-point instead. ** Multiple file scripting is slightly vulnerable. Files are not locked when they are being read by the prover, so a long file could be edited and saved as the prover is processing it, resulting in a loss of synchronization between Emacs and the proof assistant. Files ought to be coloured red while they are being processed, just as single lines are. Workaround: be careful not to edit a file as it is being read by the proof assistant! * Problems with particular Emacs versions ** General note: PLEASE CHECK YOUR EMACS IS UP TO DATE Most of the issues below relate to old Emacs versions. Proof General is already chock-full of patches for Emacs bugs, it's time to start removing these kludges rather than adding more. Feel free to report a bug which may be Emacs-related: from now on I will add a note here rather than try to investigate older Emacsen and add more patches to the code. ** XEmacs "nesting too deep for parser" warnings (unresolved in any XEmacs) This is sometimes triggered by very complex output, typically with Isabelle's tracing messages when font-lock is called. XEmacs implementation of parse-partial-sexp appears at fault. It gives this error message when nesting depth reaches 100. With GNU Emacs, a nesting depth of 40000 or more is possible. Some error handling has been added in the code to cope with this condition. If you notice the disappearance of correct syntax highlighting in the response buffer when large output with unbalanced parentheses is produced, this error may be the cause. You can clear the response buffer by hitting "c" when it is selected. ** XEmacs font-lock problem in certain versions of XEmacs 21.4 When reloading (with C-x C-f) an already loaded script file that has been changed on the file system you see the error: (1) (warning/warning) Error caught in `font-lock-pre-idle-hook': (wrong-type-argument markerp nil) As a result fontification, etc, fails. Workaround: use C-x C-v instead. This problem has gone away since 21.4.12 or so. Update: this has reappeared in version 21.4.15. ** GNU Emacs menus: options not updated dynamically, positions erratic, etc. Also, proof assistant specific menus only appear in scripting buffer. These are drawbacks with GNU Emacs menu support on early versions. As of Emacs 21.3, these glitches have gone. (Although bugs have been known to return). ** GNU Emacs faces sometimes faulty, esp in console mode Emacs support is let down in console mode, because faces are not implemented there. (XEmacs can use colours and underline in console mode) ** If you have problems using Mule versions of GNU Emacs Beware setting standard-display-european: Pascal Brisset suggests adding this line to .emacs should help: (setq process-coding-system-alist '(("" . no-conversion))) ** XEmacs undo in the script buffer can edit the "uneditable region" Test case: Insert some nonsense text after the locked region. Kill the line. Process to the next command. Press C-x u, nonsense text appears in locked region. Workaround: take care with undo in XEmacs. ** X-Symbol on GNU Emacs X-Symbol 4.X isn't finished yet and will only supported GNU Emacs from GNU Emacs 21.4 onwards. For the time being there are a few minor glitches (buffer gets modified during decoding, subscripts/superscripts don't work, output colouration may spill into adjacent symbols...), but on the whole it is quite usable (and rather faster than XEmacs). For more information about X-Symbol, see http://x-symbol.sourceforge.net. ** As of GNU Emacs 20.3, multi-byte character codes are used. This breaks some of the code in Proof General, which is turned off in case the suspicious looking function toggle-enable-multibyte-characters is present. The code that is turned off deals with term markup for proof by pointing, which only affects LEGO at the moment. This problem could affect forthcoming versions of XEmacs (but hasn't as far as XEmacs 21.4). [Can anybody tell us if it affects Mule versions of Emacs?] Workaround: for LEGO pbp, use GNU Emacs 20.2, or XEmacs 20.4/later. ** XEmacs sometimes has strange start-up delays of several seconds. Possibly due to face allocation, when running remotely and displaying on an 8-bit display. One workaround (and in fact the recommended way of working) is to run XEmacs locally and only the proof assistant on your fast compute server, by setting proof-rsh-command. ** Looping in Emacs 21.2 Several (odd) circumstances cause this version of Emacs to loop, in particular, when moving the cursor into multi-byte characters. Workarounds have been added to avoid this: you may see junk characters in the shell buffer as a side effect.