16 files changed, 459 insertions, 0 deletions
diff --git a/html/projects/acs.html b/html/projects/acs.html
new file mode 100644
index 00000000..d3768c17
--- /dev/null
+++ b/html/projects/acs.html
@@ -0,0 +1,36 @@
+<h2>Implementing Atomic Command Sequences</h2>
+<p>
+In Proof General, the blue region of a script buffer contains the
+initial segment of the proof script which has been processed
+successfully. It consists of atomic sequences of commands
+(ACS). Retraction is supported to the beginning of every ACS. By
+default, every command is an ACS. But the granularity of atomicity
+should be able to be adjusted.
+</p>
+<p>
+This adjustment is essential when arbitrary retraction is not
+supported in the prover. Usually, after a theorem has been proved, one
+may only retract to the start of the goal. One needs to mark the proof
+of the theorem as an ACS. At present, support for these goal-save
+sequences has been hard wired. No other ACS are currently
+supported. We need a generalisation to overcome this deficiency.
+</p>
+<p>
+This improvement should allow support for Coq's <i>Section</i> command,
+LEGO's <i>Discharge</i> and simplified support for Isabelle/Isar,
+by removing some of the prover-specific code.
+</p>
+<p>
+<b>References:</b>
+Proof General manual
+(<?php htmlshow("ProofGeneral/doc/ProofGeneral_17.html#SEC119","this section","Proof General Manual") ?>), and proof assistant manuals.</p>
+<p>
+<b>Skills:</b>
+Good Emacs Lisp, understanding of "granularity" problem
+for proof assistant history mechanisms.</p>
+<p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>
+(based on an original idea by Thomas Kleymann).
+</p>
+
diff --git a/html/projects/coqfile.html b/html/projects/coqfile.html
new file mode 100644
index 00000000..35d48eb1
--- /dev/null
+++ b/html/projects/coqfile.html
@@ -0,0 +1,22 @@
+<h2>Multiple file handling support for Coq</h2>
+<p>
+Coq Proof General does not yet handle script management across file
+boundaries, as do the LEGO and Isabelle versions.  Script management
+for multiple files means that whenever a file is viewed in the editor,
+it is locked if it has been loaded into the current Coq session.  It
+may mean that Proof General can make use of the file-level primitives
+of Coq, so that the user doesn't have to escape the interface, 
+or carefully load each file and its dependencies.  This also means that
+complete proof scripts will not so often need to be interpreted by
+Proof General, solving one of the present bottlenecks with using
+Coq Proof General.
+</p>
+<p>
+<b>Skills:</b>
+ Some understanding of Coq implementation, co-operation with
+ the Coq developers to get any Coq modifications (if any) incorporated.
+ Some Emacs Lisp knowledge. 
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
diff --git a/html/projects/coqpbp.html b/html/projects/coqpbp.html
new file mode 100644
index 00000000..366feb7c
--- /dev/null
+++ b/html/projects/coqpbp.html
@@ -0,0 +1,17 @@
+<h2>Proof-by-pointing support for Coq</h2>
+<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>
diff --git a/html/projects/corba.html b/html/projects/corba.html
new file mode 100644
index 00000000..35faa73f
--- /dev/null
+++ b/html/projects/corba.html
@@ -0,0 +1,37 @@
+<h2>An Experimental CORBA binding and IDL mapping for ML</h2>
+<p>
+The future version of Proof General may use CORBA as a communication
+mechanism between different components.  CORBA is also used by the
+Unix/Linux desktops KDE and GNOME, which use the free implementations
+MICO and ORBIT respectively.  We would like to be able to use ML to
+write to interface with other CORBA components on the desktop and 
+network.  For this a binding for ORB functions in ML is needed, as well 
+as perhaps a mapping from the CORBA IDL into Standard ML, so that
+we can write CORBA enabled applications in SML.  
+</p>
+<p>
+This project involves the design and implementation of an experimental
+version (subset of features) of such a system, using one of the
+open-source ML compilers such as Moscow ML, Poly/ML or OCaml (in fact,
+there is already some handling of COM in OCaml which can be used to
+access an ORB).  Essentially, we want to analyse the feasibility
+and performance of using a CORBA architecture for Proof General.
+</p>
+<p>
+An CORBA binding for Haskell would also be an interesting project.
+</p>
+<p>
+See 
+<a href="http://www.cl.cam.ac.uk/~cvr21/projects.html">Claudio Russo's</a> 
+project suggestion for a similar proposal, including useful links.
+</p>
+<p>
+<b>Skills:</b>
+Good ML, C, C++, programming skills and understanding of abstraction
+mechanisms, basic understanding of CORBA and willing to get to
+grasps with some of MICO or ORBIT.
+</p><p>
+<b>Proposers:</b>
+<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a> and
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
diff --git a/html/projects/hol.html b/html/projects/hol.html
new file mode 100644
index 00000000..6828899a
--- /dev/null
+++ b/html/projects/hol.html
@@ -0,0 +1,40 @@
+<h2>Proof General for HOL</h2> 
+<p> 
+It is fairly easy to get basic support for Proof General for 
+<a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL</a>, and
+this has recently been tried for HOL 98.  However, it would be a bigger
+and more interesting project to get proper and complete support for
+HOL working.  There are a couple of problems unique to HOL.
+</p>
+<p>
+Much more than Isabelle, HOL relies on its meta language, ML.  HOL
+proof scripts often use batch-oriented single step tactic proofs
+constructed in ML, but Proof General does not offer an easy way to
+edit these kind of proofs (as opposed to multi-step interactive
+proofs).  The <a
+href="http://hagi.is.s.u-tokyo.ac.jp/boomborg/">Boomburg-HOL</a> Emacs
+interface by Koichi Takahashi and Masima Hagiya addressed this
+problem, as well as providing support for proof-by-pointing to HOL.
+Their interface could perhaps be reinterpreted or reimplemented inside
+Proof General.  Implemented in a generic way, batch script editing
+would also be useful for Isabelle.
+</p>
+<p>
+Another problem is that HOL scripts sometimes use SML structures,
+which can cause confusion because Proof General does not really parse
+SML, it just looks for semicolons.  This could be improved by taking a
+better parser (e.g. from sml mode).
+</p>
+<p>
+Finally, to fully support the current Proof General feature set,
+it would be useful to extend HOL with support for communicating
+file-dependency information to Proof General, and term-structure
+markup for proof by pointing.
+<p>
+<b>Skills:</b>
+Some Standard ML, some Emacs Lisp.  Basic understanding of
+proof assistant behaviour, interest in HOL.  
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
diff --git a/html/projects/isapbp.html b/html/projects/isapbp.html
new file mode 100644
index 00000000..c08ea85e
--- /dev/null
+++ b/html/projects/isapbp.html
@@ -0,0 +1,25 @@
+<h2>Proof-by-pointing support for Isabelle</h2>
+<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>
+
diff --git a/html/projects/mm.html b/html/projects/mm.html
new file mode 100644
index 00000000..c0946f65
--- /dev/null
+++ b/html/projects/mm.html
@@ -0,0 +1,26 @@
+<h2>Mulitple modes for Emacs</h2>
+<p>
+Emacs has a mechanism for customizing the editing behaviour of buffers
+based on their <i>major mode</i>.  A buffer can only have one major
+mode, but in literate styles of programming and proving we want to mix
+program text with documentation in a single file.  A way of
+multiplexing major modes is needed, so that different regions of a
+buffer can be edited in different modes.  One approach may be to use
+"views" onto untangled buffers, although it isn't clear how search and
+replace, etc, should behave in this case.  
+</p><p>
+The <a href="http://mmm-mode.sourceforge.net/">MMM mode</a> Emacs
+add-on allows multiple-modes in a similar way, and was originally
+designed for the situation where you have a script embedded in an HTML
+page.
+This project 
+might try applying MMM mode for Proof General 
+with Coq and Isabelle/Isar, as a feasibility demonstration.
+</p><p>
+<b>Skills:</b>
+A passion for Emacs and Emacs Lisp.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+
diff --git a/html/projects/outline.html b/html/projects/outline.html
new file mode 100644
index 00000000..67680b8f
--- /dev/null
+++ b/html/projects/outline.html
@@ -0,0 +1,26 @@
+<h2>Integrating block-structured development and outline mode</h2>
+<p>
+Emacs already provides powerful outline facilities (cf. the
+outl-minor-mode setup for the well-known auc-tex package).  
+Similarly, proof systems such as Isabelle/Isar are inherently based on
+block-structured proof texts, with compositional proof checking.
+</p><p>
+But Proof General currently offers a mostly linear model of
+incremental script management.  The aim of this project is to extend that
+model to a hierarchic one: e.g. sub-proofs could be suppressed in the
+presentation, or even temporarily suspended (to achieve top-down
+development).
+</p><p>
+Outline support would be useful for the large scale structure of formal
+developments as well, e.g. support the basic arrangement into logical
+section (cf. Coq), or even just traditional layout-based ones (cf. LaTeX).
+</p>
+<p>
+<b>Skills:</b>
+Some understanding of the workings of Emacs outline mode and Proof
+General script management.  Good portion of Emacs lisp knowledge.
+</p><p>
+<b>Proposer:</b>
+<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
+</p>
+
diff --git a/html/projects/pgip.html b/html/projects/pgip.html
new file mode 100644
index 00000000..073edd06
--- /dev/null
+++ b/html/projects/pgip.html
@@ -0,0 +1,22 @@
+<h2>A New Protocol for Interactive Proof in Proof General</h2>
+<p>
+PGIP is a protocol for interactive proof to be used in the next
+version of Proof General.  It is based around the present protocol,
+but implemented with a standard collection of messages rather than
+different messages for different proof assistants.  An outline of PGIP
+and an experimental DTD
+is given in the <a href="/home/da/drafts/#white">white paper</a>.  A
+first implementation of PGIP will consist of (1) a filter (or
+modification of the output routines) for an existing proof assistant,
+which could be implemented in perl or some other language; and (2) a
+new backend for Proof General in Emacs, which configures it for PGIP.
+</p>
+<p>
+<b>Skills:</b>
+Interest in interactive proof and basic understanding
+of interaction mechanisms with at least one of 
+LEGO, Coq, Isabelle.   Programmming in Emacs Lisp.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
diff --git a/html/projects/pgml.html b/html/projects/pgml.html
new file mode 100644
index 00000000..46cdd960
--- /dev/null
+++ b/html/projects/pgml.html
@@ -0,0 +1,26 @@
+<h2>Specification and tools for PGML</h2>
+<p> 
+PGML is the proposed logical markup language for future versions of
+Proof General.  The basic version legitimizes the present markup
+scheme which is used by Proof General (based on 8-bit characters).
+The ideas for PGML are described in the white paper 
+<a href="/home/da/drafts/#white">here</a>, and an experimental
+DTD is given there.  This project is to refine the specification
+of PGML, and develop some tools for using it.  Various tools are desirable,
+including: (1) translation tools which convert PGML to various other
+formats, such as HTML and LaTeX.  (2) a display tool which displays PGML 
+inside Emacs, or converts it to HTML for display by a web browser; 
+(3) a filter or revised version of LEGO which converts its 8-bit markup 
+into PGML, for testing purposes.  We need the last tool for other
+proof assistants too.
+</p>
+<p> 
+<b>Skills:</b> 
+Understanding of markup languages and tools for using and specifying them.
+Interest in representation of mathematical content. 
+Necessary programming skills.
+</p><p> 
+<b>Proposer:</b> 
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p> 
+
diff --git a/html/projects/reelcase.html b/html/projects/reelcase.html
new file mode 100644
index 00000000..f5fa2f04
--- /dev/null
+++ b/html/projects/reelcase.html
@@ -0,0 +1,34 @@
+<h2>A ClearCase-like Configuration Management tool for Linux</h2>
+<p>
+Managing large libraries of theories and proofs, good software
+engineering practices of configuration management become important
+when using proof assistants.  One powerful and popular configuration
+management tool is the commercial <a
+href="http://www.rational.com/products/clearcase/index.jtmpl">Rational
+ClearCase</a>.  
+</p>
+<p>
+The crucial way that ClearCase goes beyond CVS is in providing a view
+of a configuration directly through a special mountpoint on
+the filesystem.  
+</p>
+<p>
+This is a project to implement a kernel-level filesystem driver for
+Linux using the Linux VFS to create a ClearCase-like view of a
+configuration, through a mountable filesystem.  The underlying
+configuration management could be done through RCS or CVS, perhaps
+invoked via a companion user-level process.
+Particular revisions of files should be accessible through names
+interpreted specially by the filesystem driver, and some
+user-level commands will be needed for other operations.
+</p>
+<p>
+<b>Skills:</b> 
+Expert C programmer, with ability to understand and work on Linux
+kernel code.  Understanding of configuration management principles.
+</p><p>
+<b>Proposers:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>
+from an idea by 
+<a href="http://www.dcs.ed.ac.uk/home/cxl">Christoph L&uuml;th</a>
+</p>
diff --git a/html/projects/scrgen.html b/html/projects/scrgen.html
new file mode 100644
index 00000000..d65b477f
--- /dev/null
+++ b/html/projects/scrgen.html
@@ -0,0 +1,26 @@
+<h2>Script General</h2>
+<p>
+Proof General is based around a core system of script management
+for proof scripts.  But the idea of script management is not
+restricted to proof assistants, it makes sense for many interactive
+scripting languages.  It deserves to be better known and used.
+A worthwhile project would be to rewrite the core script management
+features of Proof General so that they could work for arbitrary
+interactive scripting languages, and instantiate to Proof General as
+well as languages such as ML, Haskell, LISP, Scheme, Python, and
+even Emacs Lisp itself.
+</p>
+<p>
+An alternative version of this project is to implement a 
+generic basis for script management which does <i>not</i> depend on 
+Emacs, but uses a similar protocol to communicate with other
+text editors or display widgets.  This could be implemented in
+SML, OCaml, Java, C++, or any other suitable language.
+<p>
+<b>Skills:</b>
+Proficient Emacs Lisp (or other programming language), 
+knowledge of scripting languages desirable.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
diff --git a/html/projects/test.html b/html/projects/test.html
new file mode 100644
index 00000000..f9d5ecf0
--- /dev/null
+++ b/html/projects/test.html
@@ -0,0 +1,24 @@
+<h2>A Test Harness and Test Suite for Proof General</h2>
+<p>
+As Proof General becomes a more complex system, we badly need some way
+of performing automatic functional testing, to ensure that changes and
+extensions preserve functional correctness.  Although classical
+testing of interfaces involves manually following a checklist of
+actions and observations, it should be straightforward to automate
+this using Emacs Lisp.  Interactive actions can be simulated by
+certain function calls, and their results can be determined by
+examining the contents of the edit buffers.  This project proposes the
+design and implementation of a test harness and accompanying test
+suite to test some of the core functions of Proof General.
+Ultimately, the tests should be run as part of the build process
+before each development release is allowed to go ahead.
+</p>
+<p>
+<b>Skills:</b>
+An interesting in testing user interfaces.
+Basic knowledge of Emacs Lisp.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+
diff --git a/html/projects/thybrowse.html b/html/projects/thybrowse.html
new file mode 100644
index 00000000..8993d942
--- /dev/null
+++ b/html/projects/thybrowse.html
@@ -0,0 +1,34 @@
+<h2>A Generic Theory Browser</h2>
+<p>
+Proof General has very limited mechanisms for helping the user find
+theorems and definitions during a proof.  It has notion of displaying
+a "current context" for a proof, and configuration with a proof
+engine command for searching for theorems.  It would be useful to
+extend these facilities with a <i>theory browser</i> for investigating
+the theories currently defined in (or available from) a running proof
+assistant.  This involves designing a small protocol to communicate
+with the proof assistant and a generic way of displaying theories
+which have different aspects from system to system.  A way which would
+fit in well with Emacs would be to use a <tt>dired</tt>-like buffer.
+</p>
+<p>
+An alternative version of this project would be to write a standalone
+theory browser which uses an extension of the forthcoming Proof
+General standardized protocol for interaction (see white paper <a
+href="/home/da/drafts/#white">here</a>).  This could be implemented in
+Java, or in a functional language, Perl, C or C++, so long as a nice
+toolkit is chosen (Qt or GTK).
+</p>
+<p>
+(For a related idea, see the browser integrated with OCaml).
+</p>
+<p>
+<b>Skills:</b>
+Interface programming skills.
+Basic understanding of what theories are for several different proof
+assistants.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+
diff --git a/html/projects/webreplay.html b/html/projects/webreplay.html
new file mode 100644
index 00000000..1754e2df
--- /dev/null
+++ b/html/projects/webreplay.html
@@ -0,0 +1,24 @@
+<h2>A Web-based Proof Replayer for Proof General</h2>
+<p>
+One of the nice features of Proof General is that it is very easy to
+replay existing proofs, by mouse clicks alone.  No low-level
+understanding of a proof assistant is needed to step through proofs.
+We would like to have a web-based version of Proof General which
+allowed for this proof replay (at least), perhaps running a proof
+assistant remotely.  The main aspect is to implement an engine for
+script management (colouring of lines of files), displaying in a web
+browser, sending lines to a proof assistant process, and displaying the
+results.  Ideally, the ideas for new standard protocols for Proof
+General in the <a href="/home/da/drafts/#white">white paper</a> would
+be followed.
+</p>
+<p>
+<b>Skills:</b>
+Strong web programming skills using scripting languages,
+dynamic HTML, etc.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+
+
diff --git a/html/projects/xmlpgip.html b/html/projects/xmlpgip.html
new file mode 100644
index 00000000..30828a97
--- /dev/null
+++ b/html/projects/xmlpgip.html
@@ -0,0 +1,40 @@
+<h2>A New Protocol for Interactive Proof in Proof General</h2>
+<p>
+PGIP is a protocol for interactive proof to be used in the next
+version of Proof General.  It is based around the present protocol,
+but implemented with a standard collection of messages rather than
+different messages for different proof assistants.  An outline of PGIP
+is given in the <a href="/home/da/drafts/#white">white paper</a>.  A
+first implementation of PGIP will consist of (1) a filter (or
+modification of the output routines) for an existing proof assistant,
+which could be implemented in perl or some other language; and (2) a
+new backend for Proof General in Emacs, which configures it for PGIP.
+</p>
+<p>
+<b>Skills:</b>
+Interest in interactive proof and basic understanding
+of interaction mechanisms with at least one of 
+LEGO, Coq, Isabelle.   Programmming in Emacs Lisp.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
+<html>
+  <head>
+    <title></title>
+  </head>
+
+  <body>
+    <h1></h1>
+
+
+
+    <hr>
+    <address><a href="mailto:da@dcs.ed.ac.uk">David Aspinall</a></address>
+<!-- Created: Tue Apr 25 18:11:06 BST 2000 -->
+<!-- hhmts start -->
+Last modified: Tue Apr 25 18:22:01 BST 2000
+<!-- hhmts end -->
+  </body>
+</html>