Known Bugs and Workarounds for Proof General. ============================================= $Id$ Contact: proofgen@dcs.ed.ac.uk See also: http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS ----------------- Generic problems ================ * Highlighting of locked (blue) and queue (red) regions in FSF Emacs may be unreliable (disappear) in some cases. Cause unknown. If you observe this, please submit a bug report with details of your system and any other information you think may be relevant. Workaround: switch to using XEmacs. * Toolbar enablers for XEmacs 21: since these have been switched on, it is apparent that the recognition of completed proofs is unreliable. Please report cases where the buttons are enabled/disabled at the wrong time. * Ordinary undo in the script buffer can edit the "uneditable region" in XEmacs. This doesn't happen in FSFmacs. 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. * In FSFmacs, when proof-strict-read-only is set and font lock is switched on, spurious "Region read only" errors are given which break font lock. Workaround: turn off proof-strict-read-only, font-lock, or for the best of all possible worlds, switch to XEmacs. * As of FSFmacs 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. This could effect forthcoming versions of XEmacs. Workaround: use FSFmacs 20.2, or XEmacs 20.4/later. * Using C-g can leave script management in a mess. The code needs to have some regions protected from Emacs interrupts. Workaround: Don't type C-g while script management is processing. If you do, use proof-restart-scripting. * Outline-mode does not work in proof script files due to read-only restrictions of protected region. Workaround: none, nevermind. (If it's hugely needed we could support modified outline commands). * `proof-find-next-terminator' (bound to C-c C-e) doesn't work properly. Neither does 'proof-goto-command-start' (C-c C-a). Workaround: use other means to navigate in a proof scipt buffer. * Multiple file handling for Lego and Isabelle 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! * 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. * There is an problem with process communication on Solaris, where there is an input line length limitation for terminals in cooked mode, perhaps to 256 characters. Further input elicits a bell character (^G). This ruins Proof General's parsing of the shell buffer. Future fix: try setting process-connection-type to nil, which instructs XEmacs to use pipes instead of pseudo-terminals for subprocess I/O. (You lose job control of processes you start in shell mode, and some commands (notably ls) behave differently when writing output to a pipe instead of a tty. But using a pipe will allow you to paste arbitrarily long blocks of text into shell mode.) Current workaround: use another OS, e.g. Linux. [1999/08/20: believed to be fixed] * XEmacs sessions maybe grow excessively in terms of memory allocation. Maybe some of the spans aren't removed properly. Setting a limit on the size of the process buffer doesn't seem to help. [1998/10/06: believed to be fixed] * When proof-rsh-command is set to "ssh host" and you issue Ctrl-c to interrupt, 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. FSF Emacs specific bugs ======================= *`proof-zap-commas-region' does not work for Emacs 20.2 on lego/example.l . On *initially* fontifying the buffer, commas are not zapped. However, when entering text, commata are zapped correctly. Workaround: don't stare too much at commata LEGO Proof General Bugs ======================= * If LEGO attempts to write a (object) file in a non-writable directory, it forgets the protocol mechanism on how to interact with Proof General and gets stuck. Workaround: Directly enter "Configure AnnotateOn" in the Proof Shell to recover. * After a `Discharge', retraction ought to only be possible back to the first declaration/definition which is discharged. However, LEGO Proof General does not know that Discharge has such a non-local effect. Workaround: retract back to the first declaration/definition which is discharged. * A thorny issue is local definitions in a proof state. LEGO cannot undo them explicitly. Workaround: retract back to a command before a definition. * Normalisation commands such as `Dnf', `Hnf' `Normal' cannot be undone in a proof state by the Proof General. Workaround: retract back to the start of the proof. * After LEGO has issued a `*** QED ***' you may undo steps in the proof as long as you don't issue a `Save' command or start a new proof. The LEGO Proof General assumes that all proofs are terminated with a proper `Save' command. Workaround: Always issue a `Save' command after completing a proof. If you forget one, you should retract to a point before the offending proof development. *legotags doesn't find all declarations. It cannot handle lists e.g., with [x,y:nat]; it only tags x but not y. [The same problem exists for coqtags] Workaround: don't rely too much on the etags mechanism. Coq Proof General Bugs ====================== * coqtags doesn't find all declarations. It cannot handle lists e.g., with "Parameter x,y:nat" it only tags x but not y. [The same problem exists for legotags] Workaround: don't rely too much on the etags mechanism. * User defined tactics cannot be retracted. Workaround: you may need to retract to the beginning of the proof. Isabelle Proof General Bugs =========================== * General difficulty with complex proof scripts. Since Isabelle uses ML as a top-level language for writing proof-scripts, Proof General may have difficulty understanding scripts which stray too far away from the standard functions, tactics, and tacticals. You will usually notice when a function, or whatever, doesn't get highlighted as you might expect. This probably has no detrimental impact on the interface unless you use your own "goal" or "qed" forms. * Blocking when processing multiple files, beginning from a .ML file. Proof General will block the Emacs process when it is waiting for a theory file (and it's ancestors) to be read. To avoid this, assert the theory file rather than the ML file, or use C-c C-s to start scripting before using one of the assertion commands. * Cut-and-paste from Isabelle output (e.g. goals buffer) is problematic. You will find that this inserts otherwise-invisible special characters into the script buffer, which are used to do the highlighting. If you really need to do cut-and-paste, customize the variable proof-shell-leave-annotations-in-output to nil. Unfortunately this will turn off highlighting.