diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-12-11 12:30:32 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-12-11 12:30:32 +0000 |
| commit | b6844dcb873d17f980886b3e9e3ee09896ffa2f3 (patch) | |
| tree | 94ccc201aad66ab2e9afed61a8f1f31932833cb9 /BUGS | |
| parent | df09ad8168164e4235c70898f88ecd05149a2b3c (diff) | |
Removed multiple provers problem, it's handled gracefully now and not a bug.
Diffstat (limited to 'BUGS')
| -rw-r--r-- | BUGS | 23 |
1 files changed, 9 insertions, 14 deletions
@@ -36,30 +36,24 @@ 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. -* You can't use more than one proof assistant at a time in the same -Emacs session. Attempting to load Proof General for a second prover -will fail. Workaround: stick to one prover per Emacs session, -make sure that the proof-assistants variables only enables -Proof General for the provers you need. - * 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 obscure bug with processes on Solaris which results in -buffers full of ^G after certain combinations of input. Workaround: -get a patch from Sun, or use Linux. +buffers full of ^G after certain combinations of input. +Workaround: get a patch from Sun, or use Linux. -* XEmacs sessions perhaps grow excessively in terms of memory +* 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.) -*`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. - FSF Emacs specific bugs ======================= @@ -69,6 +63,7 @@ FSF Emacs specific bugs commas are not zapped. However, when entering text, commata are zapped correctly. Workaround: don't stare too much at commata + LEGO Proof General Bugs ======================= @@ -78,7 +73,7 @@ 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 issues are local definitions in a proof state. LEGO cannot +* A thorny issue is local definitions in a proof state. LEGO cannot undo them explicitly. Workaround: retract back to a command before a definition. |