From 1aea7fca0334e89fbcf69cc7477589e4118b3ebe Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Sun, 19 Mar 2000 06:40:30 +0000
Subject: Improved links, new project on ACS.

---
 html/devel.phtml         |  1 +
 html/develdownload.phtml |  4 +++-
 html/functions.php3      |  2 +-
 html/projects.phtml      |  1 +
 html/projects/acs.html   | 36 ++++++++++++++++++++++++++++++++++++
 html/register.phtml      |  5 ++++-
 6 files changed, 46 insertions(+), 3 deletions(-)
 create mode 100644 html/projects/acs.html

diff --git a/html/devel.phtml b/html/devel.phtml
index 57e7b109..dfd45d4b 100644
--- a/html/devel.phtml
+++ b/html/devel.phtml
@@ -27,6 +27,7 @@ see <a href="/home/da/drafts/#white">here</a>.
 </ul>
 <ul>
 <li>
+Get involved!
 Take a look at the Proof General <a href="projects.phtml">project proposals</a>.
 </li>
 </ul>
diff --git a/html/develdownload.phtml b/html/develdownload.phtml
index 8902c89b..f3fca353 100644
--- a/html/develdownload.phtml
+++ b/html/develdownload.phtml
@@ -45,8 +45,10 @@ the planned changes to come.
 <!-- End Warning. -->
 </ul>
 
+<p>
 For install instructions, see 
-the <?php link_root("download#install",stable version download") ?>.
+the <?php link_root("download#install","stable version download") ?>.
+</p>
 
 <p>
 </p>
diff --git a/html/functions.php3 b/html/functions.php3
index c3bb4bc7..715fbafc 100644
--- a/html/functions.php3
+++ b/html/functions.php3
@@ -152,7 +152,7 @@ function footer($filemodified=".") {
 
 function click_to_go_back() {
   print "<p>\nClick <a href=\"index.phtml\">here</a> to go back to the ";
-  print $project_title;
+  print $project_title; // FIXME: doesn't work.
   print " front page.</p>\n";
 }
 
diff --git a/html/projects.phtml b/html/projects.phtml
index d6088410..edff89a5 100644
--- a/html/projects.phtml
+++ b/html/projects.phtml
@@ -31,6 +31,7 @@ title.
 <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>
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/register.phtml b/html/register.phtml
index be72cea4..c06142c6 100644
--- a/html/register.phtml
+++ b/html/register.phtml
@@ -33,7 +33,7 @@ provide a case for support for Proof General in the future.
 </p>
 <p>
 If you have already registered you do not need to fill in the form
-again, so return to <?php link_root("download","the download page.") ?>
+again, so return to <?php link_root("download#prereq","the download page.") ?>
 </p>
 <?php endif; ?>
 <h2>Registration Form</h2>
@@ -99,6 +99,9 @@ again, so return to <?php link_root("download","the download page.") ?>
    }
    print "</p>\n<p>";
 
+   print "<p>\nClick ";
+   link_root("download#prereq","here");
+   print " to return to the download page.<br></p>\n";
    click_to_go_back();
   
    footer();
-- 
cgit v1.2.3