blob: 9131d56bbb79ad690a5864d54548edf88a04a4d7 (
plain)
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
|
<p>
<!-- da: Put this line in instead if you're not me -->
<!-- <i>(News items entered by <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a> -->
<!-- unless noted.)</i> -->
<i>News items by <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.</i>
</p>
<ul>
<li><b>10th March 2000</b>
<p>
New: <b>HOL Proof General</b>!
It took me only a couple of hours to add a basic instantiation of
ProofGeneral for <a href="http://www.cl.cam.ac.uk/HVG/HOL/HOL.html">HOL98</a>.
Most of this time was in trying to find out how to do things in HOL,
I could have done with a HOL user to hand. But I thought it was high time
HOL got a look-in.
</p>
HOL Proof General provides script management support, automatic
multiple files, decoration of proof scripts and output.
Character-sequence X Symbols as in Coq and LEGO. Although this is a
basic feature set for Proof General, the result is still an enormous
improvement over shell interaction.
</p>
<p>
My hope is to entice HOL users so that one of them may improve HOL
Proof General. I don't plan to maintain or seriously improve this
instantiation myself.
</p>
<p>
The HOL support is shipping in the
current <a href="develdownload.phtml">development release</a>.
</p>
<li><b>15th February 2000</b>
<p>
There is now a new
<?php link_root("devel","page for developers") ?>.
I plan to apply for funding to continue managing the evolution
and development of Proof General, once my own job position
is more secure.
Now is the time to flesh out ideas
for the future!
Check the development page for the
latest proposals. These include some desirable contributions
which could be undertaken as self-contained projects.
</p>
<li><b>9th February 2000</b>
<p>
Countdown to Proof General 3.1 begins. This will be a bug fix releaase.
A few bugs have been fixed in
recent Proof General development releases, one important one is fixing
support for non-mule versions of FSF Emacs (thanks to Pierre Courtieu
for raising it to my attention). I would like to release PG 3.1 next
month so that everyone can benefit.
</p>
<p>
In the meantime, please
<?php
hlink("feedback.phtml","report any important problems ","Feedback form")?>
that you would like to see fixed, and consider trying out
the current <a href="devel.phtml">development release</a>.
</p>
<li><b>14th December 1999</b>
<p>
I'm pleased to say that Proof General will be demonstrated at
<a href="http://iks.cs.tu-berlin.de/etaps2000/etaps.html">ETAPS 2000</a>.
Here are some draft <a href="papers/pgtalk.pdf">slides</a> for
the presentation
(any <a href="mailto:da@dcs.ed.ac.uk">comments</a> would be welcome).
A presentation of Proof General based on these slides was given at
<a href="http://www.clrc.ac.uk/">Rutherford Appleton Laboratory</a> last week.
</p>
<li><b>26th November 1999</b>
<p>
Proof General 3.0 is released!
</p>
</ul>
<p>
<i>Click <a href="oldnews.phtml">here</a> for old news.</i>
</p>
|
