+Below is the latest pre-release of Proof General, +made available for those who wish to test the latest features or bug +fixes. For developers, this release is also available as a +complete CVS snapshot (further below). +
++Pre-releases of Proof General may be buggy as we add new features and +experiment with them. Nonetheless, we welcome bug reports. But +please make sure you are using the latest pre-release before +reporting problems. +
++Please register if you haven't done so already. +
+ + + ++The manual included with the pre-release may be +updated from that of the +last stable release. +
++Here is the pre-release documentation: the user manual in +, + +or +, +and the new separate "adapting" manual, in +, + +or +. +
+ + + ++This version has been tested with XEmacs version 21.4 and +(minimally) with FSF Emacs 20.7.1. +We recommend the use of XEmacs; use under FSF Emacs +can no longer be properly supported. +
++Check the + + file + +for a summary of changes since the last stable version, and +notes about work-in-progress. +
+| gzip'ed tar file | + ++ |
| zip file | ++ |
| RPM package | ++ |
| individual files | +http access to files in development release + |
+NB: we no longer distribute the source RPM, since you can build +both source and "binary" RPMs direct from the tarball using +"rpm -ta". +
++For install instructions, see +the stable version download. +
+ ++
++
+ + + ++This archive is a snapshot from our CVS repository. +
++What's the difference from the user's pre-release above? +The complete archive also includes: +
++You probably don't need to download this if you're only +interested in hacking the Emacs lisp part of the program for a prover +that is currently supported. Note that there are no pre-built +documentation files in the developer's release. +
+ + diff --git a/html/doc.html b/html/doc.html index ccdfab58..3f092ade 100644 --- a/html/doc.html +++ b/html/doc.html @@ -98,7 +98,7 @@ list. HREF="http://www.dcs.ed.ac.uk/home/djs">Dilip Sequeira. Implementing Proof by Pointing without a Structure Editor. LFCS Technical Report ECS-LFCS-97-368. + HREF="http://www.lfcs.informatics.ed.ac.uk/reports/97/ECS-LFCS-97-368/index.html">ECS-LFCS-97-368. Also published as Rapport de recherche de l'INRIA Sophia Antipolis + + +
+Please use the form below to send us comments, suggestions,
+or offers to help with Proof Generl development.
+
+Or send email directly to
+the
+
+You can also report a bug using this form, although it would +be more helpful to do this from within Emacs, using the +"Proof General -> Submit bug report" menu command. +
+ + + +Dear " . $from . ",\n"; }; + print ""; + print "Thank-you for sending us feedback"; + if ($subject != "") { print " about " . $subject; }; + print ".
\n"; + print "If you provided a valid return email address, somebody from the Proof General team will acknowledge your message after it has been read."; + print "
"; + + mail($project_feedback, + "[Web Feedback Form]: " . $subject, + $message, + "Reply-To: " . $from . "\n"); + + click_to_go_back(); + + footer(); +endif; +?> diff --git a/html/kit b/html/kit index d7ba8cb2..edf6671f 100644 --- a/html/kit +++ b/html/kit @@ -1,4 +1,4 @@ - + + +The Proof General Kit project is in an early pre-experimental stage at +the moment. If you are interested in collaborating, or have ideas +or suggestions to contribute, please send a note to +kit@proofgeneral.org + ++Not much has been started yet. +
+ +But you can download the DTDs for PGIP and PGML, here: +