diff options
author | 2000-03-19 06:40:30 +0000 | |
---|---|---|
committer | 2000-03-19 06:40:30 +0000 | |
commit | 1aea7fca0334e89fbcf69cc7477589e4118b3ebe (patch) | |
tree | 0953471fca8b5154ba418473d7016d29f169850b | |
parent | c6ab796932dbddb2fffeacf2b8f22ca5dbcf246c (diff) |
Improved links, new project on ACS.
-rw-r--r-- | html/devel.phtml | 1 | ||||
-rw-r--r-- | html/develdownload.phtml | 4 | ||||
-rw-r--r-- | html/functions.php3 | 2 | ||||
-rw-r--r-- | html/projects.phtml | 1 | ||||
-rw-r--r-- | html/projects/acs.html | 36 | ||||
-rw-r--r-- | html/register.phtml | 5 |
6 files changed, 46 insertions, 3 deletions
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(); |