1 files changed, 90 insertions, 0 deletions
diff --git a/html/projects.phtml b/html/projects.phtml
new file mode 100644
index 00000000..281c043d
--- /dev/null
+++ b/html/projects.phtml
@@ -0,0 +1,90 @@
+<?php  
+  require('functions.php3');
+  small_header("Proof General Project Proposals"); 
+  ?>
+
+<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 small amount of supporting
+research.  They would be ideal projects for interested students
+or researchers.
+</p>
+
+<ul>
+<li><b>Proof-by-pointing support for Coq</b>
+<p>
+Coq already has sophisticated notions of proof-by-pointing,
+and old work on support for Proof General may be helpful.  
+We want to integrate with the latest version of Coq's
+proof-by-pointing, possibly improving Proof General's
+support along the way.
+</p>
+<p>
+<b>Skills:</b>
+ Some understanding of Coq implementation, co-operation with
+ the Coq developers to get any Coq modifications (if any) incorporated.
+ Minimal Emacs Lisp knowledge. 
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+
+<li><b>Proof-by-pointing support for Isabelle</b>
+<p>
+Isabelle has a sophisticated concrete syntax mechanism which makes it
+difficult to add annotations to connect the displayed output back to
+the internal abstract syntax.  This issue needs to be solved to
+support proof-by-pointing (and other features) in Isabelle.
+A 
+<a href="http://www.informatik.uni-bremen.de/~bu/isa_contrib/isabelle.html">
+patch by Burkhart Wolff</a> 
+providing term structure annotations for a previous release of
+Isabelle may be useful here.  To implement proof-by-pointing itself,
+tactics using the gesture information must be written.
+</p>
+<p>
+<b>Skills:</b>
+ Some understanding of Isabelle implementation, 
+ co-operation with the Isabelle developers to get
+ Isabelle modifications incorporated.
+ Skill in writing Isabelle tactics.
+ Minimal Emacs Lisp knowledge.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+</li>
+</ul>
+
+
+
+<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>
+Note: the proposer of the project is just that; he or she 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.  Contact the project proposer first for more details.
+</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();
+?>