Deleted file

15 files changed, 0 insertions, 433 deletions

diff --git a/html/projects/acs.html b/html/projects/acs.html
deleted file mode 100644
index d3768c17..00000000
--- a/html/projects/acs.html
+++ /dev/null
@@ -1,36 +0,0 @@
-<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
deleted file mode 100644
index 35d48eb1..00000000
--- a/html/projects/coqfile.html
+++ /dev/null
@@ -1,22 +0,0 @@
-<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
deleted file mode 100644
index 366feb7c..00000000
--- a/html/projects/coqpbp.html
+++ /dev/null
@@ -1,17 +0,0 @@
-<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
deleted file mode 100644
index 35faa73f..00000000
--- a/html/projects/corba.html
+++ /dev/null
@@ -1,37 +0,0 @@
-<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
deleted file mode 100644
index 6828899a..00000000
--- a/html/projects/hol.html
+++ /dev/null
@@ -1,40 +0,0 @@
-<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
deleted file mode 100644
index c08ea85e..00000000
--- a/html/projects/isapbp.html
+++ /dev/null
@@ -1,25 +0,0 @@
-<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/outline.html b/html/projects/outline.html
deleted file mode 100644
index 67680b8f..00000000
--- a/html/projects/outline.html
+++ /dev/null
@@ -1,26 +0,0 @@
-<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
deleted file mode 100644
index 073edd06..00000000
--- a/html/projects/pgip.html
+++ /dev/null
@@ -1,22 +0,0 @@
-<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
deleted file mode 100644
index 46cdd960..00000000
--- a/html/projects/pgml.html
+++ /dev/null
@@ -1,26 +0,0 @@
-<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
deleted file mode 100644
index f5fa2f04..00000000
--- a/html/projects/reelcase.html
+++ /dev/null
@@ -1,34 +0,0 @@
-<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
deleted file mode 100644
index d65b477f..00000000
--- a/html/projects/scrgen.html
+++ /dev/null
@@ -1,26 +0,0 @@
-<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
deleted file mode 100644
index f9d5ecf0..00000000
--- a/html/projects/test.html
+++ /dev/null
@@ -1,24 +0,0 @@
-<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
deleted file mode 100644
index 8993d942..00000000
--- a/html/projects/thybrowse.html
+++ /dev/null
@@ -1,34 +0,0 @@
-<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
deleted file mode 100644
index 1754e2df..00000000
--- a/html/projects/webreplay.html
+++ /dev/null
@@ -1,24 +0,0 @@
-<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
deleted file mode 100644
index 30828a97..00000000
--- a/html/projects/xmlpgip.html
+++ /dev/null
@@ -1,40 +0,0 @@
-<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>