+The Proof General project was initiated in 1994 (under the name of +"lego-mode") and coordinated until October 1998 by Thomas +Kleymann. Since October 1998, David Aspinall has been in charge of +Proof General. +
+
The project has benefited from funding by EPSRC +and the EC. +
+ ++The generic base for Proof General was developed at the +LFCS by Kleymann, Sequeira, +Goguen and Aspinall (in order of appearance). +It follows some of the ideas used in +Project CROAP. +
++The authors and current maintainers of the various instantiations of +Proof General are mentioned on the + +
++For more on the history of the development of +Proof General, see the + +
+ +
+Have you any questions, comments, or suggestions about Proof General?
+
+Send us a message using this form.
+
+Discuss Proof General with other users and receive +announcements by joining our mailing +list. +
+ + + diff --git a/html/doc.phtml b/html/doc.phtml new file mode 100644 index 00000000..5f90f3f9 --- /dev/null +++ b/html/doc.phtml @@ -0,0 +1,63 @@ ++Full documentation for Proof General is included in the When running Proof General the +manual is available from the "Proof General" menu. It should also +appear in the system info pages. +
+ +
+For convenience, the documentation is also available in HTML
+
+
+You can download the
+dvi,
+ps,
+or
+pdf
+versions for printing.
+
+
Proof General supports Script Management as documented in: +
++ It has support for Proof by Pointing, as documented in: +
+
+Before downloading Proof General, we'd be grateful if you
+register.
+
+The information collected will be used only to help a case for
+support for Proof General in the future.
+
+If you have already registered you do not need to do so again. +
+ ++You may also like to consider joining the +Proof General +mailing list. +
+ ++You can download the latest +stable release +or the latest +pre-release. +
+ +
+This version of Proof General has been tested
+with XEmacs 20.4 and FSF Emacs 20.2, 20.3
+It is available in two formats:
+
+Both the tarball and the RPM package include the generic elisp
+code,
+code for LEGO, Coq, and Isabelle, installation instructions
+and documentation.
+
+To use Proof General, simply unpack the sources with +
++ tar -xpzf ProofGeneral-2.0.tar.gz ++
+(use gunzip in place of -z if you don't have GNU tar),
+and then add this one line to your .emacs file:
+
+ (load-file "directory/generic/proof-site.el") ++
+Where directory is the directory in which you unpacked
+the sources.
+
+If you use the RPM package, directory is
+/usr/share/emacs/ProofGeneral
+
+Further customization is possible via the Customize menus in
+Emacs.
+
+See the
+file in the distribution for more details.
+
+Please send us +any problems, suggestions, or patches. +
+ +
+This pre-release of Proof General may be unstable as new
+features are added and experimented with.
+
+Check the
+
+
+
+
+file for a summary of changes since the last stable version.
+
+Please make test with the latest pre-release before reporting any problems
+in a pre-release.
+
+If you are interested in helping to develop the core of Proof General, +you may like to download a complete archive of all the sources used to +build the Proof General pre-release. The difference from the working +version distribution above is that we include our low-level list of +things to do, some developer's make files used to generate +documentation files and the release itself from our CVS repository, +some test files, sources for some of the images (in GIMP form), and the web pages. +
++You probably don't need to download this if you're only +interested in hacking the Emacs lisp part of the program (but you may +still like to check the latest + +). + +
+ ++If there is any interest from developers, we could make our +CVS repository open to anonymous cvs server access. Please +ask. +
+ + diff --git a/html/features.phtml b/html/features.phtml new file mode 100644 index 00000000..3171c74d --- /dev/null +++ b/html/features.phtml @@ -0,0 +1,140 @@ + + ++It doesn't matter if you're an Emacs militant or a pacifist! +
+ ++Proof General will be useful to you if you use a proof +assistant, and you'd like some of the following features: +
+ ++ Proof General colours a proof script to show the state in the proof + assistant. Parts of a proof script that have been processed are + displayed in blue and are "locked" -- they cannot be edited. Parts + of the script currently being processed by the proof assistant are + shown in red. Commands are provided to process new parts of the + buffer, or undo already processed parts. +
++ Take a look at this + screenshot + of Proof General to see script managament in action. +
++ Dependencies between script files is + communicated from the proof assistant to Proof General. + If you want to edit a file which has been loaded into the + proof assistant already, Proof General will unlock the file + and all the files which depend on it. This connects the + editor with the theory dependency or make system of the + proof assistant. +
+ ++ Proof by pointing uses the + interface to highlight subterms under the mouse, and Proof General + uses the subterm structure to make it easy + to cut and paste complicated subterms. +
+ ++ Using the toolbar, you can replay proofs without knowing any + low-level commands of the proof assistant or any Emacs hot-keys! +
+ ++ Proof General decorates proof scripts: proof commands are + highlighted and different fonts may be used for definitions and + assumptions, for example. +
++ Proof General is supplied with utilities to make tag indexes + for Emacs. This makes it easy to quickly access definitions from a + standard library, for example, and in large proof developments + split across multiple files. + +
++ Adapting for a new proof assistant is mainly a matter of setting + some variables with regular expressions to help parse output from + the prover, and setting other variables with commands to send to the + prover. + To get the most from Proof General (proof-by-pointing, for example), + it may be necessary to augment the output routines of the + proof assistant. +
+ Please feel free to download Proof General to customize it for a new + system, and + + how you get on. ++For more details of the above features, see the + +
+ diff --git a/html/feedback.phtml b/html/feedback.phtml new file mode 100644 index 00000000..30e3bded --- /dev/null +++ b/html/feedback.phtml @@ -0,0 +1,88 @@ + + +
+Please use the form below to send us comments and suggestions.
+
+Or send email directly to
+the
+Proof General maintainer
+<proofgen@dcs.ed.ac.uk>.
+
+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("da", /*"proofgen@dcs.ed.ac.uk",*/ + "[Web Feedback Form]: " . $subject, + $message, + "Reply-To: " . $from . "\n"); + + click_to_go_back(); + + footer(); +endif; +?> diff --git a/html/fileshow.phtml b/html/fileshow.phtml new file mode 100644 index 00000000..4ab2170e --- /dev/null +++ b/html/fileshow.phtml @@ -0,0 +1,13 @@ +\n"; + markup_plain_text($filename); + print "\n"; + print "
+
+
+Web pages by
+David Aspinall.
+[" + . $text . "]
';
+
+/* A link to one of the main pages (must appear in navbar menu) */
+
+function link_root($page,$text) {
+ print "";
+ print $text;
+ print "\n";
+}
+
+function small_header($title) {
+ include('smallheader.phtml');
+ print "