diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-11-17 14:03:09 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-11-17 14:03:09 +0000 |
| commit | 1f3bc5756940a7d58b32a549624a0fd10d0f52fe (patch) | |
| tree | b02937e063cff927fe710e6d1a39376fd7c78617 /etc | |
| parent | dbc91730ae55b4e118c093b00f2ba1863360ad1e (diff) | |
Updated
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/README | 11 | ||||
| -rw-r--r-- | etc/mailinglist-bait | 28 | ||||
| -rw-r--r-- | etc/testing-log.txt | 4 |
3 files changed, 28 insertions, 15 deletions
@@ -9,9 +9,18 @@ announce Announcement lego Files for testing LEGO Proof General isa Isabelle Proof General isar Isar PG +demoisa Isabelle Demo PG + README this file example test protocol for example proof scripts -notes.txt Misc notes
\ No newline at end of file +notes.txt Misc notes + +debugging-tips.txt Notes on debugging +profiling.txt profiling + +testing-log.txt Notes on tests carried out + +release-log.txt A record of official releases
\ No newline at end of file diff --git a/etc/mailinglist-bait b/etc/mailinglist-bait index 395e67d4..6fa15b9c 100644 --- a/etc/mailinglist-bait +++ b/etc/mailinglist-bait @@ -2,27 +2,27 @@ 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). +anyone who can test a pre-release and tell me how it goes. 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! +David von Oheimb's patches for X-Symbol have been made a proper +generic part of Proof General 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-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. +supported currently is 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. diff --git a/etc/testing-log.txt b/etc/testing-log.txt index 08528479..2010c27f 100644 --- a/etc/testing-log.txt +++ b/etc/testing-log.txt @@ -1,3 +1,7 @@ +Wed Nov 17 13:43:11 GMT 1999 + + Tested compiled version. Seems to work well for XEmacs! + Tue Nov 16 15:28:51 GMT 1999 Tested automatic multiple file handling: see etc/demoisa |