diff options
| -rw-r--r-- | html/devel.phtml | 25 | ||||
| -rw-r--r-- | html/develdownload.phtml | 45 | ||||
| -rw-r--r-- | html/download.phtml | 40 | ||||
| -rw-r--r-- | html/elispmarkup.php3 | 134 | ||||
| -rw-r--r-- | html/features.phtml | 18 | ||||
| -rw-r--r-- | html/fileshow.phtml | 8 | ||||
| -rw-r--r-- | html/main.phtml | 33 | ||||
| -rw-r--r-- | html/mission.phtml | 138 | ||||
| -rw-r--r-- | html/news.phtml | 14 | ||||
| -rw-r--r-- | html/projects/hol.html | 7 | ||||
| -rw-r--r-- | html/proofgen.css | 13 |
11 files changed, 404 insertions, 71 deletions
diff --git a/html/devel.phtml b/html/devel.phtml index fa9dc1ed..75c5af17 100644 --- a/html/devel.phtml +++ b/html/devel.phtml @@ -46,18 +46,33 @@ for Proof General. </ul> <ul> <li> -See our current low-level lists of things to do, for the +<a name="lowleveltodo">See our current low-level lists of things to do</a>, +for the <!-- WARNING! Lines below automatically edited by makefile. --> <?php fileshow("ProofGeneral-3.1pre000310/todo","generic base"); ?>, <br> and for each prover: - <?php fileshow("ProofGeneral-3.1pre000310/isa/todo","isa to do"); ?>, - <?php fileshow("ProofGeneral-3.1pre000310/isar/todo","isar to do"); ?>, - <?php fileshow("ProofGeneral-3.1pre000310/coq/todo","coq to do"); ?>, - <?php fileshow("ProofGeneral-3.1pre000310/lego/todo","lego to do"); ?>. + <?php fileshow("ProofGeneral-3.1pre000309/lego/todo","lego to do"); ?>, + <?php fileshow("ProofGeneral-3.1pre000309/coq/todo","coq to do"); ?>, + <?php fileshow("ProofGeneral-3.1pre000309/isa/todo","isa to do"); ?>, + <?php fileshow("ProofGeneral-3.1pre000309/isar/todo","isar to do"); ?>, + <?php fileshow("ProofGeneral-3.1pre000309/hol98/todo","hol to do"); ?>. <!-- end WARNING --> </li> </ul> +<!-- <ul> --> +<!-- <li> --> +<!-- Browse source files from the current pre-release: --> +<!-- <?php fileshow("ProofGeneral-3.1pre000309/generic/proof.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.1pre000309/generic/proof-site.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.1pre000309/generic/proof-config.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.1pre000309/generic/proof-script.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.1pre000309/generic/proof-shell.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.1pre000309/generic/proof-toolbar.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.1pre000309/generic/proof-syntax.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.1pre000309/generic/proof-splash.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.1pre000309/generic/proof-easy-config.el") ?>. --> +<!-- </ul> --> <ul> <li> <?php hlink("feedback.phtml","Send us a message ","Feedback form")?> diff --git a/html/develdownload.phtml b/html/develdownload.phtml index 97728d91..1c3fa2bc 100644 --- a/html/develdownload.phtml +++ b/html/develdownload.phtml @@ -4,10 +4,10 @@ ?> <p> -Here is the latest pre-release of Proof General, made available -for those who wish to test the latest features or bug fixes. -For developers, this release is also available as a complete archive, -including forthcoming support for more proof assistants. +<a href="#prerel">Here</a> is the latest pre-release of Proof General, +made available for those who wish to test the latest features or bug +fixes. For developers, this release is also available as a +<a href="#devel">complete CVS snapshot</a>. </p> <p> Pre-releases of Proof General may be buggy as we add new features and @@ -45,6 +45,15 @@ the planned changes to come. <!-- End Warning. --> </ul> +For install instructions, see +the <?php link_root("download#install",stable version download") ?>. + +<p> +</p> +<p> +</p> + + <!-- WARNING! Line below automatically edited by makefile. --> <h2><a name="devel">Complete Archive of ProofGeneral-3.1pre000310 for Developers</a></h2> <!-- End Warning. --> @@ -64,31 +73,19 @@ What's the difference from the user's pre-release above? The complete archive also includes: </p> <ul> - <li> provisional instantiations of Proof General to new provers <br> - (mentioned in the - <!-- WARNING! Line below automatically edited by makefile. --> - <?php fileshow("ProofGeneral-3.1pre000310/CHANGES","CHANGES"); ?> file), - <!-- End Warning. --> - </li> - <li> the - <!-- WARNING! Line below automatically edited by makefile. --> - <?php fileshow("ProofGeneral-3.1pre000310/todo","generic low-level list of things to do"); ?> - and for each prover: - <?php fileshow("ProofGeneral-3.1pre000310/isa/todo","isa to do"); ?>, - <?php fileshow("ProofGeneral-3.1pre000310/isar/todo","isar to do"); ?>, - <?php fileshow("ProofGeneral-3.1pre000310/coq/todo","coq to do"); ?>, - <?php fileshow("ProofGeneral-3.1pre000310/lego/todo","lego to do"); ?>. - <!-- End Warning. --> + <li> the low-level developer's todo files + (see <?php link_root("devel#lowleveltodo","the developers page") ?>) and the detailed <!-- WARNING! Line below automatically edited by makefile. --> <?php fileshow("ProofGeneral-3.1pre000310/ChangeLog","ChangeLog"); ?>, <!-- End Warning. --> </li> - <li> developer's Makefile used to generate documentation files <br> - and the release itself from our CVS repository, </li> - <li> some test files, </li> - <li> sources for some of the images, - <li> the web pages. + <li> developer's Makefile used to generate documentation files + and the release itself,</li> + <li> test files, </li> + <li> image source files, </li> + <li> the web pages, </li> + <li> working instantiations of Proof General for new provers </li> </ul> <p> Note: there are no pre-built documentation files in the developer's diff --git a/html/download.phtml b/html/download.phtml index 3078bff5..4d692215 100644 --- a/html/download.phtml +++ b/html/download.phtml @@ -57,7 +57,7 @@ of <a href="http://www.xemacs.org">XEmacs</a> <a href="http://sunsite.doc.ic.ac.uk/Mirrors/ftp.xemacs.org/pub/xemacs/"> ftp mirror</a> may help). <br> -<b>or</b> version 20.2 or later (20.4 recommended) of the much poorer +<b>or</b> version 20.2 or later (20.5 recommended) of the much poorer <a href="http://www.gnu.org/software/emacs/">FSF GNU Emacs</a>. <br> Both Emacsen are available for a variety of platforms, including @@ -85,21 +85,21 @@ package. for installation notes. <br>X-Symbol presently only works with XEmacs. </li> -<li> -For FSF Emacs, a version of <tt>func-menu.el</tt> to get -<?php link_root("features#funcmenu","function menus") ?>. -<br>Unfortunately I can't find a version of this that -works with current FSF Emacs releases. I'd be grateful -for a pointer to one. -<br> -(The package -<tt>imenu.el</tt> may be a suitable replacement, -and it ships with both Emacsen. Perhaps -somebody could contribute patches to use that -instead of <tt>func-menu</tt>). +<!-- <li> --> +<!-- For FSF Emacs, a version of <tt>func-menu.el</tt> to get --> +<!-- <?php link_root("features#funcmenu","function menus") ?>. --> +<!-- <br>Unfortunately I can't find a version of this that --> +<!-- works with current FSF Emacs releases. I'd be grateful --> +<!-- for a pointer to one. --> +<!-- <br> --> +<!-- (The package --> +<!-- <tt>imenu.el</tt> may be a suitable replacement, --> +<!-- and it ships with both Emacsen. Perhaps --> +<!-- somebody could contribute patches to use that --> +<!-- instead of <tt>func-menu</tt>). --> </ul> <p> -All components mentioned are distributed under the GPL license. +All components mentioned above are distributed under the GPL license. </p> <br> <br> @@ -150,15 +150,21 @@ Check the <?php fileshow("ProofGeneral-3.0/CHANGES","CHANGES"); ?> file for a summary of changes since version 2.1. <p> Check the latest <?php fileshow("ProofGeneral/BUGS","BUGS"); ?> file -before reporting problems. If you find a problem not mentioned -there, please +(also +<?php fileshow("ProofGeneral/lego/BUGS","lego/BUGS, "); ?> +<?php fileshow("ProofGeneral/coq/BUGS","coq/BUGS, "); ?> +<?php fileshow("ProofGeneral/isa/BUGS","isa/BUGS, "); ?> +<?php fileshow("ProofGeneral/isar/BUGS","isar/BUGS," ); ?> +<?php fileshow("ProofGeneral/hol98/BUGS","hol98/BUGS"); ?>) +before reporting problems. If you find a problem not already mentioned, +please <?php hlink("feedback.phtml","send us a note","Feedback form")?>. </p> <br> <br> -<h3> Easy installation! </h3> +<h3><a name="install">Easy installation!</a></h3> <p> To use Proof General, simply unpack the sources with </p> diff --git a/html/elispmarkup.php3 b/html/elispmarkup.php3 new file mode 100644 index 00000000..a18586c9 --- /dev/null +++ b/html/elispmarkup.php3 @@ -0,0 +1,134 @@ +<?php +// +// Markup Emacs Lisp and Outline files +// +// David Aspinall, March 2000 +// +// $Id$ +// +// + +function isexpanded($headingno,$expanded) { + // print "testing $headingno"; + $all = ereg("all",$expanded); + $thisone = ereg("," . $headingno,$expanded); + return ($all ? ! $thisone : $thisone); +} + +function addexpanded($headingno,$expanded) { + $all = ereg("all",$expanded); + return ($all ? str_replace("," . $headingno,"",$expanded) : + $expanded . "," . $headingno); +} + +function removeexpanded($headingno,$expanded) { + $all = ereg("all",$expanded); + return ($all ? $expanded . "," . $headingno : + str_replace("," . $headingno,"",$expanded)); +} + +function link_toggle($headingno,$text,$thispage,$filename,$expanded) { + if (isexpanded($headingno,$expanded)) { + $newexpanded=removeexpanded($headingno,$expanded); + } else { + $newexpanded=addexpanded($headingno,$expanded); + } + print "<a name=\"$headingno\"><a href=\"$thispage"; + print "?file=" . urlencode($filename); + print "&expanded=" . urlencode($newexpanded) . "#" . $headingno . "\">" . $text . "</a></a>\n"; +} + +// FIXME: this is a nonsense really. Might be okay if it +// used dynamic HTML but it's too much of a faff at the moment. +// Also, we should use the tree structure properly and keep a stack! + +function outline_markup($filename,$thispage,$expanded) { + if ($title=="") { $title=$filename; }; + $outline = false; + $file = file($filename); + $i = 0; + $level=0; + $headingno=0; + /* Now parse file, watching for outline headers */ + for (;$i < count($file);$i++) { + $line = $file[$i]; + // HTML escapes + $line = htmlentities($line); + // Anchors for URLs + $line = ereg_replace("((http://|mailto:)[-a-zA-Z0-9\.~/_@]+)","<a href=\"\\1\">\\1</a>",$line); + // Assume a heading + $multipar=false; + if (ereg("-\*- (mode:)?outline -\*-",$line)) { + // Found line with outline mode header, set flag + // and print message + $outline = true; + print "<p><i>"; + print "This is a flattened outline file: click on a title to hide/reveal the leaf underneath it."; + print "<br>Click "; + print "<a href=\"$thispage?file=" . urlencode($filename); + print "&expanded=all\">here</a> to show body, or "; + print "<a href=\"$thispage?file=" . urlencode($filename); + print "\">here</a> to hide all."; + print "</i></p>\n"; + } elseif ($outline) { + if (ereg("^ *\n",$line)) { + // if (!newpara) { print "</p><p>\n"; }; + $newpara = true; + } elseif (ereg("^([\*]+) (.*)\n",$line,$heading)) { + $newlevel = strlen($heading[1])+1; + // if ($newlevel < $level) { + // Up a level + // $p = strpos($path,"-"); + // $path = substr($path,0,$p-1); + if ($newpara && + $level<=$newlevel && + isexpanded($headingno,$expanded)) { print "<p>\n"; } + $headingno++; + $level=$newlevel; + $text="<h$level>$heading[2]</h$level>"; + link_toggle($headingno,$text,$thispage,$filename,$expanded); + } elseif (isexpanded($headingno,$expanded)) { + if ($newpara && $level==0) { print "<p>\n"; } + print $line; + $newpara=false; + $level=0; + } + } else { + print $line; + } + } +} + +// +// For browsing source. Unfinished. +// + +function elisp_markup($filename,$thispage,$title="") { + if ($title=="") { $title=$filename; }; + $file = file($filename); + $i = 0; + $level=0; + $headingno=0; + /* Now parse file, watching for outline headers */ + for (;$i < count($file);$i++) { + $line = $file[$i]; + // HTML escapes + $line = htmlentities($line); + // Anchors for URLs + $line = ereg_replace("((http://|mailto:)[-a-zA-Z0-9\.~/_@]+)","<a href=\"\\1\">\\1</a>",$line); + // Font-lock equivalents... + // 1. comments + $line = ereg_replace("(;+.*\n)", + "<div style=\"color: #8080E0\">\\1</div>", + $line); + // 2. keywords + // FIXME: this inserts CR's. + $line = ereg_replace("^\(def(macro|un|var|custom|const|group)", + "(<div style=\"color: #C0B0B0\">def\\1</div>", + $line); + // FIXME: add hrefs for keywords, looking up in TAGS file. + // FIXME: add line numbers + // FIXME: parse strings + print $line; + } +} diff --git a/html/features.phtml b/html/features.phtml index c2c6dc89..89ad9fd1 100644 --- a/html/features.phtml +++ b/html/features.phtml @@ -67,10 +67,11 @@ If not, read on… <?php dt("Multiple files.","multiple") ?> <dd> Script management in Proof General can work across many script - files. When a script is visited in the editor, it is locked - (coloured) to reflect whether the proof assistant has loaded it in - this session. When a file is unlocked, all of the files which - depend on it are automatically unlocked too. + files, integrating with the file handling of + the proof assistant. When a script is visited in the editor, it + is locked (coloured) to reflect whether the proof assistant has + loaded it in this session. When a file is unlocked, all of the + files which depend on it are automatically unlocked too. <p> Dependencies between script files are either communicated from the proof assistant to Proof General, or maintained automatically by @@ -128,8 +129,9 @@ If not, read on… Instead of seeing "not P", you see "¬ P", instead of "a * b", you see "a × b", etc. <br> - [the examples above are simple so they will work on most browsers - without needing images] + (Those examples are simple so they will work on most browsers + without needing images, see the + <a href="screenshot.phtml">screenshots</a> for more examples.) <p> <?php footnote("X-Symbol currently works in XEmacs only") ?> </dd> @@ -153,8 +155,8 @@ If not, read on… <dd> Tags are an editing feature which allow you to quickly locate the definition or declaration of a particular identifier. Proof General - is supplied with utilities to make tag indexes for Emacs, for the - proof assistants LEGO and Coq. This makes it easy to quickly access + is supplied with utilities to make tag indexes for Emacs. + This makes it easy to quickly access definitions from a standard library, for example, and in large proof developments split across multiple files. <!-- <?php footnote("Tags programs are provided for LEGO and Coq") ?> --> diff --git a/html/fileshow.phtml b/html/fileshow.phtml index 6e984bdf..741ef556 100644 --- a/html/fileshow.phtml +++ b/html/fileshow.phtml @@ -1,7 +1,9 @@ <?php require('functions.php3'); + require('elispmarkup.php3'); $filename=$HTTP_GET_VARS["file"]; $title=$HTTP_GET_VARS["title"]; + $expanded=$HTTP_GET_VARS["expanded"]; if ($title=="") { $title = $filename; }; small_header($title); print "<pre>\n"; @@ -10,8 +12,10 @@ substr($filename,0,1)=="/" or substr($filename,0,1)=="~") { print "Sorry, can't show you that file!\n"; - } else { - markup_plain_text($filename); + } elseif (substr($filename,-3)==".el") { + elisp_markup($filename,"fileshow.phtml"); + else { + outline_markup($filename,"fileshow.phtml",$expanded); } print "</pre>\n"; print "<hr>"; diff --git a/html/main.phtml b/html/main.phtml index e6d9f997..5c0a3068 100644 --- a/html/main.phtml +++ b/html/main.phtml @@ -17,6 +17,15 @@ For detailed version numbers, check the </p> <p> +To read more about what features Proof General +provides, +<?php link_root("features","click here") ?>. +<br> +To see what Proof General looks like in use, have a look at these +<a href="screenshot.phtml">screenshots</a>. +</p> + +<p> Proof General is ready-customized for several proof assistants, including: </p> @@ -28,7 +37,7 @@ including: "<img src=\"images/coq-badge.gif\" width=110 height=35 border=0 alt=\"Coq badge\">","The Coq Home Page") ?> </td> <td> - <b> Coq Proof General </b> for + <b><?php fileshow("ProofGeneral/coq/README","Coq Proof General "); ?></b> for <?php hlink("http://pauillac.inria.fr/coq/assis-eng.html", "Coq","The Coq Home Page") ?> <br> @@ -47,7 +56,7 @@ including: "<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">", "The LEGO Home Page") ?> </td> - <td><b>LEGO Proof General</b> for + <td><b><?php fileshow("ProofGeneral/lego/README","LEGO Proof General "); ?></b> for <?php hlink("http://www.dcs.ed.ac.uk/home/lego", "LEGO","The LEGO Home Page") ?> <br> @@ -69,7 +78,7 @@ including: "<img src=\"images/isabelle-badge.gif\" width=128 height=37 border=0 alt=\"Isabelle badge\">", "The Isabelle Home Page"); ?> </td> - <td><b> Isabelle Proof General </b> for + <td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/", "Isabelle", "The Isabelle Home Page"); ?> <br> @@ -78,7 +87,7 @@ including: <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>. <br> Additional maintainance, support for - <a href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar</a> + <?php fileshow("ProofGeneral/isar/README","Isabelle/Isar "); ?> by <a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>. </div> @@ -86,6 +95,13 @@ including: </tr> </table> <p> +There is also a preliminary version of +<b><?php fileshow("ProofGeneral/hol98/README","HOL Proof General "); ?></b>, for +<a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL98</a>. +We are seeking a volunteer from the HOL community to support +and improve this (perhaps also supporting other HOL variants). +</p> +<p> Proof General is ready to be customized to new proof assistants. <br> It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", @@ -94,15 +110,6 @@ It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", Full documentation on configuration is provided. </p> -<p> -To read more about what features Proof General -provides, -<?php link_root("features","click here") ?>. -<br> -To see what Proof General looks like in use, have a look at these -<a href="screenshot.phtml">screenshots</a>. -</p> - <p> You can download Proof General diff --git a/html/mission.phtml b/html/mission.phtml new file mode 100644 index 00000000..00f7b60f --- /dev/null +++ b/html/mission.phtml @@ -0,0 +1,138 @@ +<?php + require('functions.php3'); + small_header("Proof General Mission (draft)"); + ?> + +<center> +<h2>Mission Statement</h2> +<h2>Proof General Developers</h2> +<h2>March 2000</h2> +</center> + +<p> +We seek to provide an interface suite for helping users interact with +<a href="#pas"><i>proof assistants</i></a>. +</p> + +<p> +Our approach is based on these principles: +<ul> +<li> +Be useful to both <a href="#experts"><i>experts and novices</i></a>. +</li> +<li> +Be <a href="scalable"><i>scalable</i></a> to large proof developments. +</li> +<li> +Be <a href="#learn"><i>easy to learn</i></a>, +yet still provide advanced features. +</li> +<li> +Be <a href="#generic"><i>generic</i></a> +to support many proof assistants with +a uniform interaction mechanism. +</li> +<li> +Be a <a href="#quality"><i>high-quality</i></a> research prototype. +</li> +</ul> +</p> +<p> +Above all, we take a <i>pragmatic</i> approach to constructing +interfaces. Our primary aim is to provide a tool which is +immediately useful for proof engineering, rather than +to provide publications by conducting research in +human-computer interaction. +</p> +<p> +This aim means that we harness a range of +<a href="#proven">proven techniques</a> +reimplemented in our generic system. +Nevertheless, by the act of constructing Proof General, we do invent +and incorporate some <a href="#novel">novel advances</a> which +contribute to research in the field. +</p> + +<hr> +<p> +</p> +<h2>Footnotes and elaboration</h2> + +<dl> +<?php dt("Proof assistants.","pas") ?> +<dd> +Computer programs for constructing formal machine proofs. Terminology +varies; we include all kinds of theorem proving systems +which involve user interaction while a proof is constructed. +We currently focus on systems based on a notion of <i>proof +script</i>, which is a file containing a user-level representation +of the proof or how it was constructed. +</dd> +<?php dt("Experts and novices.","experts") ?> +<dd> +Many interfaces for proof assistants are aimed at novice or beginner +users (and often used for teaching). Instead, we want to provide an +interface which is useful for expert users in the first place. +But we believe such a system can also be helpful for beginner users. +</dd> +<?php dt("Scalability.","scalable") ?> +<dd> +Some interfaces fail to scale to large proof developments; +we want Proof General to be useful for real-life, large +projects, consisting of many theorems and theories. +</dd> +<?php dt("Easy to learn.","learn") ?> +<dd> +It is difficult enough to learn how to use the logic and language +of a proof assistant, without an extra effort for learning its +interface. We want to provide a friendly interface with +intuitive features, hence a shallow learning curve. +</dd> +<?php dt("Genericity.","generic") ?> +<dd> +Proof General is intended to be used with a variety of underlying +proof assistants. We appreciate that different proof assistants are +based on different logical principles, and implement different proof +languages. Yet interaction between different systems often has a +similar behaviour. We exploit this to provide a good user interface +for many systems at once, saving repeated development effort by proof +assistant implementors. It has the added benefit of providing a +uniform interaction mechanism between different systems, making it +easier for users to experiment with several proof assistants. +</dd> +<?php dt("High-quality.","quality") ?> +<dd> +The developers are working on Proof General in the academic sector, +and engineering work itself is not directly funded. Despite this, we +strive to follow good engineering practices to build a robust and +maintainable system, which users can easily install (or test on the +web). To this end, we employ open-source development with frequent +test releases before stable releases, and high-priority attention to +user suggestions and bug reports. We use CVS for source control, +a strategy of bottom-up successive improvement, and provide support +for each proof assistant by an experienced user/developer. +</dd> +<?php dt("Proven techniques.","proven") ?> +<dd> +Amongst other features, Proof General currently includes +<?php link_root("features#script","script management ") ?> +and +<?php link_root("features#pbp","proof-by-pointing") ?>, +both championed in +<a href="http://www-sop.inria.fr/croap/">Projet CROAP</a>. +</dd> +<?php dt("Novel advances.","novel") ?> +<dd> +Proof General also advances the state-of-the-art. +For example, we introduced proof-by-pointing in +an free-form environment, +and extended script management to handle +<?php link_root("features#multiple","multiple files") ?>. +</dd> +</dl> + + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/news.phtml b/html/news.phtml index 9131d56b..579c424c 100644 --- a/html/news.phtml +++ b/html/news.phtml @@ -6,15 +6,26 @@ </p> <ul> +<li><b>14th March 2000</b> +<p> +Release candidate for Proof General 3.1 available. +Pre-releases from now on are release candidates for version 3.1. +Please test and report any problems you find +(check the CHANGES and BUGS lists for issues known about +and/or resolved). Version 3.1 should be released next week. +</p> +</li> <li><b>10th March 2000</b> <p> New: <b>HOL Proof General</b>! It took me only a couple of hours to add a basic instantiation of -ProofGeneral for <a href="http://www.cl.cam.ac.uk/HVG/HOL/HOL.html">HOL98</a>. +ProofGeneral for +<a href="http://www.cl.cam.ac.uk/Researc/HVG/HOL/HOL.html">HOL98</a>. Most of this time was in trying to find out how to do things in HOL, I could have done with a HOL user to hand. But I thought it was high time HOL got a look-in. </p> +<p> HOL Proof General provides script management support, automatic multiple files, decoration of proof scripts and output. Character-sequence X Symbols as in Coq and LEGO. Although this is a @@ -30,6 +41,7 @@ instantiation myself. The HOL support is shipping in the current <a href="develdownload.phtml">development release</a>. </p> +</li> <li><b>15th February 2000</b> <p> There is now a new diff --git a/html/projects/hol.html b/html/projects/hol.html index 4b623bfb..6828899a 100644 --- a/html/projects/hol.html +++ b/html/projects/hol.html @@ -26,9 +26,14 @@ 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. +proof assistant behaviour, interest in HOL. </p><p> <b>Proposer:</b> <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>. diff --git a/html/proofgen.css b/html/proofgen.css index 3403c36e..5ad31b7f 100644 --- a/html/proofgen.css +++ b/html/proofgen.css @@ -25,6 +25,7 @@ h1{ font-family: Verdana, Arial, sans-serif; color: #FFFFFF; font-size: large; + font-series: bold } h2{ @@ -39,6 +40,18 @@ h3{ color: #FFFFD0 } +h4{ + font-family: Verdana, Arial, sans-serif; + font-size: medium; + color: #FFD0D0 +} + +h5{ + font-family: Verdana, Arial, sans-serif; + font-size: medium; + color: #E0C0C0 +} + blockquote,form,input,select{ font-family: Verdana, Arial, sans-serif; color: #FFFFFF |