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
|
-*- 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)
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
*** Separate README and BUGS files for each supported prover
Check these files for detail of support and issues with each prover.
*** Names of shell, goals, script buffers now based on proof assistant name
Basing the name on the command isn't very abstract and leads to strange
names for some provers, "coqtop" and "hol.unquote". Now we just use
the lower case of the proof assistant name.
*** Fixes for supporting Japanese versions of Emacs which have older CL macs.
Probs 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.
*** Minor bug fix for duplicated short output.
Only seen with "val x=1" or similar messages.
We now set proof-shell-eager-annotation-start-length appropriately.
*** Bug fix with .thy files and X-Symbol mode
Subsequently visited theory files would have X-Symbols broken.
*** Bug fix for (non-mule) FSF Emacs 20.5.
Emacs would freeze when starting proof assistant due to character
matching problem.
*** 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.
*** 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.
*** Minor cosmetic improvements
Name of proof assistant "Start Isabelle" etc. in menu.
** Coq Changes
** 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
** Isar Changes
*** Syntax tweaks.
** Changes for developers to note
*** todo files added for each prover (todo split from global todo).
|
