From 84ebc40061e1ce380210691618b70773cc1ff713 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 31 Aug 2009 20:01:03 +0000 Subject: Merge in Isar and Coq bugs --- BUGS | 53 +++++++++++++++++++++++++++++++++-------------------- coq/BUGS | 20 -------------------- isar/BUGS | 21 --------------------- 3 files changed, 33 insertions(+), 61 deletions(-) delete mode 100644 coq/BUGS delete mode 100644 isar/BUGS diff --git a/BUGS b/BUGS index c90c33dc..d6df20f6 100644 --- a/BUGS +++ b/BUGS @@ -5,14 +5,10 @@ For latest, see: http://proofgeneral.inf.ed.ac.uk/trac 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 a few specific bugs. +The bugs here are split into problems which are generic, +and those which only apply to particular provers. -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. +The FAQ mentions other issues which are not necessarily PG bugs. * Reporting bugs @@ -22,7 +18,7 @@ problem carefully, include a short demonstration file and tell us the exact version of Emacs and Proof General that you are using. -* Generic problems, for all Emacs versions +* Generic problems ** Visibility control doesn't distinguish theorems with same name. @@ -102,23 +98,40 @@ 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! +** 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. -* Problems with particular Emacs versions -** General note: PLEASE CHECK YOUR EMACS IS UP TO DATE +* Problems with Isabelle -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. +** Issues with tracing mode -** Undo in the script buffer can edit the "uneditable region" +Large volumes of output can cause Emacs to hog CPU spending +all its time processing the output (esp with fontifying and X-symbol +decoding). It becomes difficult to use normal editing commands, +even C-c C-c to interrupt the prover. Workaround: hitting C-g, +the Emacs quit key, will interrupt the prover in this state. +See manual for further description of this. -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. + +* 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. + +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. + + +* LEGO Proof General Bugs + +See lego/BUGS diff --git a/coq/BUGS b/coq/BUGS deleted file mode 100644 index 6599180a..00000000 --- a/coq/BUGS +++ /dev/null @@ -1,20 +0,0 @@ --*- mode:outline -*- - -* Coq Proof General Bugs - -See also ../BUGS for generic bugs. - -** 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. - -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. - -** Others not mentioned... - -Please report further issues at http://proofgeneral.inf.ed.ac.uk/trac - diff --git a/isar/BUGS b/isar/BUGS deleted file mode 100644 index 11564906..00000000 --- a/isar/BUGS +++ /dev/null @@ -1,21 +0,0 @@ --*- mode:outline -*- - -* Isabelle/Isar Proof General Bugs - -See also ../BUGS for generic bugs. - -** Issues with tracing mode - -1. Large volumes of output can cause Emacs to hog CPU spending -all its time processing the output (esp with fontifying and X-symbol -decoding). It becomes difficult to use normal editing commands, -even C-c C-c to interrupt the prover. Workaround: hitting C-g, -the Emacs quit key, will interrupt the prover in this state. -See manual for further description of this. - -2. Interrupt response may be lost in large volumes of output, when -using pty communication. Symptom is interrupt on C-g, but PG thinks -the prover is still busy. Workaround: hit return in the shell buffer, -or set proof-shell-process-connection-type to nil to use piped -communication. - -- cgit v1.2.3