1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
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.
|