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 script buffers in recent versions of FSF Emacs is a mess. The underlying text property implementation has changed and it seems difficult to get the desired behaviour of highlighting now. Workaround: switch to using XEmacs. * If you use C-x C-v or C-x C-w on a script file which is in active scripting mode, Proof General will lose track of the file. Workaround: always turn off active scripting first with C-c C-s. * Toolbar enablers for XEmacs 21: since these have been switched on, it is apparent that the recognition of completed proofs may be unreliable (it wasn't used before). Also there is a timing issue, so that occasionally the buttons are disabled/enabled when they shouldn't be. An extra click on the toolbar solves this. * Synchronization during start-up: if you press C-c C-n quickly in succession whilst the prover is cranked up, synchronization may be spoilt, and you see the message "script management confused" later on. This is a minor bug, most likely to be noticed when it takes a while to start the proof assistant (e.g. Isabelle!). Workarounds: many! Type slowly. Use C-c C-RET. Start the prover first via the menu, or C-c C-s. * 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. 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.1). Can anybody tell me if it affects Mule versions of Emacs? Workaround: for LEGO pbp, 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 processed proof script files due to 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). * 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. * 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. * In tty mode, the binding C-c C-RET has no effect. Workaround: manually bind C-c RET to 'proof-goto-point instead. LEGO Proof General Bugs ======================= * PBP doesn't work on FSF, see note above. * [FSF specific] `proof-zap-commas-region' does not work for Emacs 20.2 on lego/example.l . On *initially* fontifying the buffer, commas are not zapped [unfontified]. However, when entering text, commata are zapped correctly. Workaround: don't stare too much at commata * 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. * Surely others that aren't mentioned here. Please report them to proofgen@dcs.ed.ac.uk. 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 as scripting is turned on. To avoid this, assert the theory file rather than the ML file. Isabelle and Isabelle/Isar Proof General Bugs ============================================= * We've heard from one user that there are problems using Proof General with Isabelle compiled under MLWorks for Sun Ultra/Solaris2.7. These may be to do with the piped communication mechnism; perhaps MLWorks doesn't flush the output after printing prompts. If anyone discovers this, a possible work-around is to set process-connection-type to t instead of nil in proof-shell.el. Please report to proofgen@dcs.ed.ac.uk if you try this!