blob: 395e67d43b4ccb0a6ac2116439ac9b50abb26508 (
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
|
Dear Proof General users,
This is a newsy note to tell you that Proof General 3.0 is ready for
release Very Soon Now. In the meantime, I'd be very grateful to
anyone who can test a pre-release and tell me how it goes. (I try to
do as much testing as I can, but it's getting more difficult as more
proof assistants are supported).
I'm quite excited about this release. I've concentrated on usability,
making the code clean and robust, and making PG easier to adapt for
new proof assistants. But there are some important new features too...
David von Oheimb's patches for X-Symbol have been made generic now,
and easy to turn on and off. I've added some basic support for Coq
and LEGO, so Greek letters and symbols like /\ and -> display as you
would like. Break free from ASCII!
Proof-by-pointing has been resurrected! The interface relies on the
proof assistant to construct the proof commands, and the only prover
supported currently LEGO. One reason PBP was disabled was that LEGO's
implementation is experimental and incomplete. But I hope that people
can see PBP almost working in LEGO and be encouraged to implement it
for other provers. We can certainly hope for support in Coq, since
the CtCoq proof-by-pointing code has been moved into the Coq kernel
now. I hope the Coq community can encourage somebody to do this.
Visit http://zermelo.dcs.ed.ac.uk/~proofgen/ for more.
Best regards,
- David.
|
