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 ================ * Ordinary undo in 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. * 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. Workaround: use other means to navigate in a proof scipt buffer. * 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. * 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: Is this bug still present? Please tell us if you think so.) 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.