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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
-*- outline -*-
* Summary of Changes for Proof General 3.1 from 3.0
** New instantiations of Proof General!
*** HOL 98 (http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html)
by David Aspinall. This is a fairly basic Proof General instance
only, hopefully to entice HOL users so that one of them may improve it.
I don't plan to maintain or improve this instantiation myself.
(Nevertheless, please report problems as usual to proofgen@dcs.ed.ac.uk)
See README in the hol98 directory for more details.
*** Plastic (http://www.dur.ac.uk/CARG/plastic.html) (ongoing work)
by Paul Callaghan <P.C.Callaghan@durham.ac.uk>.
The Plastic system itself is not yet publicly available,
so this is only included in the developers tar file.
** Generic Changes
*** Added key binding C-c C-BS and menu entry for delete last command
This restores the old function of the sequence "C-u C-c C-u" onto
a safer key. In version 3.0 it was only available via
control-button2 in the goals buffer. The function invoked is
`proof-undo-and-delete-last-successful-command'.
*** Separate README and BUGS files for each supported prover
Check these files for detail of support and issues with each prover.
*** Fixes for different Emacsen compatibility
**** Supporting Japanese versions of Emacs which have older CL macs.
Problems occurred with CL macs with Japanicised documentation,
defined in "egg.el".
Japanese Emacs users, please report any other problems you find,
they may be fixable for similar reasons. Better still, report these
compatibility problems also to the Japanese Emacs developers, I
don't know who to contact.
**** Bug fix for (non-mule) FSF Emacs 20.5.
Emacs would freeze when starting proof assistant due to character
matching problem.
**** Fixes for XEmacs on Windows.
Toolbar now enabled when console-type=mswindows.
*** Fix for infamous Solaris ^G problem: proof-shell-process-connection-type
A user (or proof assistant configuration) can now specify whether
to use pty or piped communication. This is to fix the problem that
Solaris users have (because of a Solaris bug), when lots of ^G's
appear.
The default setting for proof-shell-process-connection-type is made
by calling uname, if possible. If this contains "sun"
then proof-shell-process-connection-type is set to nil for using
pipes. Otherwise we use ptys which are to be prefered over pipes
because pipes can become full or lose data, and pipes don't work
which some proof assistants.
If necessary, you can override this by customization, as usual.
*** Minor cosmetic improvements
**** Names of shell, goals, script buffers now based on proof assistant name
Basing the name on the command wasn't very abstract and lead to strange
names for some provers, "coqtop" and "hol.unquote". Now we just use
the lower case of the proof assistant name.
**** Name of proof assistant "Start Isabelle" etc. appears in menu.
*** Minor bug fixes
**** Fix for using electric terminator inside locked region.
With strict read only turned off, would get Emacs error.
Now simply inserts terminator char anywhere in locked region.
[Reported by David von Oheimb]
**** Fix for turning on multiple frame mode
Would trigger error if there was no active scripting buffer.
[Reported by David von Oheimb]
**** Fix for duplicated short output.
Only seen with "val x=1" or similar very short messages.
We now set proof-shell-eager-annotation-start-length appropriately.
[Reported by John Longley]
**** Fixes for filenames with odd characters in them (mainly for Windows)
Fixes to allow filenames with \ and " in them.
Added for Coq, Isabelle, and HOL.
[Reported by Kim Hyung Ho]
**** Fixes for Windows
Solve some bizarre file reading problems (some still remain, buggy XEmacs?)
Add default colours for using in Windows.
** Coq Changes
*** Incomplete handling of Section
Coq PG will now issue Reset commands for sections. This still
doesn't mirror the undo behaviour of sections properly, which
should be treated as atomic, but it means that you can retract
a file with sections in, at least.
** LEGO Changes
*** Fix for error messages, now properly displays "cannot assume" message.
** Isabelle Changes
*** Fix for Poly/ML with interrupts: use proof-shell-pre-interrupt-hook
*** Fix for directory changes under Windows
We use different low-level cd command that understands Windows syntax.
But since Isabelle functions don't understand Windows syntax, we map
backslashes -> forward slashes there.
*** Bug fix with .thy files and X-Symbol mode
Subsequently visited theory files would have X-Symbols broken.
** Isar Changes
*** Syntax tweaks.
*** Fix for Poly/ML with interrupts: use proof-shell-pre-interrupt-hook
*** Fix for directory changes under Windows
** Changes for developers to note
*** todo files added for each prover (todo split from global todo).
*** Added new configuration hook: proof-shell-pre-interrupt-hook
This is added particularly for Isabelle running with Poly/ML,
which requires interaction after an interrupt.
*** Added new customization: proof-shell-filename-escapes
See documentation for details. This was to fix filename substitution
for occasions when Proof General needs to escape some special
characters in the filename. Each prover should set this for
good behaviour with strange filenames (including those of Windows!)
*** for others, see ChangeLog.
|
