Renamed file

1 files changed, 96 insertions, 0 deletions

diff --git a/html/projects.html b/html/projects.html
new file mode 100644
index 00000000..a8c180aa
--- /dev/null
+++ b/html/projects.html
@@ -0,0 +1,96 @@
+<?php  
+  require('functions.php3');
+  small_header("Proof General Projects"); 
+  ?>
+
+<p>
+Here are some proposals for projects connected to Proof General.
+</p>
+<p>
+The projects are designed as fairly self-contained contributions,
+involving code development and possibly a portion of supporting
+research.  They would be ideal projects for interested students
+or researchers.
+</p>
+<p>
+The projects are divided into those which are specific to Proof
+General, and those which would be useful more widely and do not depend
+on Proof General.  For more information on a project, click on its
+title.
+</p>
+
+<h2>A. Projects involving Proof General</h2>
+<ol>
+<li><?php pgproject("coqpbp","Proof-by-pointing support for Coq") ?></li>
+<li><?php pgproject("coqfile","Multiple file handling support for Coq") ?></li>
+<li><?php pgproject("isapbp","Proof-by-pointing support for Isabelle") ?></li>
+<li><?php pgproject("outline","Integrating block-structured development and outline mode") ?></li>
+<li><?php pgproject("thybrowse","A Generic Theory Browser") ?></li>
+<li><?php pgproject("pgml","Specification and tools for PGML") ?></li>
+<li><?php pgproject("pgip","A New Protocol for Interactive Proof in Proof General") ?></li>
+<li><?php pgproject("webreplay","A Web-based Proof Replayer for Proof General") ?></li>
+<li><?php pgproject("test","A Test Harness and Test Suite for Proof General") ?></li>
+<li><?php pgproject("hol","Proof General for HOL") ?></li>
+<li><?php pgproject("acs","Implementing Atomic Command Sequences") ?></li>
+</ol>
+
+<h2>B. Projects not directly involving Proof General</h2>
+<ol>
+<li><?php pgproject("mm","Multiplexed Modes for Emacs") ?></li>
+<li><?php pgproject("scrgen","Script General") ?></li>
+<li><?php pgproject("corba","An Experimental CORBA binding for ML") ?></li>
+<li><?php pgproject("reelcase","A ClearCase-like Configuration Management tool for Linux") ?></li>
+</ol>
+
+<p>
+Some projects involve Emacs Lisp.  This is the embedded programming
+language inside Emacs.  It is very easy to learn, since it is small,
+has a good manual, and has an interactive interpreter.  It is easy to
+use, not least because of its <i>self-documenting</i> nature: each
+variable or function is compiled together with documentation of its
+purpose.  (Other languages would do well to follow this).  It also
+has a powerful source-level debugger, <i>edebug</i>.
+</p>
+
+<!-- template for project pages -->
+<!-- <h2> </h2> -->
+<!-- <p> -->
+<!-- </p> -->
+<!-- <p> -->
+<!-- <b>Skills:</b> -->
+<!-- </p><p> -->
+<!-- <b>Proposer:</b> -->
+<!-- <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>. -->
+<!-- </p> -->
+
+<p>
+If you are interested in working on any of these projects,
+feel free to discuss with the project proposer or on the 
+<?php link_root("devel#develmail","developer's mailing list") ?>.
+</p>
+
+<p>
+If you would like to use any of these ideas as a formal project
+proposal for students at your institution, please feel free
+but do <?php hlink("feedback.phtml","let us know ","Feedback form")?>
+if some work is begun, to help coordinate efforts.
+NB: the proposer of the project does not guarantee to be available for
+formal supervision or intensive help with the project (but it may be
+possible to find somebody else to do that).
+</p>
+
+<p>
+If you would like to submit a project proposal
+for an improvement or extension of Proof General,
+please send an email or write a description on the 
+<?php hlink("feedback.phtml","web feedback form","Feedback form")?>.
+Projects should be significant contributions rather than
+incremental improvements (although we welcome the suggestion of those
+too).
+</p>
+
+
+<?php
+   click_to_go_back();
+   footer();
+?>