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
|
-*- mode:outline -*-
* Isabelle 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.
** set proof_timing is problematic
It will make the goals display disappear during proof. This is
because Proof General only displays goals output that appears *after*
Isabelle messages, but Isabelle prints the timing message after the
goals are displayed.
** General difficulty with proof scripts containing ML structures, etc.
Proof General does not understand full ML syntax(!), so it will be
confused by structures which contain semi-colons after declarations,
for example. Also, it cannot undo function declarations. See the
section on ML files in the manual for more details.
** 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.
** Subsection Interaction with theory database
Isabelle Proof General uses some support from Isabelle to remove and
reload theories from the theory database. To maintain consistency,
Isabelle is rather conservative. So re-asserting a retracted file will
often re-load it, even if it has not changed. (This is because the
file may have implicit dependencies on things in the global ML
environment not made apparent by the theory structure).
This may lead to seemingly unnecessary repetition of time-consuming
proofs, so be careful not to retract more than you need!
As of Isabelle 99-1 and Proof General 3.2, there should be much
less unncessary re-loading of theories; be careful to use Isabelle's
mechanisms of declaring dependencies in theory file headers.
** Clash with SML mode
Since Isabelle proof scripts are not differentiated from `.ML' files,
Proof General may compete with `sml-mode' (if you use it) for
controlling these buffers. To ensure Proof General wins, load it last.
Workaround: use another extension for real ML files, e.g. `.sml',
and disable `.ML' from entering `sml-mode'.
|
