diff options
Diffstat (limited to 'html/main.html')
| -rw-r--r-- | html/main.html | 154 |
1 files changed, 154 insertions, 0 deletions
diff --git a/html/main.html b/html/main.html new file mode 100644 index 00000000..3d6e8ea6 --- /dev/null +++ b/html/main.html @@ -0,0 +1,154 @@ +<h2>What is Proof General?</h2> +<p> +<b>Proof General</b> is a generic interface for proof assistants, +currently based on Emacs. +It has been developed at the +<a href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a> +in the <a href="http://www.ed.ac.uk/">University of Edinburgh</a>. +Proof General +works best under +<a href="http://www.xemacs.org/">XEmacs</a>, but can also be used with +<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>. +You need a recent version in either case. +</p> +<p> +The aim of the Proof General project is to provide powerful and +configurable interfaces which help user-interaction with interactive +proof assistants. The strategy of Proof General is to target power +users rather than novices, building an environment for <i>proof +engineering</i>. But we include modern user interface features, such +as toolbar and menus, which make use easier for all. Proof General is +currently used by many people for organizing large proof developments, +and also for teaching interactive proof. +<p> +To read more about what Proof General +provides, +<a href="features">check the features list</a>. +To see what Proof General looks like in use, have a look at these +<a href="screenshot">screenshots</a>. +To download Proof General, visit the +<a href="download">download page</a>. +To contact the developers, click +<?php hlink("feedback","here","Feedback form")?>. +</p> + + + +<h2>What systems does Proof General work with?</h2> +<p> +Proof General comes ready-customized for these proof assistants: +</p> + +<table width="90%"> + <tr> + <td align="center"> + <?php hlink("http://pauillac.inria.fr/coq/", + "<img src=\"images/coqlogo4.gif\" width=66 height=61 border=0 alt=\"Coq badge\">","The Coq Home Page") ?> + </td> + <td> + <b><?php fileshow("ProofGeneral/coq/README","Coq Proof General "); ?></b> for + <?php hlink("http://pauillac.inria.fr/coq/", + "Coq","The Coq Home Page") ?> + <br> + <div style="font-size: smaller"> + First crafted by + <a href="http://www.dcs.ed.ac.uk/~hhg">Healfdene Goguen</a>. + <br> + Contributions by Patrick Loiseleur. + <br> + Maintained by + <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>. + </div> + </td> + </tr> + <tr> + <td align="center"> + <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/", + "<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">", + "The Isabelle Home Page"); ?> + </td> + <td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for + <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/", + "Isabelle", "The Isabelle Home Page"); ?> + <br> + <div style="font-size: smaller"> + Crafted and maintained by + <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>. + <br> + Additional maintainance, support for + <a href="http://isabelle.in.tum.de/Isar">Isabelle/Isar</a> + by + <a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>. + </div> + </td> + </tr> + <tr> + <td align="center"> + <?php hlink("http://www.dcs.ed.ac.uk/home/lego", + "<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">", + "The LEGO Home Page") ?> + </td> + <td><b><?php fileshow("ProofGeneral/lego/README","LEGO Proof General "); ?></b> for + <?php hlink("http://www.dcs.ed.ac.uk/home/lego", + "LEGO","The LEGO Home Page") ?> + <br> + <div style="font-size: smaller"> + First crafted by <a href="http://www.dcs.ed.ac.uk/~tms">Thomas Kleymann</a> + and + <a href="http://www.dcs.ed.ac.uk/~djs/welcome.html">Dilip Sequeira</a>. + <br> + Maintained by + <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a> + and + <a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>. + </div> + </td> + </tr> + <tr> + <td align="center"> + <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html", + "PhoX", + "The PhoX Home Page") ?> + </td> + <td><b><?php fileshow("ProofGeneral/phox/README","PhoX Proof General "); ?></b> for + <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html", + "PhoX","The PhoX Home Page") ?> + <br> + <div style="font-size: smaller"> + Crafted and maintained by + <a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</a> + and + <a href="mailto:roziere@logique.jussieu.fr">Paul Roziere</a>. + </div> + </td> + </tr> +</table> +<p> +There are also <i>experimental</i> instances of Proof General: +<ul> +<li><b><?php fileshow("ProofGeneral/hol98/README","HOL Proof General"); ?></b>, +for <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL98</a>. +</li> +<li><b><?php fileshow("ProofGeneral/twelf/README","Twelf Proof General"); ?></b>, +for <a href="http://www.twelf.org">Twelf</a>. +</li> +<li><b><?php fileshow("ProofGeneral/acl2/README","ACL2 Proof General"); ?></b>, +for <a href="http://www.cs.utexas.edu/users/moore/acl2">ACL2</a>. +</li> +</ul> +<p> +These instances of Proof General are functional, but only show a bare +fraction of what is possible. We are +seeking volunteers to support and improve each of these +(please <a href="feedback">send a note to + <tt><?php print $project_feedback; ?></tt></a> if you're interested). +</p> +<p> +Proof General is ready to be customized to new proof assistants. +It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", +"very easy"); ?> to get basic support working. +Full <a href="ProofGeneral/doc/PG-adapting.pdf">documentation on +configuration</a> is provided. +</p> + + |