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
|
-*- mode:outline -*-
* Isabelle Proof General Bugs
See also ../BUGS for generic bugs.
** 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'.
|
