diff options
Diffstat (limited to 'html')
121 files changed, 7583 insertions, 0 deletions
diff --git a/html/.cvsignore b/html/.cvsignore new file mode 100644 index 00000000..d6e10bc1 --- /dev/null +++ b/html/.cvsignore @@ -0,0 +1 @@ +ProofGeneral diff --git a/html/.htaccess b/html/.htaccess new file mode 100644 index 00000000..45e6575e --- /dev/null +++ b/html/.htaccess @@ -0,0 +1,2 @@ +RemoveHandler .html +AddType application/x-httpd-php .html diff --git a/html/FAQ b/html/FAQ new file mode 100644 index 00000000..4422a8f0 --- /dev/null +++ b/html/FAQ @@ -0,0 +1,5 @@ +<?php require('functions.php3'); + require('elispmarkup.php3'); + fileshowmarkup("ProofGeneral/FAQ", + "Frequently Asked Questions about using Proof General"); +?> diff --git a/html/Kit/Makefile b/html/Kit/Makefile new file mode 100644 index 00000000..b35b720b --- /dev/null +++ b/html/Kit/Makefile @@ -0,0 +1,11 @@ +# +# Update dtds from PG Kit repository. +# + +.PHONY: dtdupdate + +DTDTARGS=dtd/pgip.dtd dtd/pgml.dtd + +# checkout in temp dir because otherwise CVS complains of repo clash (fixes?) +dtdupdate: + mkdir dtdtmp; cvs -d :ext:da@localssh.dcs.ed.ac.uk:/home/proofgen/src export -kv -D today -d dtdtmp Kit/dtd; mv dtdtmp/* dtd; rmdir dtdtmp; cvs commit -m"Updated from Kit repo" dtd diff --git a/html/Kit/dtd/pgip.dtd b/html/Kit/dtd/pgip.dtd new file mode 100644 index 00000000..2861fff2 --- /dev/null +++ b/html/Kit/dtd/pgip.dtd @@ -0,0 +1,226 @@ +<?xml version="1.0" encoding="UTF-8"?> + +<!-- DTD for PGIP, the Proof General Interface Protocol --> +<!-- Author: David Aspinall, LFCS, University of Edinburgh --> +<!-- Version: pgip.dtd,v 1.6 2001/09/10 19:00:42 da Exp --> + +<!-- Status: Incomplete. --> +<!-- For commentary, see the Proof General Kit white paper, --> +<!-- available from http://www.proofgeneral.org/kit --> + + +<!ELEMENT pgip (%provermsg; | %kitmsg;)*> +<!ATTLIST pgip + version CDATA + class CDATA #IMPLIED + origin CDATA + id CDATA> + + +<!-- STATUS/ERROR MESSAGES --> +<!-- ===================== --> + +<!ELEMENT information (#PCDATA)> +<!ATTLIST information + kind CDATA #IMPLIED + location CDATA #IMPLIED> + +<!-- kind=message,urgentmessage,display --> + +<!ELEMENT error (#PCDATA)> +<!ATTLIST error + kind CDATA #IMPLIED + location CDATA #IMPLIED> + +<!-- kind=warning,fatal,interrupt --> + +<!ENTITY % proverstatus "information | error"> + + + +<!-- CONFIGURATION MESSAGES --> +<!-- ====================== --> + +<!ENTITY % kitconfig "usespgml | haspref | prefval | idtable | + addid | delid | menuadd | menudel | guiconfig"> + +<!-- This is how it should be: + <!ENTITY % pgml SYSTEM "pgml.dtd"> + --> + +<!-- Types for config settings --> + +<!ELEMENT pgipbool EMPTY> +<!ELEMENT pgipint (#PCDATA)> +<!ELEMENT pgipstring (#PCDATA)> +<!ELEMENT pgipchoice (pgipchoiceitem+)> +<!ELEMENT pgipchoiceitem (#PCDATA)> +<!ATTLIST pgipchoiceitem + tag CDATA #IMPLIED> + +<!ENTITY % pgiptype "pgipbool | pgipint | pgipstring | pgipchoice"> + + +<!ELEMENT usespgml EMPTY> +<!ATTLIST usespgml + version CDATA #IMPLIED> + +<!ELEMENT haspref pgiptype> +<!ATTLIST haspref + default CDATA #IMPLIED + class CDATA #IMPLIED> + +<!ELEMENT prefval (#PCDATA)> +<!ATTLIST prefval + name CDATA #IMPLIED> + +<!ELEMENT idtable (#PCDATA)> +<!ATTLIST idtable + class CDATA #IMPLIED> + +<!ELEMENT addid (#PCDATA)> +<!ATTLIST addid + class CDATA #IMPLIED> + +<!ELEMENT delid (#PCDATA)> +<!ATTLIST delid + class CDATA #IMPLIED> + +<!ELEMENT menuadd (#PCDATA)> +<!ATTLIST menuadd + path CDATA #IMPLIED + name CDATA #IMPLIED> + +<!ELEMENT menudel (#PCDATA)> +<!ATTLIST menudel + path CDATA #IMPLIED + name CDATA #IMPLIED> + + +<!-- gui configuration --> + +<!-- the PCDATA is the icon, base64-encoded --> +<!ELEMENT objtype (#PCDATA)> +<!ATTLIST objtype + name CDATA #REQUIRED> + +<!ELEMENT opn (opsrc, optrg, opcmd)> +<!ATTLIST opn + name CDATA #REQUIRED> + +<!-- source types as space-separated list; target type is a single type --> +<!ELEMENT opsrc (#PCDATA)> +<!ELEMENT optrg (#PCDATA)> +<!-- the prover command, with a printf "%1"-style substitution of arguments --> +<!ELEMENT opcmd (#PCDATA)> + +<!-- proof operations (no target sort) --> +<!ELEMENT proofopn (opsrc, opcmd)> +<!ATTLIST opn + name CDATA #REQUIRED> + +<!-- interactive operations-- require some input --> +<!ELEMENT iopn (inputform, opsrc, optrg, opcmd)> +<!ATTLIST iopn + name CDATA #REQUIRED> + +<!-- an input form is a list of fields --> +<!ELEMENT inputform (field)+> +<!-- and a field has a type (int, string, bool, choice(c1...cn)) --> +<!-- and a name; under that name, it will be substituted into the command --> +<!-- Ex. field name=number opcmd="rtac %1 %number" --> +<!-- the PCDATA is the prompt for the input field --> +<!ELEMENT field (pgiptype)> +<!ATTLIST field + type CDATA #REQUIRED + name CDATA #REQUIRED> + + +<!ELEMENT guiconfig (objtype*, opn*, iopn*, proofopn*) > + + + +<!ENTITY % proverconfig "askpgml | askprefs | resetprefs | + setpref | getpref"> + +<!ELEMENT askpgml EMPTY> + +<!ELEMENT askprefs EMPTY> +<!ATTLIST askprefs + class CDATA #IMPLIED> + +<!ELEMENT resetprefs EMPTY> +<!ATTLIST resetprefs + class CDATA #IMPLIED> + +<!ELEMENT setpref EMPTY> +<!ATTLIST setpref + class CDATA #IMPLIED> + +<!ELEMENT getpref EMPTY> +<!ATTLIST getpref + class CDATA #IMPLIED> + + + +<!-- COMMANDS --> +<!-- ======== --> + +<!ELEMENT provercmd (#PCDATA)> + +<!ELEMENT goalcmd (#PCDATA)> + +<!ELEMENT undocmd EMPTY> + +<!ELEMENT abortcmd EMPTY> + +<!ELEMENT closecmd (#PCDATA) + goalid CDATA #REQUIRED> + +<!ELEMENT postponecmd (#PCDATA) + goalid CDATA #REQUIRED + thmname CDATA #REQUIRED> + +<!ELEMENT savecmd EMPTY> +<!ATTLIST savecmd + thmname CDATA #REQUIRED> + +<!ELEMENT forgetcmd EMPTY> +<!ATTLIST forgetcmd + thmname CDATA #REQUIRED> + +<!ELEMENT restorecmd EMPTY> +<!ATTLIST restorecmd + goalid CDATA #REQUIRED> + +<!ELEMENT loadfilecmd (#PCDATA)> + +<!ELEMENT retractfilecmd (#PCDATA)> + +<!ENTITY % command "provercmd | goalcmd | undocmd | savecmd | forgetcmd | + closecmd | quitcmd | postponecmd | restorecmd | + loadfilecmd | retractfilecmd"> + +<!-- savecmd Finishes a proof and saves a new theorem + closecmd Temporarily closes a proof and saves state with given id + postponecmd As closecmd, but saves a new theorem and + generates a proof obligation + --> + + + + +<!-- Roots of PGIP messages --> + +<!-- Messages sent to PG Kit components --> + +<!ENTITY % kitmsg "%kitconfig | %proverstatus"> + +<!-- Messages sent to proof assistant (class "pa") --> + +<!ENTITY % provermsg "proverconfig"> + + + + +<!ELEMENT br EMPTY> diff --git a/html/Kit/dtd/pgml.dtd b/html/Kit/dtd/pgml.dtd new file mode 100644 index 00000000..d484c100 --- /dev/null +++ b/html/Kit/dtd/pgml.dtd @@ -0,0 +1,75 @@ +<?xml version="1.0" encoding="UTF-8"?> + +<!-- DTD for PGML, the Proof General Markup Language --> +<!-- Author: David Aspinall, LFCS, University of Edinburgh --> +<!-- Version: pgml.dtd,v 1.6 2001/09/10 16:04:17 da Exp --> + +<!-- Status: Complete but experimental version. --> +<!-- For commentary, see the Proof General Kit white paper, --> +<!-- available from http://www.proofgeneral.org/kit --> + + +<!ELEMENT pgml (statedisplay | termdisplay | information | warning | error)*> +<!ATTLIST pgml + version CDATA #IMPLIED> + +<!ELEMENT statedisplay (statepart)*> +<!ATTLIST statedisplay + systemid CDATA #IMPLIED + name CDATA #IMPLIED + kind CDATA #IMPLIED> + +<!ENTITY % termitem "action | term | type | atom | sym"> +<!ENTITY % nonactionitem "term | type | atom | sym"> + +<!ELEMENT information (#PCDATA | %termitem;)*> +<!ATTLIST information + name CDATA #IMPLIED + kind CDATA #IMPLIED> + +<!ELEMENT warning (#PCDATA | %termitem;)*> +<!ATTLIST warning + name CDATA #IMPLIED + kind CDATA #IMPLIED> + +<!ELEMENT error (#PCDATA | %termitem;)*> +<!ATTLIST error + name CDATA #IMPLIED + kind CDATA #IMPLIED> + +<!ELEMENT statepart (#PCDATA | %termitem;)*> +<!ATTLIST statepart + name CDATA #IMPLIED + kind CDATA #IMPLIED> + +<!ELEMENT termdisplay (#PCDATA | %termitem;)*> +<!ATTLIST termdisplay + name CDATA #IMPLIED + kind CDATA #IMPLIED> + +<!ELEMENT term (#PCDATA | %termitem;)*> +<!ATTLIST term + pos CDATA #IMPLIED + kind CDATA #IMPLIED> + +<!-- maybe combine this with term and add extra attr to term? --> +<!ELEMENT type (#PCDATA | %termitem;)*> +<!ATTLIST type + kind CDATA #IMPLIED> + +<!ELEMENT action (#PCDATA | %nonactionitem;)*> +<!ATTLIST action + kind CDATA #IMPLIED> + +<!ELEMENT atom (#PCDATA)> +<!ATTLIST atom + kind CDATA #IMPLIED + fullname CDATA #IMPLIED> + +<!ELEMENT sym (#PCDATA)> +<!ATTLIST sym + name CDATA #IMPLIED + alt CDATA #IMPLIED> + +<!ELEMENT br EMPTY> + diff --git a/html/ProofGeneralPortrait.eps.gz b/html/ProofGeneralPortrait.eps.gz Binary files differnew file mode 100644 index 00000000..97feb1a4 --- /dev/null +++ b/html/ProofGeneralPortrait.eps.gz diff --git a/html/about b/html/about new file mode 100644 index 00000000..a58717d8 --- /dev/null +++ b/html/about @@ -0,0 +1,5 @@ +<?php include('index.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?>
\ No newline at end of file diff --git a/html/about.html b/html/about.html new file mode 100644 index 00000000..2c8e03db --- /dev/null +++ b/html/about.html @@ -0,0 +1,54 @@ +<h2>Contact information</h2> + +<p> +Have you any questions, comments, or suggestions about Proof General? +<br> +Send us a message using <a href="feedback">this form</a> +or by email to +<?php mlinktxt($project_feedback, "$project_feedback"); ?>. +<br> +Receive announcements and discuss Proof General on +our <a href="mailinglist">mailing +list</a>. +</p> + +<h2>About the Proof General project</h2> +<p> +The forefather of Proof General was LEGO mode, begun in 1994 at the <a +href="http://www.lfcs.informatics.ed.ac.uk">LFCS</a> by Thomas Kleymann. LEGO +mode was an Emacs-based front end for LEGO similar to David Aspinall's +<a href="http://homepages.inf.ed.ac.uk/da/Isamode">Isamode</a>, +developed at the LFCS since 1992. After 1994, implementations of +proof-by-pointing and script management were added to LEGO mode, and +the code was made generic. The generic basis was developed by +Thomas Kleymann, Dilip Sequeira, Healfdene Goguen and David Aspinall. +The current authors and maintainers of the various instantiations of +Proof General are mentioned on the +<a href="main">front page</a>. +</p> +<p> +The Proof General project was coordinated until October 1998 by +Thomas Kleymann, and since then by David Aspinall. The project has +benefited from funding by +<!-- this link is broken: <a href="http://www.dcs.ed.ac.uk/lfcs/research/logic_and_proof/attbpa.html"> --> +EPSRC, +<!-- (Applications of a Type Theory based Proof Assistant) --> +<!-- </a>, --> +the <a +href="http://www.dcs.ed.ac.uk/lfcs/research/types_bra/index.html">EC</a>, +and the <a href="http://www.lfcs.informatics.ed.ac.uk">LFCS</a>. +</p> + +<p> +David Aspinall designed the web pages and graphics for Proof General. +<br> +Check the <a href="gallery">gallery</a> for more publicity +pictures! +</p> +<p> +For more on the history of the development of +the Proof General program, see the +<?php htmlshow("ProofGeneral/doc/ProofGeneral_1.html#SEC3","manual preface.","","html") ?> +</p> + +<?php include('links.html') ?> diff --git a/html/adaptingman b/html/adaptingman new file mode 100644 index 00000000..74a3152c --- /dev/null +++ b/html/adaptingman @@ -0,0 +1,3 @@ +<?php require('functions.php3'); + hack_html("ProofGeneral/doc/PG-adapting_toc.html","Proof General adapting manual"); +?> diff --git a/html/components b/html/components new file mode 100644 index 00000000..7f600582 --- /dev/null +++ b/html/components @@ -0,0 +1,5 @@ +<?php include('components.html'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?> diff --git a/html/components.html b/html/components.html new file mode 100644 index 00000000..7d2b10e9 --- /dev/null +++ b/html/components.html @@ -0,0 +1,72 @@ +<?php + require('functions.php3'); + small_header("Proof General Standalone Components"); + ?> + +<p> As part of the Proof General project, some components have been +developed which might be useful in a wider context. They are +presented on this page. +</p> + +<p>As usual with free software, these programs +come with no guarantees of any sort. +Nonetheless, please <a href="feedback">contact us</a> with +any comments, suggestions, or problems. +</p> + +<h2>Spans: Emacs and XEmacs compatibility library for overlays/extents</h2> + +<p> +<i>Spans</i> are an abstraction of XEmacs <i>extents</i> used to help +bridge the gulf between GNU Emacs and XEmacs. In GNU Emacs, spans are +implemented using <i>overlays</i>. +</p> +<p> +The library consists of three Emacs lisp files, +<ul> +<li><a href="ProofGeneral-latest/generic/span-extent.el">span-extent.el</a> +</li> +<li><a href="ProofGeneral-latest/generic/span-overlay.el">span-overlay.el</a> +</li> +<li><a href="ProofGeneral-latest/generic/span.el">span.el</a> +(which simply loads one of the above) +</li> +</ul> +which implement a common interface for overlays/extents. +This library was originally implemented by Healfdene Goguen. +</p> +<p> +See the files for further documentation, and +<a href="adapting_13.html#SEC40">section 12.1</a> +of the <a href="adapting">Proof General adapting manual</a> +for more details. +</p> + + +<h2>Docstring magic: Elisp documentation to TeXinfo extraction</h2> + +<p> +This package generates <a +href="http://www.gnu.org/directory/texinfo.html">Texinfo</a> source +fragments from Emacs +<!-- WARNING: next URL subject to change with elisp ref man changes!! --> +<a href="http://www.gnu.org/manual/elisp/html_node/elisp_374.html#SEC374">documentation strings</a> which are embedded in Emacs lisp source and the +running interpreter. This avoids documenting functions +and variables in more than one place, and automatically adds Texinfo +markup to docstrings. It's a bit like <tt>javadoc</tt> for Emacs +Lisp, except that you must write a skeleton <tt>texi</tt> file which +contains magic comments mentioning the function or variable names you +want documented. </p> <p> The package consists of one file: <ul> +<li><a +href="ProofGeneral-latest/generic/texi-docstring-magic.el">texi-docstring-magic.el</a></li> +</ul> which contains documentation and usage hints. For an extensive +example of it's use, see the <a +href="ProofGeneral-latest/doc/PG-adapting.texi">source</a> for the <a +href="adapting">PG adapting manual</a>. </p> + +<hr> + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/counter.php3 b/html/counter.php3 new file mode 100644 index 00000000..0ea4593d --- /dev/null +++ b/html/counter.php3 @@ -0,0 +1,50 @@ +<?php +/* + * Increment an access counter. + * David Aspinall, June 1999. + * + * $Id$ + * + */ + +$counterFile = "counter.txt"; +$counterStart = "counterstart.txt"; +$maxlen = 10; + +// NB: probably have trouble with permissions +// if file doesn't exist already, so start with +// empty files made with touch. + +// Here's how to cause it to be initialized: +// +// rm -f counter.txt counterstart.txt +// touch counter.txt counterstart.txt +// chmod o+w counter.txt counterstart.txt +// + +if (is_readable($counterFile) && is_writeable($counterFile)) { + $fp = fopen($counterFile,"r+"); + if (filesize($counterFile)<1) { + // Start counter, write a timestamp. + $num = 1; + if (is_readable($counterStart) && is_writeable($counterStart)) { + $fps = fopen($counterStart,"w"); + fputs($fps,time()); + fclose($fps); + print "<!-- Hit counter initialized. -->"; + } else { + print "<!-- Hit counter initialized, but timestamp could not be set -->"; + }; + } else { + $num = fgets($fp,$maxlen); + $num += 1; + print "<!-- Hit counter: $num -->"; + }; + rewind($fp); + fputs($fp,$num); + fclose($fp); +} else { + print "<!-- Hit counter file $counterFile cannot be accessed. -->"; +}; +?> + diff --git a/html/cvsweb.cgi b/html/cvsweb.cgi new file mode 100644 index 00000000..9aee4f44 --- /dev/null +++ b/html/cvsweb.cgi @@ -0,0 +1,2685 @@ +#!/usr/bin/perl -ws +# +# cvsweb - a CGI interface to CVS trees. +# +# Written in their spare time by +# Bill Fenner <fenner@freebsd.org> (original work) +# extended by Henner Zeller <zeller@think.de>, +# Henrik Nordström <hno@hem.passagen.se> +# Ken Coar <coar@Apache.Org> +# +# Adjustments for Proof General pages by David Aspinall <da@dcs.ed.ac.uk> +# -- added hr, bighr, widehr, stylesheet. July 2000 +# +# Based on: +# * Bill Fenners cvsweb.cgi revision 1.28 available from: +# http://www.freebsd.org/cgi/cvsweb.cgi/www/en/cgi/cvsweb.cgi +# +# Copyright (c) 1996-1998 Bill Fenner +# (c) 1998-1999 Henner Zeller +# (c) 1999 Henrik Nordström +# All rights reserved. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions +# are met: +# 1. Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# 2. Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# +# THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND +# ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +# ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE +# FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +# DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS +# OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) +# HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY +# OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF +# SUCH DAMAGE. +# +# Original version tag +# Id: cvsweb.cgi,v 1.79 1999/11/03 08:05:29 hzeller Exp +# +# Proof General version tag +# $Id$ +# +# +### + +use strict; + +use vars qw ( + $config $allow_version_select $verbose + %CVSROOT %CVSROOTdescr %MIRRORS %DEFAULTVALUE %ICONS %MTYPES + %alltags @tabcolors %fileinfo %tags @branchnames %nameprinted + %symrev %revsym @allrevisions %date %author @revdisplayorder + @revisions %state %difflines %log %branchpoint @revorder $prcgi + $checkoutMagic $doCheckout $scriptname $scriptwhere + $where $Browser $nofilelinks $maycompress @stickyvars + %input $query $barequery $sortby $bydate $byrev $byauthor + $bylog $byfile $hr_default $logsort $cvstree $cvsroot + $mimetype $defaultTextPlain $defaultViewable $allow_compress + $GZIPBIN $backicon $diricon $fileicon $fullname $newname + $cvstreedefault $body_tag $logo $defaulttitle $footer + $backcolor $long_intro $short_instruction $shortLogLen + $show_author $dirtable $tablepadding $columnHeaderColorDefault + $columnHeaderColorSorted $hr_breakable $hr_funout $hr_ignwhite + $hr_ignkeysubst $diffcolorHeading $diffcolorEmpty $diffcolorRemove + $diffcolorChange $diffcolorAdd $diffcolorDarkChange $difffontface + $difffontsize $inputTextSize $mime_types $allow_annotate + $allow_markup $use_java_script $open_extern_window + $extern_window_width $extern_window_height $edit_option_form + $checkout_magic $show_subdir_lastmod $show_log_in_markup $v + $navigationHeaderColor $tableBorderColor $markupLogColor + $tabstop $state $annTable $sel $curbranch $HideModules @HideModules + $module $moddate $stylesheet $hr $widehr $bighr +); + +##### Start of Configuration Area ######## +# == EDIT this == +# User configuration is stored in +# $config = $ENV{'CVSWEB_CONFIG'} || '/etc/httpd/conf/cvsweb.conf'; +$config = "/home/proofgen/www/cvsweb.conf"; + +# == Configuration defaults == +# Defaults for configuration variables that shouldn't need +# to be configured.. +$allow_version_select = 1; + +##### End of Configuration Area ######## + +######## Configuration variables ######### +# These are defined to allow checking with perl -cw +%CVSROOT = %MIRRORS = %DEFAULTVALUE = %ICONS = %MTYPES = +%tags = %alltags = @tabcolors = (); +$cvstreedefault = $body_tag = $logo = $defaulttitle = $footer = +$backcolor = $long_intro = $short_instruction = $shortLogLen = +$show_author = $dirtable = $tablepadding = $columnHeaderColorDefault = +$columnHeaderColorSorted = $hr_breakable = $hr_funout = $hr_ignwhite = +$hr_ignkeysubst = $diffcolorHeading = $diffcolorEmpty = $diffcolorRemove = +$diffcolorChange = $diffcolorAdd = $diffcolorDarkChange = $difffontface = +$difffontsize = $inputTextSize = $mime_types = $allow_annotate = +$allow_markup = $use_java_script = $open_extern_window = +$extern_window_width = $extern_window_height = $edit_option_form = +$checkout_magic = $show_subdir_lastmod = $show_log_in_markup = $v = +$navigationHeaderColor = $tableBorderColor = $markupLogColor = +$tabstop = $moddate = $stylesheet = undef; + +##### End of configuration variables ##### + +use Time::Local; +use IPC::Open2; + +$verbose = $v; +$checkoutMagic = "~checkout~"; +$where = defined($ENV{'PATH_INFO'}) ? $ENV{'PATH_INFO'} : ""; +$doCheckout = ($where =~ /^\/$checkoutMagic/); +$where =~ s|^/($checkoutMagic)?||; +$where =~ s|/+$||; +($scriptname = $ENV{'SCRIPT_NAME'}) =~ s|^/?|/|; +$scriptname =~ s|/+$||; +if ($where) { + $scriptwhere = $scriptname . '/' . urlencode($where); +} +else { + $scriptwhere = $scriptname; +} +$scriptwhere =~ s|/+$||; + +# in lynx, it it very annoying to have two links +# per file, so disable the link at the icon +# in this case: +$Browser = defined($ENV{'HTTP_USER_AGENT'}) ? $ENV{'HTTP_USER_AGENT'} : "unknown"; +$nofilelinks = ($Browser =~ m'^Lynx/'); + +# newer browsers accept gzip content encoding +# and state this in a header +# (netscape did always but didn't state it) +# It has been reported that these +# braindamaged MS-Internet Exploders claim that they +# accept gzip .. but don't in fact and +# display garbage then :-/ +# Turn off gzip if running under mod_perl. piping does +# not work as expected inside the server. One can probably +# achieve the same result using Apache::GZIPFilter. +$maycompress =(( (defined($ENV{'HTTP_ACCEPT_ENCODING'}) ? $ENV{'HTTP_ACCEPT_ENCODING'} =~ m|gzip| : 0 ) + || $Browser =~ m%^Mozilla/3%) + && ($Browser !~ m/MSIE/) + && !defined($ENV{'MOD_PERL'})); + +# put here the variables we need in order +# to hold our state - they will be added (with +# their current value) to any link/query string +# you construct +@stickyvars = ('cvsroot','hideattic','sortby','logsort','f','only_with_tag'); + +if (-f $config) { + do "$config"; + $HideModules = "§" . join("§", @HideModules) . "§"; +} +else { + &fatal("500 Internal Error", + 'Configuration not found. Set the variable <code>$config</code> ' + . 'in cvsweb.cgi, or the environment variable ' + . '<code>CVSWEB_CONFIG</code>, to your <b>cvsweb.conf</b> ' + . 'configuration file first.'); +} + +undef %input; +if ($query = $ENV{'QUERY_STRING'}) { + foreach (split(/&/, $query)) { + s/%(..)/sprintf("%c", hex($1))/ge; # unquote %-quoted + if (/(\S+)=(.*)/) { + $input{$1} = $2 if ($2 ne ""); + } + else { + $input{$_}++; + } + } +} + +# For backwards compability, set only_with_tag to only_on_branch if set. +$input{only_with_tag} = $input{only_on_branch} + if (defined($input{only_on_branch})); + +foreach (keys %DEFAULTVALUE) +{ + # replace not given parameters with the default parameters + if (!defined($input{$_}) || $input{$_} eq "") { + # Empty Checkboxes in forms return -- nothing. So we define a helper + # variable in these forms (copt) which indicates that we just set + # parameters with a checkbox + if (!defined($input{"copt"})) { + # 'copt' isn't defined --> empty input is not the result + # of empty input checkbox --> set default + $input{$_} = $DEFAULTVALUE{$_} if (defined($DEFAULTVALUE{$_})); + } + else { + # 'copt' is defined -> the result of empty input checkbox + # -> set to zero (disable) if default is a boolean (0|1). + $input{$_} = 0 + if (defined($DEFAULTVALUE{$_}) + && ($DEFAULTVALUE{$_} eq "0" || $DEFAULTVALUE{$_} eq "1")); + } + } +} + +$barequery = ""; +foreach (@stickyvars) { + # construct a query string with the sticky non default parameters set + if (defined($input{$_}) && $input{$_} ne "" && $input{$_} ne $DEFAULTVALUE{$_}) { + if ($barequery) { + $barequery = $barequery . "&"; + } + my $thisval = urlencode($_) . "=" . urlencode($input{$_}); + $barequery .= $thisval; + } +} +# is there any query ? +if ($barequery) { + $query = "?$barequery"; + $barequery = "&" . $barequery; +} +else { + $query = ""; +} + +# get actual parameters +$sortby = $input{"sortby"}; +$bydate = 0; +$byrev = 0; +$byauthor = 0; +$bylog = 0; +$byfile = 0; +if ($sortby eq "date") { + $bydate = 1; +} +elsif ($sortby eq "rev") { + $byrev = 1; +} +elsif ($sortby eq "author") { + $byauthor = 1; +} +elsif ($sortby eq "log") { + $bylog = 1; +} +else { + $byfile = 1; +} + +$hr_default = $input{'f'} eq 'h'; + +$logsort = $input{"logsort"}; + + +## Default CVS-Tree +if (!defined($CVSROOT{$cvstreedefault})) { + &fatal("500 Internal Error", + "<code>\$cvstreedefault</code> points to a repository " + . "not defined in <code>%CVSROOT</code> " + . "(edit your configuration file $config)"); +} +$cvstree = $cvstreedefault; +$cvsroot = $CVSROOT{"$cvstree"}; + +# alternate CVS-Tree, configured in cvsweb.conf +if ($input{'cvsroot'}) { + if ($CVSROOT{$input{'cvsroot'}}) { + $cvstree = $input{'cvsroot'}; + $cvsroot = $CVSROOT{"$cvstree"}; + } +} + +# create icons out of description +foreach my $k (keys %ICONS) { + no strict 'refs'; + my ($itxt,$ipath,$iwidth,$iheight) = @{$ICONS{$k}}; + if ($ipath) { + $ {"${k}icon"} = "<IMG SRC=\"$ipath\" ALT=\"$itxt\" BORDER=\"0\" WIDTH=\"$iwidth\" HEIGHT=\"$iheight\">"; + } + else { + $ {"${k}icon"} = $itxt; + } +} + +# Do some special configuration for cvstrees +do "$config-$cvstree" if (-f "$config-$cvstree"); + +$fullname = $cvsroot . '/' . $where; +$mimetype = &getMimeTypeFromSuffix ($fullname); +$defaultTextPlain = ($mimetype eq "text/plain"); +$defaultViewable = $allow_markup && viewable($mimetype); + +# GIF and JPEG images are already compressed. +# Also, for some reason Netscape does not always likes compressed images. +# +if ($mimetype=="image/jpeg" || $mimetype=="image/gif") {$maycompress =0}; + +# search for GZIP if compression allowed +# We've to find out if the GZIP-binary exists .. otherwise +# ge get an Internal Server Error if we try to pipe the +# output through the nonexistent gzip .. +# any more elegant ways to prevent this are welcome! +if ($allow_compress && $maycompress) { + foreach (split(/:/, $ENV{PATH})) { + if (-x "$_/gzip") { + $GZIPBIN = "$_/gzip"; + last; + } + } +} + +if (-d $fullname) { + # + # ensure, that directories always end with (exactly) one '/' + # to allow relative URL's. If they're not, make a redirect. + ## + my $pathinfo = defined($ENV{'PATH_INFO'}) ? $ENV{'PATH_INFO'} : ""; + if (!($pathinfo =~ m|/$|) || ($pathinfo =~ m |/{2,}$|)) { + redirect ($scriptwhere . '/' . $query); + } + else { + $where .= '/'; + $scriptwhere .= '/'; + } +} + +if (!-d $cvsroot) { + &fatal("500 Internal Error",'$CVSROOT not found!<P>The server on which the CVS tree lives is probably down. Please try again in a few minutes.'); +} + +# +# See if the module is in our forbidden list. +# +$where =~ m:([^/]*):; +$module = $1; +if ($module && &forbidden_module($module)) { + &fatal("403 Forbidden", "Access to $where forbidden."); +} +############################## +# View a directory +############################### +elsif (-d $fullname) { + my $dh = do {local(*DH);}; + opendir($dh, $fullname) || &fatal("404 Not Found","$where: $!"); + my @dir = readdir($dh); + closedir($dh); + my @subLevelFiles = findLastModifiedSubdirs(@dir) + if ($show_subdir_lastmod); + getDirLogs($cvsroot,$where,@subLevelFiles); + + if ($where eq '/') { + html_header("$defaulttitle"); + print $long_intro; + } + else { + html_header("$where"); + print $short_instruction; + } + + print "<P><a name=\"dirlist\">\n"; + # give direct access to dirs + if ($where eq '/') { + chooseMirror(); + chooseCVSRoot(); + } + else { + print "<p>Current directory: <b>", &clickablePath($where,0), "</b>\n"; + + print "<P>Current tag: <B>", $input{only_with_tag}, "</b>\n" if + $input{only_with_tag}; + + } + + + print "<P>$hr\n"; + # Using <MENU> in this manner violates the HTML2.0 spec but + # provides the results that I want in most browsers. Another + # case of layout spooging up HTML. + + my $infocols = 0; + if ($dirtable) { + if (defined($tableBorderColor)) { + # Can't this be done by defining the border for the inner table? + print "<table border=0 cellpadding=0 width=\"100%\"><tr><td bgcolor=\"$tableBorderColor\">"; + } + print "<table width=\"100%\" border=0 cellspacing=1 cellpadding=$tablepadding>\n"; + $infocols++; + print "<tr><th align=left bgcolor=" . (($byfile) ? + $columnHeaderColorSorted : + $columnHeaderColorDefault) . ">"; + print "<a href=\"./" . &toggleQuery("sortby","file") . + "#dirlist\">" if (!$byfile); + print "File"; + print "</a>" if (!$byfile); + print "</th>"; + # do not display the other column-headers, if we do not have any files + # with revision information: + if (scalar(%fileinfo)) { + $infocols++; + print "<th align=left bgcolor=" . (($byrev) ? + $columnHeaderColorSorted : + $columnHeaderColorDefault) . ">"; + print "<a href=\"./" . &toggleQuery ("sortby","rev") . + "#dirlist\">" if (!$byrev); + print "Rev."; + print "</a>" if (!$byrev); + print "</th>"; + $infocols++; + print "<th align=left bgcolor=" . (($bydate) ? + $columnHeaderColorSorted : + $columnHeaderColorDefault) . ">"; + print "<a href=\"./" . &toggleQuery ("sortby","date") . + "#dirlist\">" if (!$bydate); + print "Age"; + print "</a>" if (!$bydate); + print "</th>"; + if ($show_author) { + $infocols++; + print "<th align=left bgcolor=" . (($byauthor) ? + $columnHeaderColorSorted : + $columnHeaderColorDefault) . ">"; + print "<a href=\"./" . &toggleQuery ("sortby","author") . + "#dirlist\">" if (!$byauthor); + print "Author"; + print "</a>" if (!$byauthor); + print "</th>"; + } + $infocols++; + print "<th align=left bgcolor=" . (($bylog) ? + $columnHeaderColorSorted : + $columnHeaderColorDefault) . ">"; + print "<a href=\"./", toggleQuery("sortby","log"), "#dirlist\">" if (!$bylog); + print "Last log entry"; + print "</a>" if (!$bylog); + print "</th>"; + } + print "</tr>\n"; + } + else { + print "<menu>\n"; + } + my $dirrow = 0; + + my $i; + lookingforattic: + for ($i = 0; $i <= $#dir; $i++) { + if ($dir[$i] eq "Attic") { + last lookingforattic; + } + } + if (!$input{'hideattic'} && ($i <= $#dir) && + opendir($dh, $fullname . "/Attic")) { + splice(@dir, $i, 1, + grep((s|^|Attic/|,!m|/\.|), readdir($dh))); + closedir($dh); + } + + my $hideAtticToggleLink = "<a href=\"./" . + &toggleQuery ("hideattic") . + "#dirlist\">[Hide]</a>" if (!$input{'hideattic'}); + + # Sort without the Attic/ pathname. + # place directories first + + my $attic; + my $url; + my $fileurl; + my $filesexists; + my $filesfound; + + foreach (sort { &fileSortCmp } @dir) { + if ($_ eq '.') { + next; + } + # ignore CVS lock and stale NFS files + next if (/^#cvs\.|^,|^\.nfs/); + + # Check whether to show the CVSROOT path + next if ($input{'hidecvsroot'} && ($_ eq 'CVSROOT')); + + # Check whether the module is in the restricted list + next if ($_ && &forbidden_module($_)); + + # Ignore non-readable files + next if ($input{'hidenonreadable'} && !(-r "$fullname/$_")); + + if (s|^Attic/||) { + $attic = " (in the Attic) " . $hideAtticToggleLink; + } + else { + $attic = ""; + } + + if ($_ eq '..' || -d "$fullname/$_") { + next if ($_ eq '..' && $where eq '/'); + my ($rev,$date,$log,$author,$filename) = @{$fileinfo{$_}} + if (defined($fileinfo{$_})); + print "<tr bgcolor=\"" . @tabcolors[$dirrow%2] . "\"><td>" if ($dirtable); + if ($_ eq '..') { + $url = "../" . $query; + if ($nofilelinks) { + print $backicon; + } + else { + print &link($backicon,$url); + } + print " ", &link("Previous Directory",$url); + } + else { + $url = urlencode($_) . '/' . $query; + print "<A NAME=\"$_\">"; + if ($nofilelinks) { + print $diricon; + } + else { + print &link($diricon,$url); + } + print " ", &link($_ . "/", $url), $attic; + if ($_ eq "Attic") { + print " <a href=\"./" . + &toggleQuery ("hideattic") . + "#dirlist\">[Don't hide]</a>"; + } + } + # Show last change in dir + if ($filename) { + print "</td><td> </td><td> " if ($dirtable); + if ($date) { + print " <i>" . readableTime(time() - $date,0) . "</i>"; + } + if ($show_author) { + print "</td><td> " if ($dirtable); + print $author; + } + print "</td><td> " if ($dirtable); + $filename =~ s%^[^/]+/%%; + print "$filename/$rev"; + print "<BR>" if ($dirtable); + if ($log) { + print " <font size=-1>" + . &htmlify(substr($log,0,$shortLogLen)); + if (length $log > 80) { + print "..."; + } + print "</font>"; + } + } + else { + # if there are any files (which require infocols), close the + # row with the appropriate number of columns, so that the + # vertical seperators are visible + if ($dirtable && scalar(%fileinfo)) { + print "</td>"; + my($cols) = $infocols; + while ($cols > 1) { + print "<td> </td>"; + $cols--; + } + } + } + if ($dirtable) { + print "</td></tr>\n"; + } + else { + print "<br>\n"; + } + $dirrow++; + } + elsif (s/,v$//) { + $fileurl = ($attic ? "Attic/" : "") . urlencode($_); + $url = $fileurl . $query; + my $rev = ''; + my $date = ''; + my $log = ''; + my $author = ''; + $filesexists++; + next if (!defined($fileinfo{$_})); + ($rev,$date,$log,$author) = @{$fileinfo{$_}}; + $filesfound++; + print "<tr bgcolor=\"" . @tabcolors[$dirrow%2] . "\"><td>" if ($dirtable); + print "<A NAME=\"$_\">"; + if ($nofilelinks) { + print $fileicon; + } + else { + print &link($fileicon,$url); + } + print " ", &link($_, $url), $attic; + print "</td><td> " if ($dirtable); + download_link($fileurl, + $rev, $rev, + $defaultViewable ? "text/x-cvsweb-markup" : undef); + print "</td><td> " if ($dirtable); + if ($date) { + print " <i>" . readableTime(time() - $date,0) . "</i>"; + } + if ($show_author) { + print "</td><td> " if ($dirtable); + print $author; + } + print "</td><td> " if ($dirtable); + if ($log) { + print " <font size=-1>" . &htmlify(substr($log,0,$shortLogLen)); + if (length $log > 80) { + print "..."; + } + print "</font>"; + } + print "</td>" if ($dirtable); + print (($dirtable) ? "</tr>" : "<br>"); + $dirrow++; + } + print "\n"; + } + if ($dirtable && defined($tableBorderColor)) { + print "</td></tr></table>"; + } + print "". ($dirtable == 1) ? "</table>" : "</menu>" . "\n"; + + if ($filesexists && !$filesfound) { + print "<P><B>NOTE:</B> There are $filesexists files, but none matches the current tag ($input{only_with_tag})\n"; + } + if ($input{only_with_tag} && (!%tags || !$tags{$input{only_with_tag}})) { + %tags = %alltags + } + if (scalar %tags + || $input{only_with_tag} + || $edit_option_form + || defined($input{"options"})) { + print "$bighr"; + } + + if (scalar %tags || $input{only_with_tag}) { + print "<FORM METHOD=\"GET\" ACTION=\"./\">\n"; + foreach my $var (@stickyvars) { + print "<INPUT TYPE=HIDDEN NAME=\"$var\" VALUE=\"$input{$var}\">\n" + if (defined($input{$var}) + && $input{$var} ne $DEFAULTVALUE{$var} + && $input{$var} ne "" + && $var ne "only_with_tag"); + } + print "Show only files with tag:\n"; + print "<SELECT NAME=only_with_tag"; + print " onchange=\"submit()\"" if ($use_java_script); + print ">"; + print "<OPTION VALUE=\"\">All tags / default branch\n"; + foreach my $tag (reverse sort { lc $a cmp lc $b } keys %tags) { + print "<OPTION",defined($input{only_with_tag}) && + $input{only_with_tag} eq $tag ? " SELECTED":"", + ">$tag\n"; + } + print "</SELECT>\n"; + print "<INPUT TYPE=SUBMIT VALUE=\"Go\">\n"; + print "</FORM>\n"; + } + my $formwhere = $scriptwhere; + $formwhere =~ s|Attic/?$|| if ($input{'hideattic'}); + + if ($edit_option_form || defined($input{"options"})) { + print "<FORM METHOD=\"GET\" ACTION=\"${formwhere}\">\n"; + print "<INPUT TYPE=HIDDEN NAME=\"copt\" VALUE=\"1\">\n"; + if ($cvstree ne $cvstreedefault) { + print "<INPUT TYPE=HIDDEN NAME=\"cvsroot\" VALUE=\"$cvstree\">\n"; + } + print "<center><table cellpadding=0 cellspacing=0>"; + print "<tr bgcolor=\"$columnHeaderColorDefault\"><th colspan=2>Preferences</th></tr>"; + print "<tr><td>Sort files by <SELECT name=\"sortby\">"; + print "<OPTION VALUE=\"\">File"; + print "<OPTION",$bydate ? " SELECTED" : ""," VALUE=date>Age"; + print "<OPTION",$byauthor ? " SELECTED" : ""," VALUE=author>Author" + if ($show_author); + print "<OPTION",$byrev ? " SELECTED" : ""," VALUE=rev>Revision"; + print "<OPTION",$bylog ? " SELECTED" : ""," VALUE=log>Log message"; + print "</SELECT></td>"; + print "<td>revisions by: \n"; + print "<SELECT NAME=logsort>\n"; + print "<OPTION VALUE=cvs",$logsort eq "cvs" ? " SELECTED" : "", ">Not sorted"; + print "<OPTION VALUE=date",$logsort eq "date" ? " SELECTED" : "", ">Commit date"; + print "<OPTION VALUE=rev",$logsort eq "rev" ? " SELECTED" : "", ">Revision"; + print "</SELECT></td></tr>"; + print "<tr><td>Diff format: "; + printDiffSelect(); + print "</td>"; + print "<td>Show Attic files: "; + print "<INPUT NAME=hideattic TYPE=CHECKBOX", $input{'hideattic'}?" CHECKED":"", + "></td></tr>\n"; + print "<tr><td align=center colspan=2><input type=submit value=\"Change Options\">"; + print "</td></tr></table></center></FORM>\n"; + } + print &html_footer; + print "</BODY></HTML>\n"; + } + +############################### +# View Files +############################### + elsif (-f $fullname . ',v') { + if (defined($input{'rev'}) || $doCheckout) { + &doCheckout($fullname, $input{'rev'}); + exit; + } + if (defined($input{'annotate'}) && $allow_annotate) { + &doAnnotate($input{'annotate'}); + exit; + } + if (defined($input{'r1'}) && defined($input{'r2'})) { + &doDiff($fullname, $input{'r1'}, $input{'tr1'}, + $input{'r2'}, $input{'tr2'}, $input{'f'}); + exit; + } + print("going to dolog($fullname)\n") if ($verbose); + &doLog($fullname); +############################## +# View Diff +############################## + } + elsif ($fullname =~ s/\.diff$// && -f $fullname . ",v" && + $input{'r1'} && $input{'r2'}) { + + # $where-diff-removal if 'cvs rdiff' is used + # .. but 'cvs rdiff'doesn't support some options + # rcsdiff does (-w and -p), so it is disabled + # $where =~ s/\.diff$//; + + # Allow diffs using the ".diff" extension + # so that browsers that default to the URL + # for a save filename don't save diff's as + # e.g. foo.c + &doDiff($fullname, $input{'r1'}, $input{'tr1'}, + $input{'r2'}, $input{'tr2'}, $input{'f'}); + exit; + } + elsif (($newname = $fullname) =~ s|/([^/]+)$|/Attic/$1| && + -f $newname . ",v") { + # The file has been removed and is in the Attic. + # Send a redirect pointing to the file in the Attic. + (my $newplace = $scriptwhere) =~ s|/([^/]+)$|/Attic/$1|; + &redirect($newplace); + exit; + } + elsif (0 && (my @files = &safeglob($fullname . ",v"))) { + http_header("text/plain"); + print "You matched the following files:\n"; + print join("\n", @files); + # Find the tags from each file + # Display a form offering diffs between said tags + } + else { + my $fh = do {local(*FH);}; + my ($xtra, $module); + # Assume it's a module name with a potential path following it. + $xtra = $& if (($module = $where) =~ s|/.*||); + # Is there an indexed version of modules? + if (open($fh, "$cvsroot/CVSROOT/modules")) { + while (<$fh>) { + if (/^(\S+)\s+(\S+)/o && $module eq $1 + && -d "${cvsroot}/$2" && $module ne $2) { + &redirect($scriptname . '/' . $2 . $xtra); + } + } + } + &fatal("404 Not Found","$where: no such file or directory"); + } +## End MAIN + +sub printDiffSelect { + my ($use_java_script) = @_; + $use_java_script = 0 if (!defined($use_java_script)); + my ($f) = $input{'f'}; + print "<SELECT NAME=\"f\""; + print " onchange=\"submit()\"" if ($use_java_script); + print ">\n"; + print "<OPTION VALUE=h",$f eq "h" ? " SELECTED" : "", ">Colored Diff"; + print "<OPTION VALUE=H",$f eq "H" ? " SELECTED" : "", ">Long Colored Diff"; + print "<OPTION VALUE=u",$f eq "u" ? " SELECTED" : "", ">Unidiff"; + print "<OPTION VALUE=c",$f eq "c" ? " SELECTED" : "", ">Context Diff"; + print "<OPTION VALUE=s",$f eq "s" ? " SELECTED" : "", ">Side by Side"; + print "</SELECT>"; +} + +sub findLastModifiedSubdirs { + my (@dirs) = @_; + my ($dirname, @files); + + foreach $dirname (@dirs) { + next if ($dirname eq "."); + next if ($dirname eq ".."); + my ($dir) = "$fullname/$dirname"; + next if (!-d $dir); + + my ($lastmod) = undef; + my ($lastmodtime) = undef; + my $dh = do {local(*DH);}; + + opendir($dh,$dir) || next; + my (@filenames) = readdir($dh); + closedir($dh); + + foreach my $filename (@filenames) { + $filename = "$dirname/$filename"; + my ($file) = "$fullname/$filename"; + next if ($filename !~ /,v$/ || !-f $file); + $filename =~ s/,v$//; + my $modtime = -M $file; + if (!defined($lastmod) || $modtime < $lastmodtime) { + $lastmod = $filename; + $lastmodtime = $modtime; + } + } + push(@files, $lastmod) if (defined($lastmod)); + } + return @files; +} + +sub htmlify { + my($string, $pr) = @_; + + # Special Characters; RFC 1866 + $string =~ s/&/&/g; + $string =~ s/\"/"/g; + $string =~ s/</</g; + $string =~ s/>/>/g; + + # get URL's as link .. + $string =~ s§(http|ftp)(://[-a-zA-Z0-9%.~:_/]+)([?&]([-a-zA-Z0-9%.~:_]+)=([-a-zA-Z0-9%.~:_])+)*§<A HREF="$1$2$3">$1$2$3</A>§; + # get e-mails as link + $string =~ s§([-a-zA-Z0-9_.]+@([-a-zA-Z0-9]+\.)+[A-Za-z]{2,4})§<A HREF="mailto:$1">$1</A>§; + + # get #PR as link .. + if ($pr && defined($prcgi)) { + $string =~ s!\b((pr[:#]?\s*#?)|((bin|conf|docs|gnu|i386|kern|misc|ports)\/))(\d+)\b!<A HREF="$prcgi?pr=$5">$&</A>!ig; + } + + return $string; +} + +sub spacedHtmlText { + my($string, $pr) = @_; + + # Cut trailing spaces + s/\s+$//; + + # Expand tabs + $string =~ s/\t+/' ' x (length($&) * $tabstop - length($`) % $tabstop)/e + if (defined($tabstop)); + + # replace <tab> and <space> (§ is to protect us from htmlify) + # gzip can make excellent use of this repeating pattern :-) + $string =~ s/§/§%/g; #protect our & substitute + if ($hr_breakable) { + # make every other space 'breakable' + $string =~ s/ / §nbsp; §nbsp; §nbsp; §nbsp;/g; # <tab> + $string =~ s/ / §nbsp;/g; # 2 * <space> + # leave single space as it is + } + else { + $string =~ s/ /§nbsp;§nbsp;§nbsp;§nbsp;§nbsp;§nbsp;§nbsp;§nbsp;/g; + $string =~ s/ /§nbsp;/g; + } + + $string = htmlify($string); + + # unescape + $string =~ s/§([^%])/&$1/g; + $string =~ s/§%/§/g; + + return $string; +} + +sub link { + my($name, $where) = @_; + + return "<A HREF=\"$where\">$name</A>\n"; +} + +sub revcmp { + my($rev1, $rev2) = @_; + my(@r1) = split(/\./, $rev1); + my(@r2) = split(/\./, $rev2); + my($a,$b); + + while (($a = shift(@r1)) && ($b = shift(@r2))) { + if ($a != $b) { + return $a <=> $b; + } + } + if (@r1) { return 1; } + if (@r2) { return -1; } + return 0; +} + +sub fatal { + my($errcode, $errmsg) = @_; + if (defined($ENV{'MOD_PERL'})) { + Apache->request->status((split(/ /, $errcode))[0]); + } + else { + print "Status: $errcode\n"; + } + html_header("Error"); + print "Error: $errmsg\n"; + print &html_footer; + exit(1); +} + +sub redirect { + my($url) = @_; + if (defined($ENV{'MOD_PERL'})) { + Apache->request->status(301); + Apache->request->header_out(Location => $url); + } + else { + print "Status: 301 Moved\n"; + print "Location: $url\n"; + } + html_header("Moved"); + print "This document is located <A HREF=$url>here</A>.\n"; + print &html_footer; + exit(1); +} + +sub safeglob { + my ($filename) = @_; + my ($dirname); + my (@results); + my $dh = do {local(*DH);}; + + ($dirname = $filename) =~ s|/[^/]+$||; + $filename =~ s|.*/||; + + if (opendir($dh, $dirname)) { + my $glob = $filename; + my $t; + # transform filename from glob to regex. Deal with: + # [, {, ?, * as glob chars + # make sure to escape all other regex chars + $glob =~ s/([\.\(\)\|\+])/\\$1/g; + $glob =~ s/\*/.*/g; + $glob =~ s/\?/./g; + $glob =~ s/{([^}]+)}/($t = $1) =~ s-,-|-g; "($t)"/eg; + foreach (readdir($dh)) { + if (/^${glob}$/) { + push(@results, $dirname . "/" .$_); + } + } + } + + @results; +} + +sub getMimeTypeFromSuffix { + my ($fullname) = @_; + my ($mimetype, $suffix); + my $fh = do {local(*FH);}; + + ($suffix = $fullname) =~ s/^.*\.([^.]*)$/$1/; + $mimetype = $MTYPES{$suffix}; + $mimetype = $MTYPES{'*'} if (!$mimetype); + + if (!$mimetype && -f $mime_types) { + # okey, this is something special - search the + # mime.types database + open ($fh, "<$mime_types"); + while (<$fh>) { + if ($_ =~ /^\s*(\S+\/\S+).*\b$suffix\b/) { + $mimetype = $1; + last; + } + } + close ($fh); + } + +# okey, didn't find anything useful .. + if (!($mimetype =~ /\S\/\S/)) { + $mimetype = "text/plain"; + } + return $mimetype; +} + +############################### +# show Annotation +############################### +sub doAnnotate ($$) { + my ($rev) = @_; + my ($pid); + my ($pathname, $filename); + my $reader = do {local(*FH);}; + my $writer = do {local(*FH);}; + + # make sure the revisions a wellformed, for security + # reasons .. + if (!($rev =~ /^[\d\.]+$/)) { + &fatal("404 Not Found", + "Malformed query \"$ENV{'QUERY_STRING'}\""); + } + + ($pathname = $where) =~ s/(Attic\/)?[^\/]*$//; + ($filename = $where) =~ s/^.*\///; + + http_header(); + + navigateHeader ($scriptwhere,$pathname,$filename,$rev, "annotate"); + print "<h3 align=center>Annotation of $pathname$filename, Revision $rev</h3>\n"; + + # this seems to be necessary + $| = 1; $| = 0; # Flush + + # this annotate version is based on the + # cvs annotate-demo Perl script by Cyclic Software + # It was written by Cyclic Software, http://www.cyclic.com/, and is in + # the public domain. + # we could abandon the use of rlog, rcsdiff and co using + # the cvsserver in a similiar way one day (..after rewrite) + $pid = open2($reader, $writer, "cvs server") || fatal ("500 Internal Error", + "Fatal Error - unable to open cvs for annotation"); + + # OK, first send the request to the server. A simplified example is: + # Root /home/kingdon/zwork/cvsroot + # Argument foo/xx + # Directory foo + # /home/kingdon/zwork/cvsroot/foo + # Directory . + # /home/kingdon/zwork/cvsroot + # annotate + # although as you can see there are a few more details. + + print $writer "Root $cvsroot\n"; + print $writer "Valid-responses ok error Valid-requests Checked-in Updated Merged Removed M E\n"; + # Don't worry about sending valid-requests, the server just needs to + # support "annotate" and if it doesn't, there isn't anything to be done. + print $writer "UseUnchanged\n"; + print $writer "Argument -r\n"; + print $writer "Argument $rev\n"; + print $writer "Argument $where\n"; + + # The protocol requires us to fully fake a working directory (at + # least to the point of including the directories down to the one + # containing the file in question). + # So if $where is "dir/sdir/file", then @dirs will be ("dir","sdir","file") + my @dirs = split (/\//, $where); + my $path = ""; + foreach (@dirs) { + if ($path eq "") { + # In our example, $_ is "dir". + $path = $_; + } + else { + print $writer "Directory " . $path . "\n"; + print $writer "$cvsroot/" . $path ."\n"; + # In our example, $_ is "sdir" and $path becomes "dir/sdir" + # And the next time, "file" and "dir/sdir/file" (which then gets + # ignored, because we don't need to send Directory for the file). + $path = $path . "/" . $_; + } + } + # And the last "Directory" before "annotate" is the top level. + print $writer "Directory .\n"; + print $writer "$cvsroot\n"; + + print $writer "annotate\n"; + # OK, we've sent our command to the server. Thing to do is to + # close the writer side and get all the responses. If "cvs server" + # were nicer about buffering, then we could just leave it open, I think. + close ($writer) || die "cannot close: $!"; + + # Ready to get the responses from the server. + # For example: + # E Annotations for foo/xx + # E *************** + # M 1.3 (kingdon 06-Sep-97): hello + # ok + my ($lineNr) = 0; + my ($oldLrev, $oldLusr) = ("", ""); + my ($revprint, $usrprint); + if ($annTable) { + print "<table border=0 cellspacing=0 cellpadding=0>\n"; + } + else { + print "<pre>"; + } + while (<$reader>) { + my @words = split; + # Adding one is for the (single) space which follows $words[0]. + my $rest = substr ($_, length ($words[0]) + 1); + if ($words[0] eq "E") { + next; + } + elsif ($words[0] eq "M") { + $lineNr++; + my $lrev = substr ($_, 2, 13); + my $lusr = substr ($_, 16, 9); + my $line = substr ($_, 36); + # we should parse the date here .. + if ($lrev eq $oldLrev) { + $revprint = " "; + } + else { + $revprint = $lrev; $oldLusr = ""; + } + if ($lusr eq $oldLusr) { + $usrprint = " "; + } + else { + $usrprint = $lusr; + } + $oldLrev = $lrev; + $oldLusr = $lusr; + # is there a less timeconsuming way to strip spaces ? + ($lrev = $lrev) =~ s/\s+//g; + my $isCurrentRev = ("$rev" eq "$lrev"); + + print "<b>" if ($isCurrentRev); + printf ("%8s%s%8s %4d:", $revprint, ($isCurrentRev ? "|" : " "), $usrprint, $lineNr); + print spacedHtmlText($line); + print "</b>" if ($isCurrentRev); + } + elsif ($words[0] eq "ok") { + # We could complain about any text received after this, like the + # CVS command line client. But for simplicity, we don't. + } + elsif ($words[0] eq "error") { + fatal ("500 Internal Error", "Error occured during annotate: <b>$_</b>"); + } + } + if ($annTable) { + print "</table>"; + } + else { + print "</pre>"; + } + close ($reader) || warn "cannot close: $!"; + wait; +} + +############################### +# make Checkout +############################### +sub doCheckout { + my ($fullname, $rev) = @_; + my ($mimetype,$revopt); + my $fh = do {local(*FH);}; + + # make sure the revisions a wellformed, for security + # reasons .. + if (defined($rev) && !($rev =~ /^[\d\.]+$/)) { + &fatal("404 Not Found", + "Malformed query \"$ENV{'QUERY_STRING'}\""); + } + + # get mimetype + if (defined($input{"content-type"}) && ($input{"content-type"} =~ /\S\/\S/)) { + $mimetype = $input{"content-type"} + } + else { + $mimetype = &getMimeTypeFromSuffix($fullname); + } + + if (defined($rev)) { + $revopt = "-r'$rev'"; + readLog($fullname,$rev); + $moddate=$date{$rev}; + } + else { + $revopt = ""; + readLog($fullname); + $moddate=$date{$symrev{HEAD}}; + } + + # this may not be quoted with single quotes + # in windows .. but should in U*nx. there + # is a function which allows for quoting `evil` + # characters somewhere, I know (buried in the Perl-manpage) + ## + ### just for the record: + ### 'cvs co' seems to have a bug regarding single checkout of + ### directories/files having spaces in it; + ### this is an issue that should be resolved on cvs's side + open($fh, "cvs -d'$cvsroot' co -p $revopt '$where' 2>&1 |") || + &fatal("500 Internal Error", "Couldn't co: $!"); +#=================================================================== +#Checking out squid/src/ftp.c +#RCS: /usr/src/CVS/squid/src/ftp.c,v +#VERS: 1.1.1.28.6.2 +#*************** + + # Parse CVS header + my ($revision, $filename, $cvsheader); + while(<$fh>) { + last if (/^\*\*\*\*/); + $revision = $1 if (/^VERS: (.*)$/); + $filename = $1 if (/^Checking out (.*)$/); + $cvsheader .= $_; + } + if ($filename ne $where) { + &fatal("500 Internal Error", + "Unexpected output from cvs co: $cvsheader" + . "<p><b>Check whether the directory $cvsroot/CVSROOT exists " + . "and the script has write-access to the CVSROOT/history " + . "file if it exists." + . "<br>The script needs to place lock files in the " + . "directory the file is in as well.</b>"); + } + $| = 1; + + if ($mimetype eq "text/x-cvsweb-markup") { + &cvswebMarkup($fh,$fullname,$revision); + } + else { + http_header($mimetype); + print <$fh>; + } + close($fh); +} + +sub cvswebMarkup { + my ($filehandle,$fullname,$revision) = @_; + my ($pathname, $filename); + + ($pathname = $where) =~ s/(Attic\/)?[^\/]*$//; + ($filename = $where) =~ s/^.*\///; + my ($fileurl) = urlencode($filename); + + http_header(); + + navigateHeader ($scriptwhere, $pathname, $filename, $revision, "view"); + print "$hr"; + print "<table width=\"100%\"><tr><td bgcolor=\"$markupLogColor\">"; + print "File: ", &clickablePath($where, 1), "</b>"; + print " "; + &download_link(urlencode($fileurl), $revision, "(download)"); + if (!$defaultTextPlain) { + print " "; + &download_link(urlencode($fileurl), $revision, "(as text)", + "text/plain"); + } + print "<BR>\n"; + if ($show_log_in_markup) { + readLog($fullname); #,$revision); + printLog($revision,0); + } + else { + print "Version: <B>$revision</B><BR>\n"; + print "Tag: <B>", $input{only_with_tag}, "</b><br>\n" if + $input{only_with_tag}; + } + print "</td></tr></table>"; + my @content = <$filehandle>; + my $url = download_url($fileurl, $revision, $mimetype); + print "$hr"; + if ($mimetype =~ /^image/) { + print "<IMG SRC=\"$url$barequery\"><BR>"; + } + else { + print "<PRE>"; + foreach (@content) { + print htmlify($_); + } + print "</PRE>"; + } +} + +sub viewable($) { + my ($mimetype) = @_; + + $mimetype =~ m%^text/% || + $mimetype =~ m%^image/% || + 0; +} + +############################### +# Show Colored Diff +############################### +sub doDiff { + my($fullname, $r1, $tr1, $r2, $tr2, $f) = @_; + my $fh = do {local(*FH);}; + my ($rev1, $rev2, $sym1, $sym2, $difftype, $diffname, $f1, $f2); + + if ($r1 =~ /([^:]+)(:(.+))?/) { + $rev1 = $1; + $sym1 = $3; + } + if ($r1 eq 'text') { + $rev1 = $tr1; + $sym1 = ""; + } + if ($r2 =~ /([^:]+)(:(.+))?/) { + $rev2 = $1; + $sym2 = $3; + } + if ($r2 eq 'text') { + $rev2 = $tr2; + $sym2 = ""; + } + # make sure the revisions a wellformed, for security + # reasons .. + if (!($rev1 =~ /^[\d\.]+$/) || !($rev2 =~ /^[\d\.]+$/)) { + &fatal("404 Not Found", + "Malformed query \"$ENV{'QUERY_STRING'}\""); + } +# +# rev1 and rev2 are now both numeric revisions. +# Thus we do a DWIM here and swap them if rev1 is after rev2. +# XXX should we warn about the fact that we do this? + if (&revcmp($rev1,$rev2) > 0) { + my ($tmp1, $tmp2) = ($rev1, $sym1); + ($rev1, $sym1) = ($rev2, $sym2); + ($rev2, $sym2) = ($tmp1, $tmp2); + } + my $human_readable = 0; + if ($f eq 'c') { + $difftype = '-c'; + $diffname = "Context diff"; + } + elsif ($f eq 's') { + $difftype = '--side-by-side --width=164'; + $diffname = "Side by Side"; + } + elsif ($f eq 'H') { + $human_readable = 1; + $difftype = '--unified=15'; + $diffname = "Long Human readable"; + } + elsif ($f eq 'h') { + $difftype = '-u'; + $human_readable = 1; + $diffname = "Human readable"; + } + elsif ($f eq 'u') { + $difftype = '-u'; + $diffname = "Unidiff"; + } + else { + fatal ("400 Bad arguments", "Diff format $f not understood"); + } + + # apply special options + if ($human_readable) { + if ($hr_funout) { + $difftype = $difftype . ' -p'; + } + if ($hr_ignwhite) { + $difftype = $difftype . ' -w'; + } + if ($hr_ignkeysubst) { + $difftype = $difftype . ' -kk'; + } + } +## cvs rdiff doesn't support '-p' and '-w' option .. sad +# open($fh, "cvs -d $cvsroot rdiff $difftype " . +# "-r$rev1 -r$rev2 '$where' 2>&1 |") +# || &fatal("500 Internal Error", "Couldn't cvs rdiff: $!"); +### + open($fh, "rcsdiff $difftype -r$rev1 -r$rev2 '$fullname' 2>&1 |") + || &fatal("500 Internal Error", "Couldn't GNU rcsdiff: $!"); + if ($human_readable) { + http_header(); + &human_readable_diff($fh, $rev2); + exit; + } + else { + http_header("text/plain"); + } +# +#=================================================================== +#RCS file: /home/ncvs/src/sys/netinet/tcp_output.c,v +#retrieving revision 1.16 +#retrieving revision 1.17 +#diff -c -r1.16 -r1.17 +#*** /home/ncvs/src/sys/netinet/tcp_output.c 1995/11/03 22:08:08 1.16 +#--- /home/ncvs/src/sys/netinet/tcp_output.c 1995/12/05 17:46:35 1.17 +# +# Ideas: +# - nuke the stderr output if it's what we expect it to be +# - Add "no differences found" if the diff command supplied no output. +# +#*** src/sys/netinet/tcp_output.c 1995/11/03 22:08:08 1.16 +#--- src/sys/netinet/tcp_output.c 1995/12/05 17:46:35 1.17 RELENG_2_1_0 +# (bogus example, but...) +# + if ($difftype eq '-u') { + $f1 = '---'; + $f2 = '\+\+\+'; + } + else { + $f1 = '\*\*\*'; + $f2 = '---'; + } + while (<$fh>) { + if (m|^$f1 $cvsroot|o) { + s|$cvsroot/||o; + if ($sym1) { + chop; + $_ .= " " . $sym1 . "\n"; + } + } + elsif (m|^$f2 $cvsroot|o) { + s|$cvsroot/||o; + if ($sym2) { + chop; + $_ .= " " . $sym2 . "\n"; + } + } + print $_; + } + close($fh); +} + +############################### +# Show Logs .. +############################### +sub getDirLogs { + my ($cvsroot,$dirname,@otherFiles) = @_; + my ($state,$otherFiles,$tag, $file, $date, $branchpoint, $branch, $log); + my ($rev, $revision, $revwanted, $filename, $head, $author); + + $tag = $input{only_with_tag}; + + my ($DirName) = "$cvsroot/$where"; + my (@files, @filetags); + my $fh = do {local(*FH);}; + + push(@files, &safeglob("$DirName/*,v")); + push(@files, &safeglob("$DirName/Attic/*,v")) if (!$input{'hideattic'}); + foreach $file (@otherFiles) { + push(@files, "$DirName/$file"); + } + + # just execute rlog if there are any files + if ($#files < 0) { + return; + } + + my ($filenames) = join("' '",@files); + if ($tag) { + #can't use -r<tag> as - is allowed in tagnames, but misinterpreated by rlog.. + open($fh, "rlog '$filenames' 2>/dev/null |") + || &fatal("500 Internal Error", "Failed to spawn GNU rlog"); + } + else { + open($fh, "rlog -r '$filenames' 2>/dev/null |") + || &fatal("500 Internal Error", "Failed to spawn GNU rlog"); + } + $state = "start"; + while (<$fh>) { + if ($state eq "start") { + #Next file. Initialize file variables + $rev = undef; + $revwanted = undef; + $branch = undef; + $branchpoint = undef; + $filename = undef; + $log = undef; + $revision = undef; + $branch = undef; + %symrev = (); + @filetags = (); + #jump to head state + $state = "head"; + } + print "$state:$_" if ($verbose); +again: + if ($state eq "head") { + #$rcsfile = $1 if (/^RCS file: (.+)$/); #not used (yet) + $filename = $1 if (/^Working file: (.+)$/); + $head = $1 if (/^head: (.+)$/); + $branch = $1 if (/^branch: (.+)$/); + } + if ($state eq "head" && /^symbolic names/) { + $state = "tags"; + ($branch = $head) =~ s/\.\d+$// if (!defined($branch)); + $branch =~ s/(\.?)(\d+)$/${1}0.$2/; + $symrev{MAIN} = $branch; + $symrev{HEAD} = $branch; + $alltags{MAIN} = 1; + $alltags{HEAD} = 1; + push (@filetags, "MAIN", "HEAD"); + next; + } + if ($state eq "tags" && + /^\s+(.+):\s+([\d\.]+)\s+$/) { + push (@filetags, $1); + $symrev{$1} = $2; + $alltags{$1} = 1; + next; + } + if ($state eq "tags" && /^\S/) { + if (defined($tag) && (defined($symrev{$tag}) || $tag eq "HEAD")) { + $revwanted = $tag eq "HEAD" ? $symrev{"MAIN"} : $symrev{$tag}; + ($branch = $revwanted) =~ s/\b0\.//; + ($branchpoint = $branch) =~ s/\.?\d+$//; + $revwanted = undef if ($revwanted ne $branch); + } + elsif (defined($tag) && $tag ne "HEAD") { + print "Tag not found, skip this file" if ($verbose); + $state = "skip"; + next; + } + foreach my $tagfound (@filetags) { + $tags{$tagfound} = 1; + } + $state = "head"; + goto again; + } + if ($state eq "head" && /^----------------------------$/) { + $state = "log"; + $rev = undef; + $date = undef; + $log = ""; + # Try to reconstruct the relative filename if RCS spits out a full path + $filename =~ s%^$DirName/%%; + next; + } + if ($state eq "log") { + if (/^----------------------------$/ + || /^=============================/) { + # End of a log entry. + my $revbranch; + ($revbranch = $rev) =~ s/\.\d+$//; + print "$filename $rev Wanted: $revwanted " + . "Revbranch: $revbranch Branch: $branch " + . "Branchpoint: $branchpoint\n" if ($verbose); + if (!defined($revwanted) && defined($branch) + && $branch eq $revbranch || !defined($tag)) { + print "File revision $rev found for branch $branch\n" + if ($verbose); + $revwanted = $rev; + } + if (defined($revwanted) ? $rev eq $revwanted : + defined($branchpoint) ? $rev eq $branchpoint : + 0 && ($rev eq $head)) { # Don't think head is needed here.. + print "File info $rev found for $filename\n" if ($verbose); + my @finfo = ($rev,$date,$log,$author,$filename); + my ($name); + ($name = $filename) =~ s%/.*%%; + $fileinfo{$name} = [ @finfo ]; + $state = "done" if ($rev eq $revwanted); + } + $rev = undef; + $date = undef; + $log = ""; + } + elsif (!defined($date) && m|^date:\s+(\d+)/(\d+)/(\d+)\s+(\d+):(\d+):(\d+);|) { + my $yr = $1; + # damn 2-digit year routines :-) + if ($yr > 100) { + $yr -= 1900; + } + $date = &Time::Local::timegm($6,$5,$4,$3,$2 - 1,$yr); + ($author) = /author: ([^;]+)/; + $state = "log"; + $log = ''; + next; + } + elsif (!defined($rev) && m/^revision (.*)$/) { + $rev = $1; + next; + } + else { + $log = $log . $_; + } + } + if (/^===============/) { + $state = "start"; + next; + } + } + if ($. == 0) { + fatal("500 Internal Error", + "Failed to spawn GNU rlog on <em>'$filenames'</em><p>did you set the <b>\$ENV{PATH}</b> in your configuration file correctly ?"); + } + close($fh); +} + +sub readLog { + my($fullname,$revision) = @_; + my ($symnames, $head, $rev, $br, $brp, $branch, $branchrev); + my $fh = do {local(*FH);}; + + if (defined($revision)) { + $revision = "-r$revision"; + } + else { + $revision = ""; + } + + undef %symrev; + undef %revsym; + undef @allrevisions; + undef %date; + undef %author; + undef %state; + undef %difflines; + undef %log; + + print("Going to rlog '$fullname'\n") if ($verbose); + open($fh, "rlog $revision '$fullname'|") + || &fatal("500 Internal Error", "Failed to spawn rlog"); + + while (<$fh>) { + print if ($verbose); + if ($symnames) { + if (/^\s+([^:]+):\s+([\d\.]+)/) { + $symrev{$1} = $2; + } + else { + $symnames = 0; + } + } + elsif (/^head:\s+([\d\.]+)/) { + $head = $1; + } + elsif (/^branch:\s+([\d\.]+)/) { + $curbranch = $1; + } + elsif (/^symbolic names/) { + $symnames = 1; + } + elsif (/^-----/) { + last; + } + } + ($curbranch = $head) =~ s/\.\d+$// if (!defined($curbranch)); + +# each log entry is of the form: +# ---------------------------- +# revision 3.7.1.1 +# date: 1995/11/29 22:15:52; author: fenner; state: Exp; lines: +5 -3 +# log info +# ---------------------------- + logentry: + while (!/^=========/) { + $_ = <$fh>; + last logentry if (!defined($_)); # EOF + print "R:", $_ if ($verbose); + if (/^revision ([\d\.]+)/) { + $rev = $1; + unshift(@allrevisions,$rev); + } + elsif (/^========/ || /^----------------------------$/) { + next logentry; + } + else { + # The rlog output is syntactically ambiguous. We must + # have guessed wrong about where the end of the last log + # message was. + # Since this is likely to happen when people put rlog output + # in their commit messages, don't even bother keeping + # these lines since we don't know what revision they go with + # any more. + next logentry; +# &fatal("500 Internal Error","Error parsing RCS output: $_"); + } + $_ = <$fh>; + print "D:", $_ if ($verbose); + if (m|^date:\s+(\d+)/(\d+)/(\d+)\s+(\d+):(\d+):(\d+);\s+author:\s+(\S+);\s+state:\s+(\S+);\s+(lines:\s+([0-9\s+-]+))?|) { + my $yr = $1; + # damn 2-digit year routines :-) + if ($yr > 100) { + $yr -= 1900; + } + $date{$rev} = &Time::Local::timegm($6,$5,$4,$3,$2 - 1,$yr); + $author{$rev} = $7; + $state{$rev} = $8; + $difflines{$rev} = $10; + } + else { + &fatal("500 Internal Error", "Error parsing RCS output: $_"); + } + line: + while (<$fh>) { + print "L:", $_ if ($verbose); + next line if (/^branches:\s/); + last line if (/^----------------------------$/ || /^=========/); + $log{$rev} .= $_; + } + print "E:", $_ if ($verbose); + } + close($fh); + print "Done reading RCS file\n" if ($verbose); + + @revorder = reverse sort {revcmp($a,$b)} @allrevisions; + print "Done sorting revisions",join(" ",@revorder),"\n" if ($verbose); + +# +# HEAD is an artificial tag which is simply the highest tag number on the main +# branch, unless there is a branch tag in the RCS file in which case it's the +# highest revision on that branch. Find it by looking through @revorder; it +# is the first commit listed on the appropriate branch. +# This is not neccesary the same revision as marked as head in the RCS file. + my $headrev = $curbranch || "1"; + ($symrev{"MAIN"} = $headrev) =~ s/(\.?)(\d+)$/${1}0.$2/; + revision: + foreach $rev (@revorder) { + if ($rev =~ /^(\S*)\.\d+$/ && $headrev eq $1) { + $symrev{"HEAD"} = $rev; + last revision; + } + } + ($symrev{"HEAD"} = $headrev) =~ s/\.\d+$// + if (!defined($symrev{"HEAD"})); + print "Done finding HEAD\n" if ($verbose); +# +# Now that we know all of the revision numbers, we can associate +# absolute revision numbers with all of the symbolic names, and +# pass them to the form so that the same association doesn't have +# to be built then. +# + undef @branchnames; + undef %branchpoint; + undef $sel; + + foreach (reverse sort keys %symrev) { + $rev = $symrev{$_}; + if ($rev =~ /^((.*)\.)?\b0\.(\d+)$/) { + push(@branchnames, $_); + # + # A revision number of A.B.0.D really translates into + # "the highest current revision on branch A.B.D". + # + # If there is no branch A.B.D, then it translates into + # the head A.B . + # + # This reasoning also applies to the main branch A.B, + # with the branch number 0.A, with the exception that + # it has no head to translate to if there is nothing on + # the branch, but I guess this can never happen? + # (the code below gracefully forgets about the branch + # if it should happen) + # + $head = defined($2) ? $2 : ""; + $branch = $3; + $branchrev = $head . ($head ne "" ? "." : "") . $branch; + my $regex; + ($regex = $branchrev) =~ s/\./\\./g; + $rev = $head; + + revision: + foreach my $r (@revorder) { + if ($r =~ /^${regex}\b/) { + $rev = $branchrev; + last revision; + } + } + next if ($rev eq ""); + if ($rev ne $head && $head ne "") { + $branchpoint{$head} .= ", " if ($branchpoint{$head}); + $branchpoint{$head} .= $_; + } + } + $revsym{$rev} .= ", " if ($revsym{$rev}); + $revsym{$rev} .= $_; + $sel .= "<OPTION VALUE=\"${rev}:${_}\">$_\n"; + } + print "Done associating revisions with branches\n" if ($verbose); + + my ($onlyonbranch, $onlybranchpoint); + if ($onlyonbranch = $input{'only_with_tag'}) { + $onlyonbranch = $symrev{$onlyonbranch}; + if ($onlyonbranch =~ s/\b0\.//) { + ($onlybranchpoint = $onlyonbranch) =~ s/\.\d+$//; + } + else { + $onlybranchpoint = $onlyonbranch; + } + if (!defined($onlyonbranch) || $onlybranchpoint eq "") { + fatal("404 Tag not found","Tag $input{'only_with_tag'} not defined"); + } + } + + undef @revisions; + + foreach (@allrevisions) { + ($br = $_) =~ s/\.\d+$//; + ($brp = $br) =~ s/\.\d+$//; + next if ($onlyonbranch && $br ne $onlyonbranch && + $_ ne $onlybranchpoint); + unshift(@revisions,$_); + } + + if ($logsort eq "date") { + # Sort the revisions in commit order an secondary sort on revision + # (secondary sort needed for imported sources, or the first main + # revision gets before the same revision on the 1.1.1 branch) + @revdisplayorder = sort {$date{$b} <=> $date{$a} || -revcmp($a, $b)} @revisions; + } + elsif ($logsort eq "rev") { + # Sort the revisions in revision order, highest first + @revdisplayorder = reverse sort {revcmp($a,$b)} @revisions; + } + else { + # No sorting. Present in the same order as rlog / cvs log + @revdisplayorder = @revisions; + } + +} + +sub printLog($;$) { + my ($link, $br, $brp); + ($_,$link) = @_; + ($br = $_) =~ s/\.\d+$//; + ($brp = $br) =~ s/\.?\d+$//; + my ($isDead, $prev); + + $link = 1 if (!defined($link)); + $isDead = ($state{$_} eq "dead"); + + if ($link && !$isDead) { + my ($filename); + ($filename = $where) =~ s/^.*\///; + my ($fileurl) = urlencode($filename); + print "<a NAME=\"rev$_\"></a>"; + if (defined($revsym{$_})) { + foreach my $sym (split(", ", $revsym{$_})) { + print "<a NAME=\"$sym\"></a>"; + } + } + if (defined($revsym{$br}) && $revsym{$br} && !defined($nameprinted{$br})) { + foreach my $sym (split(", ", $revsym{$br})) { + print "<a NAME=\"$sym\"></a>"; + } + $nameprinted{$br} = 1; + } + print "\n Revision "; + &download_link($fileurl, $_, $_, + $defaultViewable ? "text/x-cvsweb-markup" : undef); + if ($defaultViewable) { + print " / "; + &download_link($fileurl, $_, "(download)", $mimetype); + } + if (not $defaultTextPlain) { + print " / "; + &download_link($fileurl, $_, "(as text)", + "text/plain"); + } + if (!$defaultViewable) { + print " / "; + &download_link($fileurl, $_, "(view)", "text/x-cvsweb-markup"); + } + if ($allow_annotate) { + print " - <a href=\"" . $scriptname . "/" . urlencode($where) . "?annotate=$_$barequery\">"; + print "annotate</a>"; + } + # Plus a select link if enabled, and this version isn't selected + if ($allow_version_select) { + if ((!defined($input{"r1"}) || $input{"r1"} ne $_)) { + print " - <A HREF=\"${scriptwhere}?r1=$_$barequery" . + "\">[select for diffs]</A>\n"; + } + else { + print " - <b>[selected]</b>"; + } + } + } + else { + print "Revision <B>$_</B>"; + } + if (/^1\.1\.1\.\d+$/) { + print " <i>(vendor branch)</i>"; + } + print ", <i>" . scalar gmtime($date{$_}) . " UTC</i> ("; + print readableTime(time() - $date{$_},1) . " ago)"; + print " by "; + print "<i>" . $author{$_} . "</i>\n"; + print "<BR>Branch: <b>",$link?link_tags($revsym{$br}):$revsym{$br},"</b>\n" + if ($revsym{$br}); + print "<BR>CVS Tags: <b>",$link?link_tags($revsym{$_}):$revsym{$_},"</b>" + if ($revsym{$_}); + print "<BR>Branch point for: <b>",$link?link_tags($branchpoint{$_}):$branchpoint{$_},"</b>\n" + if ($branchpoint{$_}); + # Find the previous revision + my @prevrev = split(/\./, $_); + do { + if (--$prevrev[$#prevrev] <= 0) { + # If it was X.Y.Z.1, just make it X.Y + pop(@prevrev); + pop(@prevrev); + } + $prev = join(".", @prevrev); + } until (defined($date{$prev}) || $prev eq ""); + if ($prev ne "") { + if ($difflines{$_}) { + print "<BR>Changes since <b>$prev: $difflines{$_} lines</b>"; + } + } + if ($isDead) { + print "<BR><B><I>FILE REMOVED</I></B>\n"; + } + elsif ($link) { + my %diffrev = (); + $diffrev{$_} = 1; + $diffrev{""} = 1; + print "<BR>Diff"; + # + # Offer diff to previous revision + if ($prev) { + $diffrev{$prev} = 1; + print " to previous <A HREF=\"${scriptwhere}.diff?r1=$prev"; + print "&r2=$_" . $barequery . "\">$prev</A>\n"; + if (!$hr_default) { # offer a human readable version if not default + print "(<A HREF=\"${scriptwhere}.diff?r1=$prev"; + print "&r2=$_" . $barequery . "&f=h\">colored</A>)\n"; + } + } + # + # Plus, if it's on a branch, and it's not a vendor branch, + # offer a diff with the branch point. + if ($revsym{$brp} && !/^1\.1\.1\.\d+$/ && !defined($diffrev{$brp})) { + print " to branchpoint <A HREF=\"${scriptwhere}.diff?r1=$brp"; + print "&r2=$_" . $barequery . "\">$brp</A>\n"; + if (!$hr_default) { # offer a human readable version if not default + print "(<A HREF=\"${scriptwhere}.diff?r1=$brp"; + print "&r2=$_" . $barequery . "&f=h\">colored</A>)\n"; + } + } + # + # Plus, if it's on a branch, and it's not a vendor branch, + # offer to diff with the next revision of the higher branch. + # (e.g. change gets committed and then brought + # over to -stable) + if (/^\d+\.\d+\.\d+/ && !/^1\.1\.1\.\d+$/) { + my ($i,$nextmain); + for ($i = 0; $i < $#revorder && $revorder[$i] ne $_; $i++){} + my (@tmp2) = split(/\./, $_); + for ($nextmain = ""; $i > 0; $i--) { + my ($next) = $revorder[$i-1]; + my (@tmp1) = split(/\./, $next); + if ($#tmp1 < $#tmp2) { + $nextmain = $next; + last; + } + # Only the highest version on a branch should have + # a diff for the "next main". + last if (join(".",@tmp1[0..$#tmp1-1]) + eq join(".",@tmp2[0..$#tmp1-1])); + } + if (!defined($diffrev{$nextmain})) { + $diffrev{$nextmain} = 1; + print " next main <A HREF=\"${scriptwhere}.diff?r1=$nextmain"; + print "&r2=$_" . $barequery . + "\">$nextmain</A>\n"; + if (!$hr_default) { # offer a human readable version if not default + print "(<A HREF=\"${scriptwhere}.diff?r1=$nextmain"; + print "&r2=$_" . $barequery . + "&f=h\">colored</A>)\n"; + } + } + } + # Plus if user has selected only r1, then present a link + # to make a diff to that revision + if (defined($input{"r1"}) && !defined($diffrev{$input{"r1"}})) { + $diffrev{$input{"r1"}} = 1; + print " to selected <A HREF=\"${scriptwhere}.diff?" + . "r1=$input{'r1'}&r2=$_" . $barequery + . "\">$input{'r1'}</A>\n"; + if (!$hr_default) { # offer a human readable version if not default + print "(<A HREF=\"${scriptwhere}.diff?r1=$input{'r1'}"; + print "&r2=$_" . $barequery . + "&f=h\">colored</A>)\n"; + + } + } + } + print "<PRE>\n"; + print &htmlify($log{$_}, 1); + print "</PRE>\n"; +} + +sub doLog { + my($fullname) = @_; + my ($diffrev, $upwhere, $filename, $backurl); + + readLog($fullname); + + html_header("CVS log for $where"); + ($upwhere = $where) =~ s|(Attic/)?[^/]+$||; + ($filename = $where) =~ s|^.*/||; + $backurl = $scriptname . "/" . urlencode($upwhere) . $query; + print &link($backicon, "$backurl#$filename"), + " <b>Up to ", &clickablePath($upwhere, 1), "</b><p>\n"; + print "<A HREF=\"#diff\">Request diff between arbitrary revisions</A>\n"; + print "$hr\n"; + if ($curbranch) { + print "Default branch: "; + print ($revsym{$curbranch} || $curbranch); + } + else { + print "No default branch"; + } + print "<BR>\n"; + if ($input{only_with_tag}) { + print "Current tag: $input{only_with_tag}<BR>\n"; + } + + undef %nameprinted; + + for (my $i = 0; $i <= $#revdisplayorder; $i++) { + print "$bighr"; + printLog($revdisplayorder[$i]); + } + + print "<A NAME=diff>\n"; + print "$hr"; + print "This form allows you to request diff's between any two\n"; + print "revisions of a file. You may select a symbolic revision\n"; + print "name using the selection box or you may type in a numeric\n"; + print "name using the type-in text box.\n"; + print "</A><P>\n"; + print "<FORM METHOD=\"GET\" ACTION=\"${scriptwhere}.diff\" NAME=\"diff_select\">\n"; + foreach (@stickyvars) { + print "<INPUT TYPE=HIDDEN NAME=\"$_\" VALUE=\"$input{$_}\">\n" + if (defined($input{$_}) + && ($input{$_} ne $DEFAULTVALUE{$_} && $input{$_} ne "")); + } + print "Diffs between \n"; + print "<SELECT NAME=\"r1\">\n"; + print "<OPTION VALUE=\"text\" SELECTED>Use Text Field\n"; + print $sel; + print "</SELECT>\n"; + $diffrev = $revdisplayorder[$#revdisplayorder]; + $diffrev = $input{"r1"} if (defined($input{"r1"})); + print "<INPUT TYPE=\"TEXT\" SIZE=\"$inputTextSize\" NAME=\"tr1\" VALUE=\"$diffrev\" onChange='document.diff_select.r1.selectedIndex=0'>\n"; + print " and \n"; + print "<SELECT NAME=\"r2\">\n"; + print "<OPTION VALUE=\"text\" SELECTED>Use Text Field\n"; + print $sel; + print "</SELECT>\n"; + $diffrev = $revdisplayorder[0]; + $diffrev = $input{"r2"} if (defined($input{"r2"})); + print "<INPUT TYPE=\"TEXT\" SIZE=\"$inputTextSize\" NAME=\"tr2\" VALUE=\"$diffrev\" onChange='docuement.diff_select.r2.selectedIndex=0'>\n"; + print "<BR>Type of Diff should be a "; + printDiffSelect(); + print "<INPUT TYPE=SUBMIT VALUE=\" Get Diffs \">\n"; + print "</FORM>\n"; + print "$hr\n"; + if (@branchnames) { + print "<A name=branch>\n"; + print "<FORM METHOD=\"GET\" ACTION=\"$scriptwhere\">\n"; + foreach (@stickyvars) { + next if ($_ eq "only_with_tag"); + next if ($_ eq "logsort"); + print "<INPUT TYPE=HIDDEN NAME=\"$_\" VALUE=\"$input{$_}\">\n" + if (defined($input{$_}) && $input{$_} ne $DEFAULTVALUE{$_} + && $input{$_} ne ""); + } + print "View only Branch: \n"; + print "<SELECT NAME=\"only_with_tag\""; + print " onchange=\"submit()\"" if ($use_java_script); + print ">\n"; + print "<OPTION VALUE=\"\""; + print " SELECTED" if (defined($input{"only_with_tag"}) && + $input{"only_with_tag"} eq ""); + print ">Show all branches\n"; + foreach (reverse sort @branchnames) { + print "<OPTION"; + print " SELECTED" if (defined($input{"only_with_tag"}) + && $input{"only_with_tag"} eq $_); + print ">${_}\n"; + } + print "</SELECT>\n"; + print "<INPUT TYPE=SUBMIT VALUE=\" View Branch \">\n"; + print "</FORM>\n"; + print "</A>\n"; + } + print "<A name=logsort>\n"; + print "<FORM METHOD=\"GET\" ACTION=\"$scriptwhere\">\n"; + foreach (@stickyvars) { + next if ($_ eq "only_with_tag"); + next if ($_ eq "logsort"); + print "<INPUT TYPE=HIDDEN NAME=\"$_\" VALUE=\"$input{$_}\">\n" + if (defined($input{$_}) && $input{$_} ne $DEFAULTVALUE{$_} + && $input{$_} ne ""); + } + print "Sort log by: \n"; + print "<SELECT NAME=\"logsort\""; + print " onchange=\"submit()\"" if ($use_java_script); + print ">\n"; + print "<OPTION VALUE=cvs",$logsort eq "cvs" ? " SELECTED" : "", ">Not sorted"; + print "<OPTION VALUE=date",$logsort eq "date" ? " SELECTED" : "", ">Commit date"; + print "<OPTION VALUE=rev",$logsort eq "rev" ? " SELECTED" : "", ">Revision"; + print "</SELECT>\n"; + print "<INPUT TYPE=SUBMIT VALUE=\" Sort \">\n"; + print "</FORM>\n"; + print "</A>"; + print &html_footer; + print "</BODY></HTML>\n"; +} + +sub flush_diff_rows ($$$$) +{ + my $j; + my ($leftColRef,$rightColRef,$leftRow,$rightRow) = @_; + if ($state eq "PreChangeRemove") { # we just got remove-lines before + for ($j = 0 ; $j < $leftRow; $j++) { + print "<tr><td bgcolor=\"$diffcolorRemove\">@$leftColRef[$j]</td>"; + print "<td bgcolor=\"$diffcolorEmpty\"> </td></tr>\n"; + } + } + elsif ($state eq "PreChange") { # state eq "PreChange" + # we got removes with subsequent adds + for ($j = 0; $j < $leftRow || $j < $rightRow ; $j++) { # dump out both cols + print "<tr>"; + if ($j < $leftRow) { + print "<td bgcolor=\"$diffcolorChange\">@$leftColRef[$j]</td>"; + } + else { + print "<td bgcolor=\"$diffcolorDarkChange\"> </td>"; + } + if ($j < $rightRow) { + print "<td bgcolor=\"$diffcolorChange\">@$rightColRef[$j]</td>"; + } + else { + print "<td bgcolor=\"$diffcolorDarkChange\"> </td>"; + } + print "</tr>\n"; + } + } +} + +## +# Function to generate Human readable diff-files +# human_readable_diff(String revision_to_return_to); +## +sub human_readable_diff($){ + my ($i,$difftxt, $where_nd, $filename, $pathname, $scriptwhere_nd); + my ($fh, $rev) = @_; + my ($date1, $date2, $r1d, $r2d, $r1r, $r2r, $rev1, $rev2, $sym1, $sym2); + my (@rightCol, @leftCol); + + ($where_nd = $where) =~ s/.diff$//; + ($filename = $where_nd) =~ s/^.*\///; + ($pathname = $where_nd) =~ s/(Attic\/)?[^\/]*$//; + ($scriptwhere_nd = $scriptwhere) =~ s/.diff$//; + + navigateHeader ($scriptwhere_nd, $pathname, $filename, $rev, "diff"); + + # Read header to pick up read revision and date, if possible + while (<$fh>) { + ($r1d,$r1r) = /\t(.*)\t(.*)$/ if (/^--- /); + ($r2d,$r2r) = /\t(.*)\t(.*)$/ if (/^\+\+\+ /); + last if (/^\+\+\+ /); + } + if (defined($r1r) && $r1r =~ /^(\d+\.)+\d+$/) { + $rev1 = $r1r; + $date1 = $r1d; + } + if (defined($r2r) && $r2r =~ /^(\d+\.)+\d+$/) { + $rev2 = $r2r; + $date2 = $r2d; + } + + print "<h3 align=center>Diff for /$where_nd between version $rev1 and $rev2</h3>\n"; + + print "<table border=0 cellspacing=0 cellpadding=0 width=100%>\n"; + print "<tr bgcolor=#ffffff>\n"; + print "<th width=\"50%\" valign=TOP>"; + print "version $rev1"; + print ", $date1" if (defined($date1)); + print "<br>Tag: $sym1\n" if ($sym1); + print "</th>\n"; + print "<th width=\"50%\" valign=TOP>"; + print "version $rev2"; + print ", $date2" if (defined($date2)); + print "<br>Tag: $sym2\n" if ($sym1); + print "</th>\n"; + + my $fs = "<font face=\"$difffontface\" size=\"$difffontsize\">"; + my $fe = "</font>"; + + my $leftRow = 0; + my $rightRow = 0; + my ($oldline, $newline, $funname, $diffcode, $rest); + + # Process diff text + # The diffrows are could make excellent use of + # cascading style sheets because we've to set the + # font and color for each row. anyone ...? + #### + while (<$fh>) { + $difftxt = $_; + + if ($difftxt =~ /^@@/) { + ($oldline,$newline,$funname) = $difftxt =~ /@@ \-([0-9]+).*\+([0-9]+).*@@(.*)/; + print "<tr bgcolor=\"$diffcolorHeading\"><td width=\"50%\">"; + print "<table width=100% border=1 cellpadding=5><tr><td><b>Line $oldline</b>"; + print " <font size=-1>$funname</font></td></tr></table>"; + print "</td><td width=\"50%\">"; + print "<table width=100% border=1 cellpadding=5><tr><td><b>Line $newline</b>"; + print " <font size=-1>$funname</font></td></tr></table>"; + print "</td><tr>\n"; + $state = "dump"; + $leftRow = 0; + $rightRow = 0; + } + else { + ($diffcode,$rest) = $difftxt =~ /^([-+ ])(.*)/; + $_ = spacedHtmlText ($rest); + + # Add fontface, size + $_ = "$fs $_$fe"; + + ######### + # little state machine to parse unified-diff output (Hen, zeller@think.de) + # in order to get some nice 'ediff'-mode output + # states: + # "dump" - just dump the value + # "PreChangeRemove" - we began with '-' .. so this could be the start of a 'change' area or just remove + # "PreChange" - okey, we got several '-' lines and moved to '+' lines -> this is a change block + ########## + + if ($diffcode eq '+') { + if ($state eq "dump") { # 'change' never begins with '+': just dump out value + print "<tr><td bgcolor=\"$diffcolorEmpty\"> </td><td bgcolor=\"$diffcolorAdd\">$_</td></tr>\n"; + } + else { # we got minus before + $state = "PreChange"; + $rightCol[$rightRow++] = $_; + } + } + elsif ($diffcode eq '-') { + $state = "PreChangeRemove"; + $leftCol[$leftRow++] = $_; + } + else { # empty diffcode + flush_diff_rows \@leftCol, \@rightCol, $leftRow, $rightRow; + print "<tr><td>$_</td><td>$_</td></tr>\n"; + $state = "dump"; + $leftRow = 0; + $rightRow = 0; + } + } + } + flush_diff_rows \@leftCol, \@rightCol, $leftRow, $rightRow; + + # state is empty if we didn't have any change + if (!$state) { + print "<tr><td colspan=2> </td></tr>"; + print "<tr bgcolor=\"$diffcolorEmpty\" >"; + print "<td colspan=2 align=center><b>- No viewable Change -</b></td></tr>"; + } + print "</table>"; + close($fh); + + print "<br>$widehr\n"; + + print "<table border=0>"; + + print "<tr><td>"; + # print legend + print "<table border=1><tr><td>"; + print "Legend:<br><table border=0 cellspacing=0 cellpadding=1>\n"; + print "<tr><td align=center bgcolor=\"$diffcolorRemove\">Removed from v.$rev1</td><td bgcolor=\"$diffcolorEmpty\"> </td></tr>"; + print "<tr bgcolor=\"$diffcolorChange\"><td align=center colspan=2>changed lines</td></tr>"; + print "<tr><td bgcolor=\"$diffcolorEmpty\"> </td><td align=center bgcolor=\"$diffcolorAdd\">Added in v.$rev2</td></tr>"; + print "</table></td></tr></table>\n"; + print "</body>\n</html>\n"; + + print "<td>"; + # Print format selector + print "<FORM METHOD=\"GET\" ACTION=\"${scriptwhere}\">\n"; + foreach my $var (keys %input) { + next if ($var eq "f"); + next if (defined($DEFAULTVALUE{$var}) + && $DEFAULTVALUE{$var} eq $input{$var}); + print "<INPUT TYPE=HIDDEN NAME=\"",urlencode($var),"\" VALUE=\"", + urlencode($input{$var}),"\">\n"; + } + printDiffSelect($use_java_script); + print "<INPUT TYPE=SUBMIT VALUE=\"Show\">\n"; + print "</FORM>\n"; + print "</td>"; + + print "</tr></table>"; +} + +sub navigateHeader ($$$$$) { + my ($swhere,$path,$filename,$rev,$title) = @_; + $swhere = "" if ($swhere eq $scriptwhere); + $swhere = urlencode($filename) if ($swhere eq ""); + print "<HTML>\n<HEAD>\n"; + print '<!-- hennerik CVSweb $Revision$ -->'; + print "\n<TITLE>$path$filename - $title - $rev</TITLE>"; + print $stylesheet if ($stylesheet); + print "</HEAD>\n"; + print "<BODY BGCOLOR=\"$backcolor\">\n"; + print "<table width=\"100%\" border=0 cellspacing=0 cellpadding=1 bgcolor=\"$navigationHeaderColor\">"; + print "<tr valign=bottom><td>"; + print "<a href=\"$swhere$query#rev$rev\">$backicon"; + print "</a> <b>Return to ", &link("$filename","$swhere$query#rev$rev")," CVS log"; + print "</b> $fileicon</td>"; + + print "<td align=right>$diricon <b>Up to ", &clickablePath($path, 1), "</b></td>"; + print "</tr></table>"; +} + +sub plural_write ($$) +{ + my ($num,$text) = @_; + if ($num != 1) { + $text = $text . "s"; + } + if ($num > 0) { + return $num . " " . $text; + } + else { + return ""; + } +} + +## +# print readable timestamp in terms of +# '..time ago' +# H. Zeller <zeller@think.de> +## +sub readableTime ($$) +{ + my ($i, $break, $retval); + my ($secs,$long) = @_; + + # this function works correct for time >= 2 seconds + if ($secs < 2) { + return "very little time"; + } + + my %desc = (1 , 'second', + 60, 'minute', + 3600, 'hour', + 86400, 'day', + 604800, 'week', + 2628000, 'month', + 31536000, 'year'); + my @breaks = sort {$a <=> $b} keys %desc; + $i = 0; + while ($i <= $#breaks && $secs >= 2 * $breaks[$i]) { + $i++; + } + $i--; + $break = $breaks[$i]; + $retval = plural_write(int ($secs / $break), $desc{"$break"}); + + if ($long == 1 && $i > 0) { + my $rest = $secs % $break; + $i--; + $break = $breaks[$i]; + my $resttime = plural_write(int ($rest / $break), + $desc{"$break"}); + if ($resttime) { + $retval = $retval . ", " . $resttime; + } + } + + return $retval; +} + +## +# clickablePath(String pathname, boolean last_item_clickable) +# +# returns a html-ified path whereas each directory is a link for +# faster navigation. last_item_clickable controls whether the +# basename (last directory/file) is a link as well +## +sub clickablePath($$) { + my ($pathname,$clickLast) = @_; + my $retval = ''; + + if ($pathname eq '/') { + # this should never happen - chooseCVSRoot() is + # intended to do this + $retval = "[$cvstree]"; + } + else { + $retval = $retval . " <a href=\"${scriptname}/${query}#dirlist\">[$cvstree]</a>"; + my $wherepath = ''; + my ($lastslash) = $pathname =~ m|/$|; + foreach (split(/\//, $pathname)) { + $retval = $retval . " / "; + $wherepath = $wherepath . '/' . $_; + my ($last) = "$wherepath/" eq "/$pathname" + || "$wherepath" eq "/$pathname"; + if ($clickLast || !$last) { + $retval = $retval . "<a href=\"${scriptname}" + . urlencode($wherepath) + . (!$last || $lastslash ? '/' : '') + . ${query} + . (!$last || $lastslash ? "#dirlist" : "") + . "\">$_</a>"; + } + else { # do not make a link to the current dir + $retval = $retval . $_; + } + } + } + return $retval; +} + +sub chooseCVSRoot() { + my @foo; + foreach (sort keys %CVSROOT) { + if (-d $CVSROOT{$_}) { + push(@foo, $_); + } + } + if (@foo > 1) { + my ($k); + print "<form method=\"GET\" action=\"${scriptwhere}\">\n"; + foreach $k (keys %input) { + print "<input type=hidden NAME=$k VALUE=$input{$k}>\n" + if ($input{$k}) && ($k ne "cvsroot"); + } + # Form-Elements look wierd in Netscape if the background + # isn't gray and the form elements are not placed + # within a table ... + print "<table><tr>"; + print "<td>CVS Root:</td>"; + print "<td>\n<select name=\"cvsroot\""; + print " onchange=\"submit()\"" if ($use_java_script); + print ">\n"; + foreach $k (@foo) { + print "<option value=\"$k\""; + print " selected" if ("$k" eq "$cvstree"); + print ">" . ($CVSROOTdescr{"$k"} ? $CVSROOTdescr{"$k"} : + $k). "</option>\n"; + } + print "</select>\n</td>"; + print "<td><input type=submit value=\"Go\"></td>"; + print "</tr></table></form>"; + } + else { + # no choice .. + print "CVS Root: <b>[$cvstree]</b>"; + } +} + +sub chooseMirror() { + my ($mirror,$moremirrors); + $moremirrors = 0; + # This code comes from the original BSD-cvsweb + # and may not be useful for your site; If you don't + # set %MIRRORS this won't show up, anyway + # + # Should perhaps exlude the current site somehow.. + if (keys %MIRRORS) { + print "\nThis cvsweb is mirrored in:\n"; + foreach $mirror (keys %MIRRORS) { + print ", " if ($moremirrors); + print qq(<a href="$MIRRORS{$mirror}">$mirror</A>\n); + $moremirrors = 1; + } + print "<p>\n"; + } +} + +sub fileSortCmp { + my ($comp) = 0; + my ($c,$d,$af,$bf); + + ($af = $a) =~ s/,v$//; + ($bf = $b) =~ s/,v$//; + my ($rev1,$date1,$log1,$author1,$filename1) = @{$fileinfo{$af}} + if (defined($fileinfo{$af})); + my ($rev2,$date2,$log2,$author2,$filename2) = @{$fileinfo{$bf}} + if (defined($fileinfo{$bf})); + + if (defined($filename1) && defined($filename2) && $af eq $filename1 && $bf eq $filename2) { + # Two files + $comp = -revcmp($rev1, $rev2) if ($byrev && $rev1 && $rev2); + $comp = ($date2 <=> $date1) if ($bydate && $date1 && $date2); + $comp = ($log1 cmp $log2) if ($bylog && $log1 && $log2); + $comp = ($author1 cmp $author2) if ($byauthor && $author1 && $author2); + } + if ($comp == 0) { + # Directories first, then sorted on name if no other sort critera + # available. + my $ad = ((-d "$fullname/$a")?"D":"F"); + my $bd = ((-d "$fullname/$b")?"D":"F"); + ($c=$a) =~ s|.*/||; + ($d=$b) =~ s|.*/||; + $comp = ("$ad$c" cmp "$bd$d"); + } + return $comp; +} + +# make A url for downloading +sub download_url { + my ($url,$revision,$mimetype) = @_; + + $revision =~ s/\b0\.//; + + if (defined($checkout_magic) + && (!defined($mimetype) || $mimetype ne "text/x-cvsweb-markup")) { + my ($path); + ($path = $where) =~ s|/[^/]*$|/|; + $url = "$scriptname/$checkoutMagic/${path}$url"; + } + $url .= "?rev=$revision"; + $url .= "&content-type=$mimetype" if (defined($mimetype)); + + return $url; +} + +# Presents a link to download the +# selected revision +sub download_link { + my ($url,$revision,$textlink,$mimetype) = @_; + my ($fullurl) = download_url($url,$revision,$mimetype); + my ($paren) = $textlink =~ /^\(/; + $textlink =~ s/^\(// if ($paren); + $textlink =~ s/\)$// if ($paren); + print "(" if ($paren); + print "<A HREF=\"$fullurl"; + print $barequery; + print "\""; + if ($open_extern_window && (!defined($mimetype) || $mimetype ne "text/x-cvsweb-markup")) { + print " target=\"cvs_checkout\""; + # we should have + # 'if (document.cvswin==null) document.cvswin=window.open(...' + # in order to allow the user to resize the window; otherwise + # the user may resize the window, but on next checkout - zap - + # its original (configured s. cvsweb.conf) size is back again + # .. annoying (if $extern_window_(width|height) is defined) + # but this if (..) solution is far from perfect + # what we need to do as well is + # 1) save cvswin in an invisible frame that always exists + # (document.cvswin will be void on next load) + # 2) on close of the cvs_checkout - window set the cvswin + # variable to 'null' again - so that it will be + # reopenend with the configured size + # anyone a JavaScript programmer ? + # .. so here without if (..): + # currently, the best way is to comment out the size parameters + # ($extern_window...) in cvsweb.conf. + if ($use_java_script) { + print " onClick=\"window.open('$fullurl','cvs_checkout',"; + print "'resizeable,scrollbars"; + print ",status,toolbar" if (defined($mimetype) + && $mimetype eq "text/html"); + print ",width=$extern_window_width" if (defined($extern_window_width)); + print ",height=$extern_window_height" if (defined($extern_window_height)); + print"');\""; + } + } + print "><b>$textlink</b></A>"; + print ")" if ($paren); +} + +# Returns a Query string with the +# specified parameter toggled +sub toggleQuery($$) { + my ($toggle,$value) = @_; + my ($newquery,$var); + my (%vars); + %vars = %input; + if (defined($value)) { + $vars{$toggle} = $value; + } + else { + $vars{$toggle} = $vars{$toggle} ? 0 : 1; + } + # Build a new query of non-default paramenters + $newquery = ""; + foreach $var (@stickyvars) { + my ($value) = defined($vars{$var}) ? $vars{$var} : ""; + my ($default) = defined($DEFAULTVALUE{$var}) ? $DEFAULTVALUE{$var} : ""; + if ($value ne $default) { + $newquery .= "&" if ($newquery ne ""); + $newquery .= urlencode($var) . "=" . urlencode($value); + } + } + if ($newquery) { + return '?' . $newquery; + } + return ""; +} + +sub urlencode { + my ($in) = @_; + my ($out); + ($out = $in) =~ s/([\000-+{-\377])/sprintf("%%%02x", ord($1))/ge; + return $out; +} + +sub http_header { + my $content_type = shift || "text/html"; + my $is_mod_perl = defined($ENV{'MOD_PERL'}); + if (defined($moddate)) { + if ($is_mod_perl) { + Apache->request->header_out(Last_modified => scalar gmtime($moddate) . " GMT"); + } + else { + print "Last-Modified: " . scalar gmtime($moddate) . " GMT\n"; + } + } + if ($is_mod_perl) { + Apache->request->content_type($content_type); + } + else { + print "Content-type: $content_type\n"; + } + if ($allow_compress && $maycompress) { + my $fh = do {local(*FH);}; + if (defined($GZIPBIN) && open($fh, "|$GZIPBIN -1 -c")) { + if ($is_mod_perl) { + Apache->request->content_encoding("x-gzip"); + Apache->request->header_out(Vary => "Accept-Encoding"); + Apache->request->send_http_header; + } + else { + print "Content-encoding: x-gzip\n"; + print "Vary: Accept-Encoding\n"; #RFC 2068, 14.43 + print "\n"; # Close headers + } + $| = 1; $| = 0; # Flush header output + select ($fh); +# print "<!-- gzipped -->" if ($content_type eq "text/html"); + } + else { + if ($is_mod_perl) { + Apache->request->send_http_header; + } + else { + print "\n"; # Close headers + } + print "<font size=-1>Unable to find gzip binary in the \$PATH to compress output</font><br>"; + } + } + else { + if ($is_mod_perl) { + Apache->request->send_http_header; + } + else { + print "\n"; # Close headers + } + } +} + +sub html_header($) { + my ($title) = @_; + http_header(); + print <<EOH; +<!doctype html public "-//W3C//DTD HTML 4.0 Transitional//EN" + "http://www.w3.org/TR/REC-html40/loose.dtd"> +<html> +<title>$title</title> +<!-- hennerik CVSweb \$Revision$ \--> +EOH +print $stylesheet if ($stylesheet); +print <<EOH; +</head> +$body_tag +$logo <h1 align="center">$title</h1> +EOH +} + +sub html_footer { + return "$hr$footer\n"; +} + +sub link_tags +{ + my ($tags) = @_; + my ($ret) = ""; + my ($fileurl,$filename); + + ($filename = $where) =~ s/^.*\///; + $fileurl = urlencode($filename); + + foreach my $sym (split(", ", $tags)) { + $ret .= ",\n" if ($ret ne ""); + $ret .= "<A HREF=\"$fileurl" + . toggleQuery('only_with_tag',$sym) . "\">$sym</A>"; + } + return $ret."\n"; +} + +# +# See if a module is listed in the config file's @HideModule list. +# +sub forbidden_module { + my($module) = @_; + + return ($HideModules =~ /§$module§/); +} diff --git a/html/cvsweb.conf b/html/cvsweb.conf new file mode 100644 index 00000000..73de6277 --- /dev/null +++ b/html/cvsweb.conf @@ -0,0 +1,350 @@ +# -*-perl-*- +# Configuration of cvsweb.cgi, the +# CGI interface to CVS Repositories. +# +# (c) 1998-1999 H. Zeller <zeller@think.de> +# 1999 H. Nordström <hno@hem.passagen.se> +# based on work by Bill Fenner <fenner@freebsd.org> +# $Id$ +# +### + +############## +# CVS Root +############## +# CVSweb can handle several CVS-Repositories +# at once. Enter a short symbolic names and the +# full path of these repositories here. +# NOTE that the symbolic names may not contain +# whitespaces. +# Note, that cvsweb.cgi currently needs to have physical access +# to the CVS repository so :pserver:someone@xyz.com:/data/cvsroot +# won't work! + +# 'symbolic_name' 'path_to_the_actual_repository' +%CVSROOT = ( + 'ProofGeneral' => '/home/proofgen/cvsmirror/src' + ); + +# This tree is enabled by default when +# you enter the page +$cvstreedefault = 'ProofGeneral'; + +############## +# Defaults for UserSettings +############## +%DEFAULTVALUE = ( + # sortby: File sort order + # file Sort by filename + # rev Sort by revision number + # date Sort by commit date + # author Sort by author + # log Sort by log message + + "sortby" => "file", + + # hideattic: Hide or show files in Attic + # 1 Hide files in Attic + # 0 Show files in Attic + + "hideattic" => "1", + + # logsort: Sort order for CVS logs + # date Sort revisions by date + # rev Sort revision by revision number + # cvs Don't sort them. Same order as CVS/RCS shows them. + + "logsort" => "date", + + # f: Default diff format + # h Human readable + # u Unified diff + # c Context diff + # s Side by side + "f" => "h", + + # hidecvsroot: Don't show the CVSROOT directory + # 1 Hide CVSROOT directory + # 0 Show CVSROOT directory + "hidecvsroot" => "0", + + # hidenonreadable: Don't show entries which cannot be read + # 1 Hide non-readable entries + # 0 Show non-readble entries + "hidenonreadable" => "1", +); + +############## +# some layout stuff +############## + +$stylesheet = '<link rel="stylesheet" + href="http://www.proofgeneral.org/proofgen.css" + type="text/css">'; + + +# color settings in the body-tag +# $body_tag = '<body text="#000000" bgcolor="#ffffff">'; +$body_tag = '<body>'; + +# Wanna have a logo on the page ? +$logo = '<a href="http://www.proofgeneral.org"> + <img src="http://www.proofgeneral.org/images/ProofGeneral.jpg" alt="Proof General" align=top + width=65 height=76 border=0 ></a>'; + + +# The title of the Page on startup +$defaulttitle = "Proof General CVS Repository"; + +# This message is shown on the footer +$footer = '<small> +<i>Contact <a href="http://www.proofgeneral.org/~da/">David Aspinall</a> +for information about Proof General development. +<br> +This page was generated by +<a href="http://linux.fh-heilbronn.de/~zeller/cgi/cvsweb.cgi">CVSweb</a>. +</i> +</small>'; + +# Default page background color for the diffs +# and annotations +$backcolor = "#222222"; + +# color of navigation Header for +# diffs and annotations +$navigationHeaderColor = '#AAAA66'; + +$long_intro = <<EOT; +<p> +This is a WWW interface to the Proof General CVS Repository. +You can browse the file hierarchy by picking directories +(which have slashes after them, <i>e.g.</i>, <b>src/</b>). +If you pick a file, you will see the revision history +for that file. +Selecting a revision number will download that revision of +the file. There is a link at each revision to display +diffs between that revision and the previous one, and +a form at the bottom of the page that allows you to +display diffs between arbitrary revisions. +</p> +EOT + +$short_instruction = <<EOT; +<p> +Click on a directory to enter that directory. Click on a file to display +its revision history and to get a chance to display diffs between revisions. +</p> +EOT + +# used icons; if icon-url is empty, the text representation is used; if +# you do not want to have an ugly tooltip for the icon, remove the +# text-representation. +# The width and height of the icon allow the browser to correcly display +# the table while still loading the icons. +# These default icons are coming with apache. +# If these icons are too large, check out the miniicons in the +# icons/ directory; they have a width/height of 16/16 +# format: TEXT ICON-URL width height +%ICONS = ( + back => [ ("[BACK]", "/icons/back.gif", 20, 22) ], + dir => [ ("[DIR]", "/icons/dir.gif", 20, 22) ], + file => [ ("[TXT]", "/icons/text.gif", 20, 22) ], + ); + +# the length to which the last logentry should +# be truncated when shown in the directory view +$shortLogLen = 80; + +# Show author of last change +$show_author = 1; + +############## +# table view for directories +############## + +# Show directory as table +# this is much more readable but has one +# drawback: the whole table has to be loaded +# before common browsers display it which may +# be annoying if you have a slow link - and a +# large directory .. +$dirtable = 1; + +# show different colors for even/odd rows +@tabcolors = ('#664433', '#663344'); +$tablepadding = 2; + +# Color of Header +$columnHeaderColorDefault = '#333333'; +$columnHeaderColorSorted = '#880088'; + +# +# If you want to have colored borders +# around each row, uncomment this +$tableBorderColor = '#999999'; + +# +# Modules in the repository that should not be displayed, either by default +# nor by explicit path specification. +# +@HideModules = ( + ); + +############## +# Human Readable Diff +############## + +# (c) 1998 H. Zeller <zeller@think.de> +# +# Generates two columns of color encoded +# diff; much like xdiff or emacs-ediff mode. +# +# The diff-stuff is a piece of code I once made for +# cvs2html which is under GPL, +# see http://www.sslug.dk/cvs2html +# (c) 1997/98 Peter Toft <pto@sslug.imm.dtu.dk> +# +# some parameters to screw: +## + +# make lines breakable so that the columns do not +# exceed the width of the browser +$hr_breakable = 1; + +# give out function names in human readable diffs +# this just makes sense if we have C-files, otherwise +# diff's heuristic doesn't work well .. +# ( '-p' option to diff) +$hr_funout = 0; + +# ignore whitespaces for human readable diffs +# (indendation and stuff ..) +# ( '-w' option to diff) +$hr_ignwhite = 1; + +# ignore diffs which are caused by +# keyword-substitution like $Id - Stuff +# ( '-kk' option to rcsdiff) +$hr_ignkeysubst = 1; + +# Colors and font to show the diff type of code changes +$diffcolorHeading = '#99cccc'; # color of 'Line'-head of each diffed file +$diffcolorEmpty = '#cccccc'; # color of 'empty' lines +$diffcolorRemove = '#ff9999'; # Removed line(s) (left) ( - ) +$diffcolorChange = '#99ff99'; # Changed line(s) ( both ) +$diffcolorAdd = '#ccccff'; # Added line(s) ( - ) (right) +$diffcolorDarkChange = '#99cc99'; # lines, which are empty in change +$difffontface = "Helvetica,Arial"; +$difffontsize = "-1"; + +# the width of the textinput of the +# request-diff-form +$inputTextSize = 12; + +############## +# Mime Types +############## + +# mapping to mimetypes to help +# cvsweb to guess the correct mime-type on +# checkout; you can use the mime.types from +# apache here: +$mime_types = '/etc/httpd/conf/mime.types'; + +# quick mime-type lookup; maps file-suffices to +# mime-types for displaying checkouts in the browser. +# Further MimeTypes will be found in the +# file $mime_types (apache style mime.types - file) +# - add common mappings here for faster lookup +%MTYPES = ( + "html" => "text/html", + "shtml" => "text/html", + "gif" => "image/gif", + "jpeg" => "image/jpeg", + "jpg" => "image/jpeg", + "*" => "text/plain", + ); + +############## +# Misc +############## +# allow annotation of files +# this requires rw-access to the +# CVSROOT/history - file and rw-access +# to the subdirectory to place the lock +# so you maybe don't want it +$allow_annotate = 1; + +# allow pretty-printed version of files +$allow_markup = 1; + +# allow compression with gzip +# of output if the Browser accepts +# it (HTTP_ACCEPT_ENCODING=gzip) +# [make sure to have gzip in the path] +$allow_compress = 1; + +# Make use of javascript functions. +# This way you can select one of your CVSroot +# without pressing 'Go' (.. if you do have more +# than one CVSROOT defined) +$use_java_script = 1; + +# open Download-Links in another window +$open_extern_window = 1; + +# The size of this extern window; this size option +# needs use_java_script to be defined +# just comment them if you don't want to have a fixed +# size +#$extern_window_width = 600; +#$extern_window_height = 440; + +# Edit Options +# Enable form to edit your options (hideattic,sortbydate) +# this isn't necessary if you've $dirtable defined 'cause +# this allows editing of all your options more intuitive +$edit_option_form = (not $dirtable); + +# remember to set the path to your +# rcsutils: rlog, rcsdiff (gzip if you use compression) +#$ENV{'PATH'} = '/usr/local/bin'; + +# If you have files which automatically refers to other files +# (such as HTML) then this allows you to browse the checked +# out files as if outside CVS. +$checkout_magic = 1; + +# Show last changelog message for sub directories +# The current implementation makes many assumptions and may show the +# incorrect file at some times. The main assumption is that the last +# modified file has the newest filedate. But some CVS operations +# touches the file without even when a new version is't checked in, +# and TAG based browsing essientially puts this out of order, unless +# the last checkin was on the same tag as you are viewing. +# Enable this if you like the feature, but don't rely on correct results. +$show_subdir_lastmod = 0; + +# Background color of logentry in markup +$markupLogColor = "#ffffff"; + +# Show CVS log when viewing file contents +$show_log_in_markup = 1; + +# Tabstop used to expand tabs in colored diffs. If undefined then +# tabs are always expanded to 8 spaces. +$tabstop = 8; + +# Horizontal rules (added by da@dcs.ed.ac.uk) + +# defaults: +# $hr="<hr noshade>"; +# $bighr="<hr noshade size=1>"; +# $widehr="<hr noshade width=100%>"; + +$hr = '<img border=0 src="http://www.proofgeneral.org/images/silverrule.gif" height=4 width=100%>'; +$bighr = '<img border=0 src="http://www.proofgeneral.org/images/silverrule.gif" height=8 width=100%>'; +$widehr = '<img border=0 src="http://www.proofgeneral.org/images/silverrule.gif" height=4 width=100%>'; + + +#EOF diff --git a/html/devel b/html/devel new file mode 100644 index 00000000..a58717d8 --- /dev/null +++ b/html/devel @@ -0,0 +1,5 @@ +<?php include('index.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?>
\ No newline at end of file diff --git a/html/devel.html b/html/devel.html new file mode 100644 index 00000000..e748874b --- /dev/null +++ b/html/devel.html @@ -0,0 +1,127 @@ +<h2>Development Information</h2> +<p> +Proof General follows an open development method. +<br> +We encourage code contributions, suggestions, and bug reports, from all +users. +</p> + +<ul> +<li> +Download the latest <a href="develdownload.html">development release: +<!-- WARNING! Line below automatically edited by makefile. --> + <b>ProofGeneral-3.5pre030121</b></a> +<!-- end WARNING --> +<br> +or <a href="ProofGeneral">browse</a> the development distribution. + <br> +Check the +<!-- WARNING! Line below automatically edited by makefile. --> +<?php fileshow("ProofGeneral-3.5pre030121/CHANGES","CHANGES"); ?> file +<!-- End Warning. --> +for a summary of changes since the last stable version. +</li> +</ul> + +<ul> +<li> +Browse a mirror of the <a href="http://www.proofgeneral.org/cgi-bin/cvsweb.cgi">Proof General CVS repository</a>. <br> +<i>Note:</i> this mirror is updated nightly, so it may be +slightly out of date.<br> +If you want to be an "official" developer and +access the real CVS repository, +<a href="feedback.html">ask here</a>. +</li> +</ul> + +<ul> +<li> +Read about ideas for the <a href="kit">Proof General Kit</a> +here. +</li> +</ul> + +<ul> +<li> +Take a look at some Proof General <a href="projects.html">project proposals</a>. +</li> +</ul> + + +<ul> +<li> +Read the +developer's +<?php fileshow("ProofGeneral-3.5pre030121/README.devel","README file"); ?>, +with development hints and tips. +</li> +</ul> + + +<ul> +<li> +Read the brief list of planned +<?php fileshow("ProofGeneral-3.5pre030121/TODO","things to do "); ?> +for Proof General. +</ul> +<ul> +<li> +<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.5pre030121/todo","generic base"); ?>, + <br> + and for each prover: + <?php fileshow("ProofGeneral-3.5pre030121/lego/todo","lego to do"); ?>, + <?php fileshow("ProofGeneral-3.5pre030121/coq/todo","coq to do"); ?>, + <?php fileshow("ProofGeneral-3.5pre030121/isa/todo","isa to do"); ?>, + <?php fileshow("ProofGeneral-3.5pre030121/isar/todo","isar to do"); ?>, + <?php fileshow("ProofGeneral-3.5pre030121/hol98/todo","hol to do"); ?>. +<!-- end WARNING --> +</li> +</ul> + +<ul> +<li> +See Proof General's <a href="components">standalone components</a> +which can be used in other programs. +</li> +</ul> + + + +<!-- <ul> --> +<!-- <li> --> +<!-- Browse source files from the current pre-release: --> +<!-- <?php fileshow("ProofGeneral-3.5pre030121/generic/proof.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.5pre030121/generic/proof-site.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.5pre030121/generic/proof-config.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.5pre030121/generic/proof-script.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.5pre030121/generic/proof-shell.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.5pre030121/generic/proof-toolbar.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.5pre030121/generic/proof-syntax.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.5pre030121/generic/proof-splash.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.5pre030121/generic/proof-easy-config.el") ?>. --> +<!-- </ul> --> + + +<ul> +<li> +<?php hlink("feedback","Send us a message ","Feedback form")?> +about any development issues. +</li> +</ul> + +<h2><a name="develmail">Developers Mailing List</a></h2> + +<p> +We have a mailing list for developers, at +<a href="mailto:devel@proofgeneral.org">devel@proofgeneral.org</a>. +<br> +Posting is restricted to list members. +To subscribe (or unsubscribe), +visit +<a href="http://lists.informatics.ed.ac.uk/mailman/listinfo/proofgeneral-devel">this +web page</a>. +</p> + diff --git a/html/develdownload b/html/develdownload new file mode 100644 index 00000000..4c9b3b01 --- /dev/null +++ b/html/develdownload @@ -0,0 +1,5 @@ +<?php include('develdownload.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?> diff --git a/html/develdownload.html b/html/develdownload.html new file mode 100644 index 00000000..4c9b3b01 --- /dev/null +++ b/html/develdownload.html @@ -0,0 +1,5 @@ +<?php include('develdownload.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?> diff --git a/html/develdownload.php b/html/develdownload.php new file mode 100644 index 00000000..f3383733 --- /dev/null +++ b/html/develdownload.php @@ -0,0 +1,140 @@ +<!-- -*- html -*- --> +<?php + require('functions.php3'); + small_header("Proof General Development Release"); + ?> + + +<p> +<a href="#prerel">Below</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> (further below), which +includes files not needed for the running program. +</p> +<p> +Pre-releases of Proof General may be buggy as we add new features and +experiment with them. Nonetheless, we welcome bug reports. But +please make sure you are using the latest pre-release before +reporting problems. +</p> +<p> +Please <a href="register">register</a> if you haven't done so already. +</p> + + +<!-- WARNING! Line below automatically edited by makefile. --> +<h2><a name="doc">Manual for ProofGeneral-3.5pre030121</a></h2> +<!-- End Warning. --> +<p> +The manual included with the pre-release may be +updated from that of the +<a href="doc">last stable release</a>. +</p> +<p> +Here is the pre-release documentation: the user manual in +<?php htmlshow("ProofGeneral-latest/doc/ProofGeneral_toc.html","HTML","Proof General manual") ?>, +<?php download_link("ProofGeneral-latest/doc/ProofGeneral.ps.gz", "ps") ?> +or +<?php download_link("ProofGeneral-latest/doc/ProofGeneral.pdf", "pdf") ?>, +and the adapting manual, in +<?php htmlshow("ProofGeneral-latest/doc/PG-adapting_toc.html","HTML","Adapting Proof General manual") ?>, +<?php download_link("ProofGeneral-latest/doc/PG-adapting.ps.gz", "ps") ?> +or +<?php download_link("ProofGeneral-latest/doc/PG-adapting.pdf", "pdf") ?>. +</p> + + +<!-- WARNING! Line below automatically edited by makefile. --> +<h2><a name="prerel">Pre-release: ProofGeneral-3.5pre030121</a></h2> + +<p> +Check the +<!-- WARNING! Line below automatically edited by makefile. --> +<?php fileshow("ProofGeneral-3.5pre030121/CHANGES","CHANGES"); ?> file +<!-- End Warning. --> +for a summary of changes since the last stable +version, and notes about work-in-progress. </p> +<table width="80%" cellspacing=8> +<tr><td width=150>gzip'ed tar file</td> +<!-- WARNING! Lines below automatically edited by makefile. --> +<td><?php download_link("ProofGeneral-3.5pre030121.tar.gz") ?></td> +</tr> +<tr> +<td>zip file</td> +<td><?php download_link("ProofGeneral-3.5pre030121.zip") ?></td> +</tr> +<tr> +<td>RPM package </td> +<td><?php download_link("ProofGeneral-3.5pre030121-1.noarch.rpm") ?></td> +</tr> +<tr> +<td>individual files</td> +<td><a href="ProofGeneral">http access to files in development release</a> +</tr> +</table> +<!-- End Warning. --> +<p> +<b>Emacs versions:</b> +This version has been tested with XEmacs version 21.4.8 and with GNU +Emacs 21.2.1. XEmacs support is better tested. Older releases of Emacs +<i>may</i> work, but we recommend the use of these or newer versions +because backwards compatibility across different Emacs versions is too +difficult to support. If you cannot upgrade your Emacs, consider +using an <a href="oldrel.php">older release</a> of Proof General. +</p> +<p> +<b>Prover versions:</b> +This version has been tested with Coq 7.3, Isabelle2002, Lego 1.3.1, +and PhoX 0.8. +</p> +<p> +For install instructions, see +the <a href="download#install">stable version download</a>. +</p> + +<p> +</p> +<p> +</p> + + +<!-- WARNING! Line below automatically edited by makefile. --> +<h2><a name="devel">CVS snapshot of ProofGeneral-3.5pre030121 for developers</a></h2> +<!-- End Warning. --> + +<ul> + <li> gzip'ed tar file: +<!-- WARNING! Line below automatically edited by makefile. --> + <?php download_link("ProofGeneral-3.5pre030121-devel.tar.gz") ?> +<!-- End Warning. --> + </li> +</ul> +<p> +This tarball contains all of our development files, including some +files not present in the released version of Proof General. +Specifically: +</p> +<ul> + <li> the low-level developer's todo files + (see <a href="devel#lowleveltodo">the developers page</a>) + and the detailed + <!-- WARNING! Line below automatically edited by makefile. --> + <?php fileshow("ProofGeneral-3.5pre030121/ChangeLog","ChangeLog"); ?>, + <!-- End Warning. --> + </li> + <li> developer's Makefile used to generate documentation files + and the release itself,</li> + <li> test files, image source files, the web pages, and sometimes </li> + <li> working instantiations of Proof General for new provers. </li> +</ul> +<p> +Most people don't need this. Note that there are no pre-built +documentation files in the developer's release (developers can +run Make, by definition). +</p> + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/doc b/html/doc new file mode 100644 index 00000000..a58717d8 --- /dev/null +++ b/html/doc @@ -0,0 +1,5 @@ +<?php include('index.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?>
\ No newline at end of file diff --git a/html/doc.html b/html/doc.html new file mode 100644 index 00000000..7be1ba5f --- /dev/null +++ b/html/doc.html @@ -0,0 +1,132 @@ +<h2>Manuals for Proof General</h2> + +<p> +There is a short FAQ and two manuals for Proof General: +</p> +<ul> +<li> the <a href="FAQ">FAQ</a> (please send any contributions) +<li> the <a href="userman">Proof General user manual</a> +</li> +<li> the <a href="adaptingman">Adapting Proof General manual</a> +</li> +</ul> +<p> +The second manual gives instructions on how to adapt Proof General to new +proof systems, it's not needed for ordinary use. +For printing you can download: +<ul> +<li> +<?php download_link("ProofGeneral/doc/ProofGeneral.ps.gz", "User manual [ps]") ?> and +<?php download_link("ProofGeneral/doc/PG-adapting.ps.gz", "Adapting manual [ps]") ?>, or +</li> +<li> +<?php download_link("ProofGeneral/doc/ProofGeneral.pdf", "User manual [pdf]") ?>, +<?php download_link("ProofGeneral/doc/PG-adapting.pdf", "Adapting manual [pdf]") ?> +</li> +</ul> +<p> +The PostScript files are recommended over the PDF. +Both manuals (HTML and Info formats) are included in the +<a href="download">download</a>. When running Proof General the manual +is available from the "Proof General" menu. It should also appear in +the system Info pages. +If you're considering developing Proof General, please check +that you are using the documentation for the most recent +development version of Proof General, available with the +<a href="develdownload">development download</a>. +</p> + +<p> +You can discuss Proof General with other users and receive +announcements by joining our <a href="mailinglist.html">mailing +list</a>. +</p> + + +<h2>Manuals for Emacs</h2> + +<p>If you're new to Emacs, it's recommended to try the Emacs tutorial, +available inside Emacs by pressing <b>C-h t</b> (which means +<tt>ctrl</tt>-with-<tt>h</tt> followed by <tt>t</tt>). There are many +other <b>C-h</b> commands, and the Help menu inside Emacs gives access +to more help facilities. +</p> +<p>For on-line reading, these links might be helpful: +<ul> +<li>The <a href="http://www.gnu.org/manual/emacs/">Emacs user manual</a></li> +<li>The <a href="http://www.gnu.org/manual/emacs-lisp-intro"> + Emacs lisp introduction</a> and + <a href="http://www.gnu.org/manual/elisp">Emacs lisp reference</a>.</li> +</li> +</ul> +(You don't need to look at anything about lisp unless you're interested +in developing Proof General). +</p> +<p>The corresponding manuals for XEmacs are +available <a href="http://www.xemacs.org/Documentation/index.html">here</a> (xemacs.org). +</p> + + + + + + +<h2>References</h2> + +<p> Ideas for the future of Proof General are given here: +</p> +<ul> +<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>. + <b><i>Protocols for Interactive e-Proof</i></b>. + Draft version, see + <a href="http://homepages.inf.ed.ac.uk/da/drafts/#eproof">here</a>. +</li> +<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>. + <b><i>Proof General Kit (white paper)</i></b>. + Draft version, see + <a href="http://homepages.inf.ed.ac.uk/da/drafts/#white">here</a>. +</li> +</ul> +<p> A technology overview of Proof General is given here: +</p> +<ul> +<li> <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>. + <a href="papers/pgoutline.ps.gz">Proof General: A Generic Tool for + Proof Development</a>. + <i>Tools and Algorithms for the Construction and + Analysis of Systems, Proc TACAS 2000</i>, LNCS 1785. + <br> + Here are some <a href="papers/pgtalk.pdf">slides</a> + used for this talk and some other presentations of Proof General. +</li> +</ul> +<p> Proof General supports Script Management as documented in: +</p> +<ul> + <li> <a + href="http://www.inria.fr/croap/personnel/Yves.Bertot/me.html">Yves + Bertot</a> and <a + href="http://www.inria.fr/croap/personnel/Laurent.Thery/me.html">Laurent + Théry</a>. <a + href="ftp://babar.inria.fr/pub/croap/bertot/jsymcomp.ps">A + generic approach to building user interfaces for theorem + provers</a>. + <i>Journal of Symbolic Computation</i>, 25(7), pp. 161-194, February 1998. + </li> + </ul> + <p> + It has support for Proof by Pointing, as documented in: + </p> + <ul> + <li> <a + href="http://www.inria.fr/croap/personnel/Yves.Bertot/me.html">Yves + Bertot</a>, Thomas Kleymann-Schreiber and Dilip Sequeira. + <I>Implementing Proof by Pointing without a Structure Editor</I>. + LFCS Technical Report <a + href="http://www.lfcs.informatics.ed.ac.uk/reports/97/ECS-LFCS-97-368/index.html">ECS-LFCS-97-368</a>. + Also published as Rapport de recherche de l'INRIA + <a href="http://www.inria.fr/Unites/SOPHIA-eng.html"> Sophia + Antipolis</a> <a + href="http://www.inria.fr/RRRT/RR-3286.html">RR-3286</a> + </li> +</ul> diff --git a/html/download b/html/download new file mode 100644 index 00000000..a58717d8 --- /dev/null +++ b/html/download @@ -0,0 +1,5 @@ +<?php include('index.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?>
\ No newline at end of file diff --git a/html/download.html b/html/download.html new file mode 100644 index 00000000..e34b5cbc --- /dev/null +++ b/html/download.html @@ -0,0 +1,248 @@ +<h2>Please register</h2> +<p> +Before downloading Proof General, <i>please</i> +<a href="register">register</a>. +It's free, it only takes a moment. +If you have already registered you do not need to do so again. +<!-- Let's remove this rant for now. +The statistics collected from registrations are used to help +make a case for support for Proof General, and nothing else. +It is likely that development of Proof General will <i>finish soon</i> +unless we find new resources. As a courtesy, we do not make +registration compulsory and I can tell from the server logs that the +majority of people downloading do not register. But if you don't +register now, please consider returning to register later if you find +Proof General interesting or useful. If you don't want to fill the +form, please <a href="mailto:proofgen@dcs.ed.ac.uk">send an email</a> +directly or even a paper letter to the <a +href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a>. And if you +can offer to help resource the development of Proof General +in some way, please +<a href="feedback">contact us</a>. --> +</p> + +<p> +You can join the +Proof General +<a href="mailinglist">mailing list</a> +for announcements of new versions. +Developers and early-adopters may like to download +a <a href="develdownload.html">development release</a> +of Proof General. +If you use an old version of a proof assistant and/or an +old Emacs version, you may need to download one of the +<a href="oldrel.php">previous releases</a>. +</p> +<h2><a name="stable"> + Proof General Version 3.4, released 29th August 2002. + </a> +</h2> +<p> +Proof General is distributed under the terms of +the +<?php fileshow("ProofGeneral/COPYING","GNU General Public License"); ?>. +<br> +See <a href="#prereq">below</a> for software pre-requisites for running Proof General. +</p> + +<p> +Proof General is available as an archive and an RPM package. +</p> +<table width="80%" cellspacing=8> +<tr> +<td width=150>gzip'ed tar file</td> +<td><?php download_link("ProofGeneral-3.4.tar.gz") ?></td> +</tr> +<tr> +<td>zip file</td> +<td><?php download_link("ProofGeneral-3.4.zip") ?></td> +</tr> +<tr> +<td>RPM package </td> +<td><?php download_link("ProofGeneral-3.4-1.noarch.rpm") ?> +<br>NB: to build yourself use the tar file with <tt>rpm -ta</tt>.</td> +</tr> +<tr> +<td>individual files</td> +<td><a href="ProofGeneral-3.4">browse individual files</a> +</tr> +</table> +<p> +The archives and RPM include almost everything: the generic +code, specific code for the supported provers, installation +instructions and documentation in Info and HTML formats. +Documentation is available in other formats +here <a href="doc">here</a>. +<!-- If you want to format the documentation yourself, + you may like to download the + <?php download_link("ProofGeneralPortrait.eps.gz", + "front page image") ?>. --> +</p> + +<p> This version of Proof General has been tested with XEmacs 21.4 and +GNU Emacs 21.2. It should work with <i>some</i> earlier versions of +XEmacs, but we recommend using these Emacs versions for the most +reliable results. Support on GNU Emacs is catching up, but XEmacs is +still the better tested and more fully-featured environment. +See below for links. +</p> +<p> +See the <?php +fileshow("ProofGeneral-3.4/etc/announce","announcement"); ?> for more +details, or check the <?php +fileshow("ProofGeneral-3.4/CHANGES","CHANGES"); ?> file for a summary +of changes since version 3.3. +</p> + +<p> +Check the latest <?php fileshow("ProofGeneral/BUGS","BUGS"); ?> file +(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," ); ?>) +before reporting problems. If you find a problem not already mentioned, +please +<?php hlink("feedback.html","send us a note","Feedback form")?>. +</p> + +<br> + +<h2><a name="prereq"> + What you need to run Proof General + </a> +</h2> +<p> +To run Proof General, you <strong>must</strong> have: +</p> +<ul> +<li> +Version 21.1 or 21.4 +of <a href="http://www.xemacs.org">XEmacs</a> +(this UK +<a href="http://sunsite.doc.ic.ac.uk/Mirrors/ftp.xemacs.org/pub/xemacs/"> +ftp mirror</a> may help). +<br> +<b>or</b> version 21.2 of +<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>. +<br> +Both Emacsen are available for a variety of platforms, including +Unix variants, Windows 95/98/NT/2k, and Mac OS. +</li> +<li> +A proof assistant, for example: +<?php fileshow("ProofGeneral/coq/README","Coq"); ?>; +<?php fileshow("ProofGeneral/isa/README","Isabelle"); ?> + or <?php fileshow("ProofGeneral/isa/README","Isabelle/Isar"); ?>; +<?php fileshow("ProofGeneral/lego/README","LEGO"); ?>; +<?php fileshow("ProofGeneral/phox/README","PhoX"); ?>. +<br> +(click on links for version details; see <a href=".">front page</a> for +other assistants). +<br> +Or write your own support for a new assistant! +</li> +</ul> +</p> + +<p> +There is also an <strong>optional</strong> component for using +Proof General: +<ul> +<li> +For displaying logical and mathematical symbols, the excellent +<a href="http://x-symbol.sourceforge.net/">X-Symbol</a> +package. +<br>It's very easy to install. See <a href="#xsyminstall">here</a> +for installation notes. +<br>Versions of X-Symbol supported: +<b>version 3.4 (stable)</b>, and <i>partially</i>, <b>version 4.4 (beta)</b>. +<br> +The stable version of X-Symbol only works with XEmacs on systems running X. +The beta version also works with Emacs 21.4 (not yet available), and +has limited support for XEmacs on Windows. +</li> +<!-- <li> --> +<!-- For GNU Emacs, a version of <tt>func-menu.el</tt> to get --> +<!-- <a href="features#funcmenu">function menus</a>. --> +<!-- <br>Unfortunately I can't find a version of this that --> +<!-- works with current GNU 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> +Compatibility across the multitude of Emacs versions is quite troublesome. +<br> +XEmacs has been better tested with Proof General than GNU Emacs. +<br> +Earlier versions of either variant <i>may</i> work with Proof General +but are not officially supported because we cannot test backward +compatibility widely. Please <a href="feedback">send us fixes</a> +rather than bug reports if you discover problems. +Later versions of both Emacs variants <i>should</i> work with +Proof General: if you discover problems, please check +to see if they have been solved in a more recent +<a href="develdownload">development release</a> before +reporting. + + +<h3><a name="install">Easy installation of Proof General</a></h3> +<p> +To use Proof General, simply unpack the sources with +</p> + <blockquote> + <tt>tar xpzf ProofGeneral-3.4.tar.gz</tt> + </blockquote> +<p> +(use <tt>gunzip</tt> first in place of <tt>z</tt> if you don't have +GNU tar),<br> and then add this one line to your .emacs file: +</p> + <blockquote> + <tt> (load-file "<var>directory</var>/generic/proof-site.el")</tt> + </blockquote> +<p> +Where <var>directory</var> is the directory in which you unpacked +the sources. +<br> +If you use the RPM package, <var>directory</var> is +<tt>/usr/share/emacs/ProofGeneral</tt> +</p> +<p> +If you're using Windows, then download the zip file. +<br> +Use a zip file utility to unpack it somewhere, for example +<tt>c:\ProofGeneral</tt> +</p> +<p> +Further customization is possible via the Customize menus in +Emacs. +<br> +See the <?php fileshow("ProofGeneral-3.4/INSTALL","INSTALL")?> +file in the distribution for more details. +</p> + +<h3><a name="xsyminstall">Easy installation of X-Symbol</a></h3> + +<p> +X-Symbol is easy to install in XEmacs and configures itself automatically. +</p> +<p> +Simply download the binary package file, and do something +like this to install in your home directory: +</p> +<blockquote><tt> + mkdir -p ~/.xemacs/xemacs-packages<br> + cd ~/.xemacs/xemacs-packages<br> + tar xpzf ../x-symbol-pkg.tar.gz<br> +</tt></blockquote> +<p> +For GNU Emacs, you must remove the <tt>.elc</tt> files supplied, and +add some code to your <tt>.emacs</tt>. See +<a href="http://x-symbol.sourceforge.net/news.html">this page</a> +for details. +More installation options are given +in the <a href="http://x-symbol.sourceforge.net/man/x-symbol_2.html">the X-Symbol manual</a>. diff --git a/html/eeproof b/html/eeproof new file mode 100644 index 00000000..2df23c96 --- /dev/null +++ b/html/eeproof @@ -0,0 +1,5 @@ +<?php include('eeproof.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?> diff --git a/html/eeproof.php b/html/eeproof.php new file mode 100644 index 00000000..3388bee5 --- /dev/null +++ b/html/eeproof.php @@ -0,0 +1,32 @@ +<?php + require('functions.php3'); + small_header("Engineering Electronic Proof"); + ?> + +<p> +The <b>Engineering Electronic Proof</b> project is +a proposed continuation of the Proof General project, +using Proof General as a vehicle to study and build +new mechanisms for managing the development of +electronic proof. +</p> + +<h3>Details</h3> +<p> +More details will be posted here in due course. +</p> +<p> +In the meantime, there is some related +information on the <a href="kit">Proof General Kit</a> +page about the next stages of development for Proof General. +</p> +<p> +<h3>Collaborations</h3> +Collaborations on this work are being sought. If you are interested in collaborating, or have ideas or suggestions to contribute, please send a note to +<a href="mailto:eeproof@proofgeneral.org"><tt>eeproof@proofgeneral.org</tt></a> +</p> + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/elispmarkup.php3 b/html/elispmarkup.php3 new file mode 100644 index 00000000..e2b47367 --- /dev/null +++ b/html/elispmarkup.php3 @@ -0,0 +1,137 @@ +<?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:)[^ \n\t]+)","<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 whole body, or "; + print "<a href=\"$thispage?file=" . urlencode($filename); + print "\">here</a> to hide whole body."; + 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); + // Pagebreaks + // ??? + // Anchors for URLs + $line = ereg_replace("((http://|mailto:)[-a-zA-Z0-9\.~/_@]+)","<a href=\"\\1\">\\1</a>",$line); + // Font-lock equivalents... + // 1. comments. Strings roughly done: ignore if quote appears after ; +// seems buggy: <div> breaks line in pre formatting. Only do for whole-lines. +// $line = ereg_replace("^([^;]*)(;+[^\"^\n]+)\n$", + $line = ereg_replace("^(;+[^\"^\n]+)\n$", + "<font color=\"#8080E0\">\\1</font>\n", + $line); + // 2. keywords + $line = ereg_replace("^\(def(macro|un|var|custom|const|group|face)", + "(<font color=\"#F0B0B0\">def\\1</font>", + $line); + // FIXME: add hrefs for keywords, looking up in TAGS file. + // FIXME: add line numbers + // FIXME: parse strings + print $line; + } +} diff --git a/html/eproofe.php b/html/eproofe.php new file mode 100644 index 00000000..e965a78a --- /dev/null +++ b/html/eproofe.php @@ -0,0 +1,30 @@ +<?php + require('functions.php3'); + small_header("Engineering Electronic Proof"); + ?> + +<p> +Proof General, and particularly, the <a href="kit">Proof General +Kit</a> is proposed as a vehicle for research into <i>engineering +electronic proof<i>. We want to investigate the +maintenance, combination, and reuse of formal proof developments. +</p> + +<h3>Planning</h3> +<p> +This project has not yet been started, and there are no public +documents available yet. +</p> +<p> +Some hints of our plans appear in the papers describing +the <a href="kit">Proof General Kit</a>. +</p> + +<p> +Any <a href="mailto:da@dcs.ed.ac.uk">comments</a> are welcomed. +</p> + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/favicon.ico b/html/favicon.ico Binary files differnew file mode 100644 index 00000000..d3faa231 --- /dev/null +++ b/html/favicon.ico diff --git a/html/features b/html/features new file mode 100644 index 00000000..a58717d8 --- /dev/null +++ b/html/features @@ -0,0 +1,5 @@ +<?php include('index.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?>
\ No newline at end of file diff --git a/html/features.html b/html/features.html new file mode 100644 index 00000000..ebe5bb27 --- /dev/null +++ b/html/features.html @@ -0,0 +1,210 @@ +<!-- FIXME: would be nice to provide links from features + mentioned here to user-manual. --> +<h2>Features of Proof General</h2> +<p> +It doesn't matter if you're an Emacs militant or a pacifist! +</p> + +<p> The aim of Proof General is to provide powerful and configurable +interfaces which help user-interaction with proof assistants. Proof +General targets power users rather than novices, but is designed to be +useful to both. Proof General leads to an environment for serious +<i>proof engineering</i> of interactively-constructed proofs. +</p> +<p>Proof General is used by many people for organizing large proof +developments, and also for teaching interactive proof. +They enjoy the following features:</p> +</p> +<dl> + <?php dt("Script management","script") ?> + <dd> + A <em>proof script</em> is a sequence of commands sent to + a proof assistant to construct a proof, usually stored in + a file. <em>Script management</em> connects the editing of a + proof script directly to an interactive proof process, + maintaining consistency between the edit buffer + and the state of the proof assistant. + <p> + Proof General colours a proof script to show the state in the proof + assistant. Parts of a proof script that have been processed are + displayed in blue and are "locked" -- they cannot be edited. Parts + of the script currently being processed by the proof assistant are + shown in red. Bodies of completed proofs in the locked region + can be hidden from view to help browsing. + Proof General has commands for processing new parts + of the buffer, or undoing already processed parts. + </p> + <p> + Take a look at these + <a href="screenshot">screenshots</a> + of Proof General to see script management in action. + </p> + </dd> +</dl><dl> + <?php dt("Simplified interaction model","simple") ?> + <dd> + Proof General is designed for proof assistants which have a + command-line (shell) interpreter. When using Proof General, the proof + assistant's shell is hidden from the user. Communication takes + place via three buffers (Emacs text widgets). The <i>script + buffer</i> holds input, the commands to construct a proof. The + <i>goals buffer</i> displays the current list of subgoals to be + solved. The <i>response buffer</i> displays other output from the + proof assistant. By default, only two of these three buffers are + displayed at once. This means that the user only sees the output + from the most recent interaction, rather than a screen full of + output from the proof assistant. + <p> + Despite this more friendly communication model, Proof General does not + commandeer the proof assistant shell: the user still has complete + access to it if necessary. + </p> + </dd> +</dl><dl> + <?php dt("Multiple files","multiple") ?> + <dd> + Script management in Proof General can work across many script + 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 + Proof General (based on the order in which files were processed). + </p> + </dd> +</dl><dl> + <?php dt("Subterm highlighting and proof by pointing","pbp") ?> + <dd> + <p> + Using hidden markup in the concrete syntax, Proof General allows the + user to explore the structure of complex terms output by the prover. + This provides nifty features for cutting-and-pasting subterms, + querying the type of a subterm, looking up the definition of an + identifier, and so on. + </p> + <p> + <em>Proof by pointing</em> uses this markup to allow the prover + to suggest steps in a proof, guided by the user's gestures + in displayed goals. For example, clicking on a hypothesis inserts + a proof step into the script to solve a goal using that hypothesis, + and executes it. + </p> + <?php footnote("Subterm markup is only fully supported by LEGO at the moment, with an experimental implementation of proof by pointing. Isabelle highlights only variables. If you would like to see these features better supported in your favourite proof assistant, please canvas the implementor to add subterm-markup support.") ?> + </dd> +</dl><dl> + <?php dt("Toolbar and menus","toolbar") ?> + <dd> + Proof General has a toolbar with buttons for examining + the proof state, starting a proof, manoeuvring in the proof script, + restarting the prover, saving a proof, searching for a theorem, + issuing a command, interrupting the assistant, and getting help. + <p> + Using the toolbar, you can replay proofs without knowing any + low-level commands of the proof assistant or any Emacs hot-keys! + <p> + Additionally, the toolbar commands and many more besides are + available on menus; you don't need to know magical key presses for + any features. + </p> + </dd> +</dl><dl> + <?php dt("Syntax highlighting","fontlock") ?> + <dd> + Syntax highlighting is an editing feature which decorates a file + with different colours or fonts according to the syntax of some + language (usually a programming language). + <p> + Proof General decorates proof scripts: proof commands are + highlighted and different fonts may be used for definitions and + assumptions, for example. + </p> + </dd> +</dl><dl> + <?php dt("Real symbols","xsymbol") ?> + <dd> + Proof General has a close integration with the + powerful + <a href="http://x-symbol.sourceforge.net/">X-Symbol</a> + package, which makes it easy to transparently use real symbols and + Greek letters in your proofs. + <br> + Instead of seeing "not P", you see "¬ P", instead + of "a * b", you see "a × b", etc. + <br> + (Those examples are simple so they will work on most browsers + without needing images, see the + <a href="screenshot">screenshots</a> for more examples.) + <p> + </dd> +</dl><dl> + <?php dt("Proof-script editing facilities","funcmenu") ?> + <dd> + <p> + Many facilities are provided for editing proof scripts. + The <i>completion</i> mechanism of Emacs can be used to + help type keywords and identifier names. + The <i>outline</i> mode of Emacs allows hiding of parts of proof scripts; + a further special <i>proof hiding</i> facility is provided to + hide the body of completed proofs. + <i>Navigation</i> in the script is supported by a pull-down menu + which gives easy access to the theorems, definitions, and declarations + in the current buffer. + </p> +<!-- it is in FSF Emacs if you download func-menu.el from somewhere --> +<!-- <?php footnote("Definitions menu is available in XEmacs only") ?> --> + <p> + </dd> +</dl><dl> + <?php dt("Remote proof assistant.") ?> + <dd> + Sometimes you may want to run a proof assistant on a powerful remote + machine. Proof General can communicate with a proof assistant running + remotely, while your files and editor reside on your local machine. + <p></p> + </dd> +</dl><dl> + <?php dt("Tags","tags") ?> + <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. + 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") ?> --> + <p></p> + </dd> +</dl><dl> + <?php dt("Adaptability","generic") ?> + <dd> + Proof General is designed to be adaptable. Many aspects + of its behaviour can be easily customized (using dialogue boxes and + buttons, no text file editing!). + <p> + Most importantly, Proof General is generic, so you can adapt it to + a new proof assistant with surprisingly little effort. + <p> + Adapting for a new proof assistant is mainly a matter of setting + some variables with regular expressions to help parse output from + the prover, and setting other variables with commands to send to the + prover. See this basic + <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", + "example instance"); ?>. + To get the most from Proof General (proof by pointing, for + example), it may be necessary to put some hooks in + the output routines of the proof assistant. + </p> + Please feel free to download Proof General to customize it for a new + system, and + <?php hlink("feedback.html","tell us ","Feedback form")?> + how you get on. + </dd> +</dl> +<p> +For (even) more details of Proof General's features, see the manuals and +papers on the <a href="doc">documentation page</a>. +</p> + diff --git a/html/feedback b/html/feedback new file mode 100644 index 00000000..94066bcf --- /dev/null +++ b/html/feedback @@ -0,0 +1,6 @@ +<?php include('feedback.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?> + diff --git a/html/feedback.php b/html/feedback.php new file mode 100644 index 00000000..e599bfcd --- /dev/null +++ b/html/feedback.php @@ -0,0 +1,89 @@ +<?php +## +## Proof General feedback form. +## +## David Aspinall, June 1999. +## +## $Id$ +## + require('functions.php3'); + + if ($argv[0] !="submit"): +### +### Feedback form +### + small_header("Proof General Feedback Form"); +?> + +<p> +Please use the form below to send us comments, suggestions, +or offers to help with Proof General development. +Or simply send an email directly to +the <?php mlinktxt($project_feedback, "Proof General maintainer <$project_feedback>."); ?> +</p> +<p> +You can also report a bug using this form, although it would +be more helpful to do this from within Emacs, using the +"<kbd>Proof General -> Submit bug report</kbd>" menu command. +</p> + +<form method=post action="<?php print $PHP_SELF . "?submit"; ?>"> +<table width="450" border="0" cellspacing="2" cellpadding="0"> +<tr> + <td width="20%">From:</td> + <td width="80%"><input type=text name="from" size="40"></td> +</tr> +<tr> + <td>Subject:</td> + <td><input type=text name="subject" size="40"></td> +</tr> +<tr><td colspan="2"> +<textarea rows="15" cols="70" wrap="physical" name="feedback"> +Dear Proof General developers, +</textarea> +(For us to reply, please include a proper email + address in the From box). +</td></tr> +<tr><td></td><td> +<p align=right> +<input type=reset value="Clear"> +<input type=submit value="Send feedback"> +</p> +</td></tr> +</table> +</form> + +<?php + click_to_go_back(); + footer(); + else: +## +## Process feedback +## + small_header("Thank-you!"); + + /* NB: No validation of address! */ + + /* FIXME: could append extra info to feedback. */ + + $message = "From:\t\t" . $from . "\nSubject:\t" . $subject + . "\n\n" . "Message:\n" . $feedback; + + if ($from != "") { print "<p>Dear " . $from . ",</p>\n"; }; + print "<p>"; + print "Thank-you for sending us feedback"; + if ($subject != "") { print " about " . $subject; }; + print ".</p>\n<p>"; + print "If you provided a valid return email address, somebody from the Proof General team will acknowledge your message after it has been read."; + print "</p>"; + + mail($project_feedback, + "[Web Feedback Form]: " . $subject, + $message, + "Reply-To: " . $from . "\n"); + + click_to_go_back(); + + footer(); +endif; +?> diff --git a/html/fileshow.php b/html/fileshow.php new file mode 100644 index 00000000..ded131d6 --- /dev/null +++ b/html/fileshow.php @@ -0,0 +1,8 @@ +<?php + require('functions.php3'); + require('elispmarkup.php3'); + $filename=$HTTP_GET_VARS["file"]; + $title=$HTTP_GET_VARS["title"]; + $expanded=$HTTP_GET_VARS["expanded"]; + fileshowmarkup($file,$title,$expanded); +?> diff --git a/html/footer.html b/html/footer.html new file mode 100644 index 00000000..de01ece5 --- /dev/null +++ b/html/footer.html @@ -0,0 +1,10 @@ +<!-- This is the footer --> +<hr> +<address> +Web pages by +<a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>. +<br> +Contact +<?php mlinktxt($project_feedback, "Proof General maintainer."); ?> +<br> + diff --git a/html/functions.php3 b/html/functions.php3 new file mode 100644 index 00000000..1a3a1457 --- /dev/null +++ b/html/functions.php3 @@ -0,0 +1,337 @@ +<?php +// +// Dave's PHP Header +// +// Included in every page. +// Prints DTD, <html> opening tag, +// and defines some useful functions. +// +// David Aspinall, June 1999/2002. +// +// $Id$ +// +// + + +// Project configuration + +$project_email = "feedback@proofgeneral.org"; +$project_list = "users@proofgeneral.org"; +$project_feedback = "feedback@proofgeneral.org"; + +// Disable when free parking forwarding is broken +// $proofgenatdcs = "proofgen@dcs.ed.ac.uk"; +// $project_email = $proofgenatdcs; +// $project_list = $proofgenatdcs; +// $project_feedback = $proofgenatdcs; + +$project_title = "Proof General"; + +$project_subtitle = "Organize your Proofs!"; +$project_full_title = $project_title . " --- " . $project_subtitle; + +if ($title == "") { $title = $project_title; } // default page title. + +/////////////////////////////////////////////////////////////////// +// +// DTD +// + +$dtd_strict = "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.0//EN\" \"http://www.w3.org/TR/REC-html40/strict.dtd\">\n"; +$dtd_loose = "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.0 Transitional//EN\" \"http://www.w3.org/TR/REC-html40/loose.dtd\">\n"; +$xml_header="<?xml version=\"1.0\"?>"; +$dtd_xml_loose ="<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">"; +$dtd_xml_strict ="<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">"; +$html="<html>\n"; +$xhtml="<html xmlns=\"http://www.w3.org/1999/xhtml\">\n"; + +print $dtd_loose; +print $html; + +//print $xml_header; +//print $dtd_xml_strict; +//print $xhtml; + + +// Validator address + +// $validator = "http://validator.dcs.ed.ac.uk/"; +// It's a private link which won't work elsewhere, but never mind. + $validator = "http://localhost/validator/"; + +function mlink($addr) { + print "<a href=\"mailto:" . $addr . "\">" . $addr . "</a>"; +} + +function mlinktxt($addr,$txt) { + print "<a href=\"mailto:" . $addr . "\">" . $txt . "</a>"; +} + + +// FIXME: doesn't seem to work. Why not? +function project_email() { + mlink($project_email); +} + + +/* Style sheet element for dt doesnt work in Netscape 4, so hack it here. + NB! This violates HTML 4 DTD. +*/ +function dt($string,$name="") { + print "<dt>"; + if ($name != "") { print "<a name =\"$name\">"; } + print "<div style=\"font-style:italic; font-weight: bold\">"; + print $string; + print "</div>"; + if ($name != "") { print "</a>"; } + print "</dt>"; +} + +/* Automatic footnotes? */ +/* FIXME: for now, just inline them. */ + +function footnote ($text) { + print "<p><i><small>[" . $text . "]</small></i></p>"; +} + +/* A hyper-link with optional mouse over text. + Could be made more sophisticated to do roll-overs, + or whatever. +*/ + +function hlink ($url,$text,$mouseover="") { + print "<a href=\"" . $url . "\""; + if ($mouseover != "") { + print " onMouseOver=\"window.status='" . $mouseover . "'; return true;\""; + }; + print ">" . $text . "</a>"; +} + +/* Determining download sizes (print broken message if file not found) */ + +function download_size($filename) { + if (file_exists($filename)) { + $size = filesize($filename); + $sizek = (int) ($size/1024); + print " ("; + if ($sizek == 0) { + print $size . " bytes)"; + } else { + print $sizek . "k)"; + } + } else { + print " (link broken)"; + } +} + +function download_link($filename,$linkname = "") { + print "<a href=\"" . $filename . "\">"; + if ($linkname == "") { + print $filename; + } else { + print $linkname; + }; + print "</a>"; + print download_size($filename); +} + +function date_modified($filename) { + $time = filemtime($filename); + if ($time) { + print "Last modified " . strftime("%d %B %Y",$time) . ".\n"; + } +} + +function small_header($title) { + include('head.html'); + include('smallheader.html'); + print "<h1>" . $title . "</h1>\n</td>\n</table>\n"; +} + +function small_header_body($title) { + include('smallheader.html'); + print "<h1>" . $title . "</h1>\n</td>\n</table>\n"; +/* print "<p>"; FIXME: hack to get CSS to work with bad HTML from texi2html */ +} + +/* FIXME: remove this function: maybe just set a global variable, + or use SCRIPT_NAME, and then include footer.html. */ + +function footer($filemodified=".") { + global $project_feedback; + include('footer.html'); + date_modified($filemodified); + print "</address>\n"; +// print "</font>\n"; /* Naughty stuff for older browsers, shouldn't do if V4 */ + print "</body>\n"; + print "</html>\n"; +} + +function click_to_go_back() { + // FIXME: the empty href no longer refers to the root, + // so this use of "/" breaks relative linking. + print "<p>\nClick <a href=\"/\">here</a> to go back to the "; + print $project_title; // FIXME: doesn't work, prints nothing. + print " front page.</p>\n"; +} + +/* Link to a marked up file */ +/* NB: could determine type automatically! */ + +function fileshow($filename,$text="",$title="") { + if ( $text == "") { $text=$filename; }; + $message=$title; + if ( $message == "") { $message=$filename; }; + $titlecode = ($title == "" ? "" : "&title=" . urlencode($title)); + hlink("fileshow.php?file=" . urlencode($filename) . $titlecode, + $text, $message); +} + +function fileshowmarkup($filename,$title="",$expanded="") { + if ($title=="") { $title = $filename; }; + small_header($title); + print "<pre>\n"; + /* I hope this is enough to prevent access outside cwd */ + if (substr($filename,0,1)=="." or + substr($filename,0,1)=="/" or + substr($filename,0,1)=="~") { + print "Sorry, can't show you that file!\n"; + } elseif (substr($filename,-3)==".el") { + elisp_markup($filename,"fileshow.php"); + } else { + outline_markup($filename,"fileshow.php",$expanded); + } + print "</pre>\n"; + print "<hr>"; + click_to_go_back(); + footer(); +} + +/* Similar for html file (NB: could pick automatically) */ + +function htmlshow($filename,$text="",$title="") { + if ( $text == "") { $text=$filename; }; + $message=$title; + if ( $message == "") { $message=$filename; }; + $urlbits = parse_url($filename); + hlink("htmlshow.php" + . "?title=" . urlencode($title) + . "&file=" . urlencode($urlbits["path"]) + . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]), + $text, $message); +} + +function htmlshow_link($filename,$title="") { + $urlbits = parse_url($filename); + return "htmlshow.php" + . "?title=" . urlencode($title) + . "&file=" . urlencode($urlbits["path"]) + . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]); +} + + +/* Markup plain text file, by escaping < and > */ + +function markup_plain_text($filename) { + $file = file($filename); + for($i = 0;$i < count($file);$i++) { + $line = $file[$i]; + $line = ereg_replace("<","<",$line); + $line = ereg_replace(">",">",$line); + print $line; + }; +} + +/* Hack an html file to be shown with our style sheet + and hack relative links to go via htmlshow.php. + This isn't particularly robust, but seems to work for + the output of texi2html. +*/ + +function hack_html($filename,$title="",$docrooturl="") { + if ($title=="") { $title=$filename; }; + if ($docrooturl=="") { + $docrooturl = "htmlshow.php?title=" . urlencode($title); + } + $file = file($filename); + /* Paste style sheet in head */ + for($i = 0;$i < count($file);$i++) { + $line = $file[$i]; + if (eregi("</HEAD>",$line)) { + /* Paste in style sheet */ + print "<style type=\"text/css\">\n<!--"; + include("proofgen.css"); + print "-->\n</style>\n"; + /* End style sheet paste in */ + print $line; + $i++; + break; + } else { print $line; }; + } + /* Now parse rest of document, hacking relative links. */ + /* Matching here is not great, will get confused by html tags inside strings, etc. */ + for (;$i < count($file);$i++) { + $line = $file[$i]; + /* PHP has no way to get the match position, so we have to + match a suffix of the line, add extra parenthesis, and calculate it. */ + while (eregi("(<A([^>]*)(HREF=\"([^\"]+)\")(.*))",$line,$linebits)) { + /* found URL in a particularly simple form */ + $matchpos = strlen($line) - strlen($linebits[1]); + print substr($line,0,$matchpos); /* start of line */ + $line = $linebits[5]; /* rest of line after link */ + $urlbits = parse_url($linebits[4]); + if ($urlbits["host"]=="") { + /* Assume a relative link, let's hack it. */ + if ($urlbits["path"]=="") { + /* A fragment in same file */ + $newurl = $docrooturl . "#" . $urlbits["fragment"]; + } else { + /* Another file, use same title */ + /* FIXME: would be nice to deal with split info files + here by adding aliases somehow */ + $newurl = "htmlshow.php?title=" . urlencode($title) + . "&file=" + . urlencode(dirname($filename) . "/" . $urlbits["path"]) + . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]); + }; + print "<A " . $linebits[2] . " HREF=\"" . $newurl . "\""; + } else { print "<A " . $linebits[2] . $linebits[3]; } + }; + /* Hack on a header and footer */ + if (eregi("<BODY.*>",$line)) { + /* Assume there's nothing else interesting on the line, whoops. */ + print $line; + small_header_body($title); + } elseif (eregi("</BODY>",$line)) { + /* Assume there's nothing else interesting on the line, whoops. */ + click_to_go_back(); + print $line; + } else { + print $line; + }; + } +} + + + +/* Display a small page with standard header, footer added on. + Much like htmlshow. */ + +function smallpage($filename,$text="",$title="",$message="") { + if ( $text == "") { $text=$filename; }; + if ( $message == "") { $message=$title; }; + if ( $message == "") { $message=$filename; }; + $urlbits = parse_url($filename); + hlink("smallpage.php" + . "?title=" . urlencode($title) + . "&file=" . urlencode($urlbits["path"]) + . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]), + $text, $message); +} + +/* Specialised version for projects */ + +function pgproject($filename,$title) { + smallpage("projects/$filename.html",$title,"Proof General Project",$title); +} + diff --git a/html/gallery b/html/gallery new file mode 100644 index 00000000..7342616d --- /dev/null +++ b/html/gallery @@ -0,0 +1,6 @@ +<?php include('gallery.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?> + diff --git a/html/gallery.php b/html/gallery.php new file mode 100644 index 00000000..035136f1 --- /dev/null +++ b/html/gallery.php @@ -0,0 +1,84 @@ +<?php + require('functions.php3'); + small_header("Proof General Gallery"); + ?> + +<blockquote> +<p> +Here are some publicity pictures for Proof General. They were created +by David Aspinall in his spare time, using the excellent freeware +programs <a href="http://www.gimp.org">GIMP</a> and <a +href="http://www.blender.nl">Blender</a>. The General himself is +based on a commercial mesh given away by +<a href="http://www.viewpoint.com">Viewpoint</a>. +</p> +<p> +Click on a thumbnail to see a full-size images. All full-size images +are 720x990 pixel JPGs (a nice size to print at 180dpi on A5 paper). +Please download and print for your own use! +<p> +Copyright for the images is held by +<a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>. +Please do not publish the images or incorporate them into other +work without his permission. If you have comments or suggestions, +or if you would like a copy of one of the images +in another size or format, +please <a href="feedback">contact us</a>. +</p> + +</p> +<p> +For pictures of what Proof General looks like in use, +see the <a href="screenshot">screenshots</a> page. +</p> +</blockquote> + +<!-- todo: php3 this --> +<table width="80%"> +<tr> +<td width="200"> +<a href="images/portrait.jpg"> +<img src="images/portrait-thumb.jpg" alt="Portrait" width=150 height=206 border=0> +</a> +</td> +<td> +<p> +Proof General portrait <br> +This is the Proof General logo, +with the home page URL at the bottom. <br> +A nice poster for your wall or door. <br> +</p> +</tr> +<tr> +<td> +<a href="images/whip.jpg"> +<img src="images/whip-thumb.jpg" alt="New recruit" width=150 height=206 border=0> +</a> +</td> +<td> +<p> +New Recruits Wanted <br> +This is a request for help with the Proof General +project. <br> +Please <a href="feedback">sign up here</a>! +</p> +</tr> +<tr> +<td> +<a href="images/whole-man.jpg"> +<img src="images/whole-man-thumb.jpg" alt="Whole man" width=150 height=206 border=0> +</a> +</td> +<td> +<p> +Scary boots! <br> +This is a full-length shot of Proof General, +again with the home page at the bottom. +</p> +</tr> +</table> + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/head.html b/html/head.html new file mode 100644 index 00000000..4259dca1 --- /dev/null +++ b/html/head.html @@ -0,0 +1,22 @@ +<head> + <meta http-equiv="Content-Type" content="text/html; charset=utf-8"> + <meta name="author" content="David Aspinall <da@dcs.ed.ac.uk>"> + <meta name="keywords" content="Isabelle, LEGO, Coq, Emacs, XEmacs, + Interface, Theorem Prover, GUI, David Aspinall"> + <meta name="description" content="Proof General is an Emacs based + generic interface for theorem provers"> + <link rel="stylesheet" href="proofgen.css" type="text/css"> + <link rel="SHORTCUT ICON" href="favicon.ico"> + <title><?php print $title ?></title> +</head> + <!-- Duplicate some style entries in body elt to support Version 3 browsers. + FIXME: Shouldn't really serve this mess up to V4s and later. --> +<!-- <font face="Verdana, Arial, LucidaSans, sans-serif;">--> +<body + bgcolor="#2D1D03" + background="images/canvaswallpaper.jpg" + text="#FFFFFF" + link="#FFD820" + vlink="#FFD820" + alink="#FFF030" + > diff --git a/html/header.html b/html/header.html new file mode 100644 index 00000000..b335ac24 --- /dev/null +++ b/html/header.html @@ -0,0 +1,61 @@ +<!-- This is the header --> +<table width="650"> +<tr> +<td width="100"> +<a href="."> +<img src="images/ProofGeneral.jpg" alt="Proof General" width=90 height=119 border=0> +</a> +</td> +<td> +<center> + <img src="images/pg-text.gif" alt="Proof General" width=170 height=17 border=0> + <h1>Organize your proofs!</h1> +<?php + /* Header link generator. David Aspinall, June 1999. + * Based orginially on navbar.php3 by Douglas Campbell + * Look for $WANTED in array. If not found, use default of "Home" + * and fix $WANTED. Hrefs are given by page parameter to current doc. + */ + $separator='<td width=10em><img align=left src="images/bullethole.gif" width=15 height=15 alt="."> '; + $urlbits = parse_url($REQUEST_URI); + $file = ereg_replace("^(.*/)+","",$urlbits["path"]); + $WANTED = ereg_replace(".html","",$file); + print "<table width=\"80%\" class=\"menubar\"><tr align=\"left\">\n"; + $links_arr = array( + "Home" => "main", + "Features" => "features", + "Download" => "download", + "Documentation" => "doc", + + "News" => "news", + "Screenshots" => "screenshot", + "Development" => "devel", + "About" => "about" + ); + $DEFAULT = $links_arr["Home"]; + $wanted_okay = 0; + for (reset($links_arr); $name = key($links_arr); next($links_arr)) { + if ($WANTED == $links_arr[$name]) { + $wanted_okay = 1; + } + }; + if (! $wanted_okay) { + $WANTED = "main"; + }; + for (reset($links_arr); $name = key($links_arr); next($links_arr)) { + print $separator; + if ($WANTED == $links_arr[$name]) { + print "<font color=\"white\">" . $name . "</font>"; + } + else { + print "<a href=\"$links_arr[$name]\">$name</a>"; + } + print " </td>\n"; + if ($name=="Documentation") print "</tr >\n<tr>"; + } + print "</tr></table>\n"; +?> +</td></tr> +</table> +</center> +<!-- End of header -->
\ No newline at end of file diff --git a/html/hits b/html/hits new file mode 100644 index 00000000..6d5c2be6 --- /dev/null +++ b/html/hits @@ -0,0 +1,26 @@ +<?php + $counterFile = "counter.txt"; + $counterStart = "counterstart.txt"; + $maxlen=10; + require('functions.php3'); + small_header("Hit counter"); + print "<p>"; + if (is_readable($counterFile)) { + print "These pages have been accessed "; + readfile($counterFile); + print " times "; + if (is_readable($counterStart)) { + $fp=fopen($counterStart,"r"); + $start=fgets($fp,20); + print "since "; + print strftime("%d %B %Y",$start); + print ".\n"; + } else { + print "<br>\n(could not access time stamp file $counterStart)\n"; + }; + } else { + echo "Could not access hit counter file $counterFile\n"; + }; + print "</p>"; + footer(); +?> diff --git a/html/htmlshow.html b/html/htmlshow.html new file mode 100644 index 00000000..d9cb8b46 --- /dev/null +++ b/html/htmlshow.html @@ -0,0 +1,5 @@ +<?php + require('functions.php3'); + hack_html($file,$title); + footer(); +?> diff --git a/html/htmlshow.php b/html/htmlshow.php new file mode 100644 index 00000000..915aac6f --- /dev/null +++ b/html/htmlshow.php @@ -0,0 +1,11 @@ +<?php + require('functions.php3'); + if (substr($file,0,1)=="." or + substr($file,0,1)=="/" or + substr($file,0,1)=="~") { + print "Sorry, can't show you that file!\n"; + } else { + hack_html($file,$title); + } + footer(); +?> diff --git a/html/images/.cvsignore b/html/images/.cvsignore new file mode 100644 index 00000000..5c165d91 --- /dev/null +++ b/html/images/.cvsignore @@ -0,0 +1 @@ +.xvpics diff --git a/html/images/IsaPGscreen.jpg b/html/images/IsaPGscreen.jpg Binary files differnew file mode 100644 index 00000000..5e2dda74 --- /dev/null +++ b/html/images/IsaPGscreen.jpg diff --git a/html/images/PG-small.jpg b/html/images/PG-small.jpg Binary files differnew file mode 100644 index 00000000..50bb9cf6 --- /dev/null +++ b/html/images/PG-small.jpg diff --git a/html/images/ProofGeneral.jpg b/html/images/ProofGeneral.jpg Binary files differnew file mode 100644 index 00000000..d2c430cd --- /dev/null +++ b/html/images/ProofGeneral.jpg diff --git a/html/images/bullethole.gif b/html/images/bullethole.gif Binary files differnew file mode 100644 index 00000000..1eb03072 --- /dev/null +++ b/html/images/bullethole.gif diff --git a/html/images/canvaswallpaper.jpg b/html/images/canvaswallpaper.jpg Binary files differnew file mode 100644 index 00000000..8062bd4e --- /dev/null +++ b/html/images/canvaswallpaper.jpg diff --git a/html/images/coq-badge.gif b/html/images/coq-badge.gif Binary files differnew file mode 100644 index 00000000..901e7645 --- /dev/null +++ b/html/images/coq-badge.gif diff --git a/html/images/coqlogo4.gif b/html/images/coqlogo4.gif Binary files differnew file mode 100644 index 00000000..5899de81 --- /dev/null +++ b/html/images/coqlogo4.gif diff --git a/html/images/coqlogo4.xcf b/html/images/coqlogo4.xcf Binary files differnew file mode 100644 index 00000000..21cd46cb --- /dev/null +++ b/html/images/coqlogo4.xcf diff --git a/html/images/isabelle-badge.gif b/html/images/isabelle-badge.gif Binary files differnew file mode 100644 index 00000000..8da95453 --- /dev/null +++ b/html/images/isabelle-badge.gif diff --git a/html/images/isabelle.gif b/html/images/isabelle.gif Binary files differnew file mode 100644 index 00000000..171b2101 --- /dev/null +++ b/html/images/isabelle.gif diff --git a/html/images/lego-badge.gif b/html/images/lego-badge.gif Binary files differnew file mode 100644 index 00000000..182ad85f --- /dev/null +++ b/html/images/lego-badge.gif diff --git a/html/images/pg-coq-screenshot.png b/html/images/pg-coq-screenshot.png Binary files differnew file mode 100644 index 00000000..eb071514 --- /dev/null +++ b/html/images/pg-coq-screenshot.png diff --git a/html/images/pg-coq-thumb.png b/html/images/pg-coq-thumb.png Binary files differnew file mode 100644 index 00000000..1510b502 --- /dev/null +++ b/html/images/pg-coq-thumb.png diff --git a/html/images/pg-isa-screenshot.png b/html/images/pg-isa-screenshot.png Binary files differnew file mode 100644 index 00000000..e903e4e3 --- /dev/null +++ b/html/images/pg-isa-screenshot.png diff --git a/html/images/pg-isa-thumb.png b/html/images/pg-isa-thumb.png Binary files differnew file mode 100644 index 00000000..d0db67cc --- /dev/null +++ b/html/images/pg-isa-thumb.png diff --git a/html/images/pg-isar-screenshot.png b/html/images/pg-isar-screenshot.png Binary files differnew file mode 100644 index 00000000..6ea369de --- /dev/null +++ b/html/images/pg-isar-screenshot.png diff --git a/html/images/pg-isar-thumb.png b/html/images/pg-isar-thumb.png Binary files differnew file mode 100644 index 00000000..bc558d56 --- /dev/null +++ b/html/images/pg-isar-thumb.png diff --git a/html/images/pg-lego-console-thumb.png b/html/images/pg-lego-console-thumb.png Binary files differnew file mode 100644 index 00000000..0a44450a --- /dev/null +++ b/html/images/pg-lego-console-thumb.png diff --git a/html/images/pg-lego-console.png b/html/images/pg-lego-console.png Binary files differnew file mode 100644 index 00000000..0e7c22a3 --- /dev/null +++ b/html/images/pg-lego-console.png diff --git a/html/images/pg-lego-screenshot.png b/html/images/pg-lego-screenshot.png Binary files differnew file mode 100644 index 00000000..e8c6b749 --- /dev/null +++ b/html/images/pg-lego-screenshot.png diff --git a/html/images/pg-lego-thumb.png b/html/images/pg-lego-thumb.png Binary files differnew file mode 100644 index 00000000..6f650baa --- /dev/null +++ b/html/images/pg-lego-thumb.png diff --git a/html/images/pg-text.gif b/html/images/pg-text.gif Binary files differnew file mode 100644 index 00000000..cf592478 --- /dev/null +++ b/html/images/pg-text.gif diff --git a/html/images/phox-einstein.jpg b/html/images/phox-einstein.jpg Binary files differnew file mode 100644 index 00000000..97af4ee3 --- /dev/null +++ b/html/images/phox-einstein.jpg diff --git a/html/images/portrait-thumb.jpg b/html/images/portrait-thumb.jpg Binary files differnew file mode 100644 index 00000000..d84d27b4 --- /dev/null +++ b/html/images/portrait-thumb.jpg diff --git a/html/images/portrait.jpg b/html/images/portrait.jpg Binary files differnew file mode 100644 index 00000000..a23f0f16 --- /dev/null +++ b/html/images/portrait.jpg diff --git a/html/images/silverrule.gif b/html/images/silverrule.gif Binary files differnew file mode 100644 index 00000000..3ad7fbda --- /dev/null +++ b/html/images/silverrule.gif diff --git a/html/images/vh40.gif b/html/images/vh40.gif Binary files differnew file mode 100644 index 00000000..c5e9402e --- /dev/null +++ b/html/images/vh40.gif diff --git a/html/images/whip-thumb.jpg b/html/images/whip-thumb.jpg Binary files differnew file mode 100644 index 00000000..16aac5b4 --- /dev/null +++ b/html/images/whip-thumb.jpg diff --git a/html/images/whip.jpg b/html/images/whip.jpg Binary files differnew file mode 100644 index 00000000..1a6341b6 --- /dev/null +++ b/html/images/whip.jpg diff --git a/html/images/whole-man-thumb.jpg b/html/images/whole-man-thumb.jpg Binary files differnew file mode 100644 index 00000000..32175a27 --- /dev/null +++ b/html/images/whole-man-thumb.jpg diff --git a/html/images/whole-man.jpg b/html/images/whole-man.jpg Binary files differnew file mode 100644 index 00000000..f3fff341 --- /dev/null +++ b/html/images/whole-man.jpg diff --git a/html/index.php b/html/index.php new file mode 100644 index 00000000..3eb50db3 --- /dev/null +++ b/html/index.php @@ -0,0 +1,8 @@ +<?php require('functions.php3'); ?> +<?php include('head.html'); ?> +<?php + include('header.html'); + include($WANTED . '.html' . $WANTEDFRAG); + footer(); +?> + diff --git a/html/index.shtml b/html/index.shtml new file mode 100644 index 00000000..d4bdff95 --- /dev/null +++ b/html/index.shtml @@ -0,0 +1,3 @@ +<!-- This is the entry point to the Proof General web pages --> +<!--#include file="counter.php3"--> +<!--#include file="index.php"--> diff --git a/html/kit b/html/kit new file mode 100644 index 00000000..d7ba8cb2 --- /dev/null +++ b/html/kit @@ -0,0 +1,5 @@ +<?php include('kit.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?> diff --git a/html/kit.html b/html/kit.html new file mode 100644 index 00000000..d7ba8cb2 --- /dev/null +++ b/html/kit.html @@ -0,0 +1,5 @@ +<?php include('kit.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?> diff --git a/html/kit.php b/html/kit.php new file mode 100644 index 00000000..0aa4015e --- /dev/null +++ b/html/kit.php @@ -0,0 +1,49 @@ +<?php + require('functions.php3'); + small_header("Proof General Kit"); + ?> + +<p> +The Proof General Kit project is in an early pre-experimental stage at +the moment. If you are interested in collaborating, or have ideas +or suggestions to contribute, please send a note to +<a href="mailto:kit@proofgeneral.org"><tt>kit@proofgeneral.org</tt></a> +</p> + +<h3>Planning</h3> +<p> +Ideas for the future of Proof General are described in these papers: +</p> +<ul> +<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>. + <b><i>Protocols for Interactive e-Proof</i></b>. + Draft version, see + <a href="http://homepages.inf.ed.ac.uk/da/papers/drafts/#eproof">here</a>. +</li> +<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>. + <b><i>Proof General Kit (white paper)</i></b>. + Draft version, see + <a href="http://homepages.inf.ed.ac.uk/da/papers/drafts/#white">here</a>. +</li> +</ul> + +<h3>Development</h3> +<p> +Not much has been started yet. +<br> +But you can download the DTDs for PGIP and PGML, here: +</p> +<ul> +<li><?php download_link("Kit/dtd/pgip.dtd") ?> +</li> +<li><?php download_link("Kit/dtd/pgml.dtd") ?> +</li> +</ul> +<p> +Comments and contributions welcomed! +</p> + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/links b/html/links new file mode 100644 index 00000000..a58717d8 --- /dev/null +++ b/html/links @@ -0,0 +1,5 @@ +<?php include('index.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?>
\ No newline at end of file diff --git a/html/links.html b/html/links.html new file mode 100644 index 00000000..f18d20f0 --- /dev/null +++ b/html/links.html @@ -0,0 +1,71 @@ +<h2>Related projects</h2> +<p> +Here are some links to related things. +If you have any suggestions +for links to include here, please +<?php hlink("feedback","contact us","Feedback form")?>. +</p> + +<ul> +<li><a href="http://homepages.inf.ed.ac.uk/da/Isamode">Isamode</a> + is an XEmacs front-end for Isabelle. It has a different + feature collection compared with Proof General: + script management is not supported, but there are extensive + menus and shortcuts provided for common Isabelle + commands. +</li> +</ul> +<ul> +<li><a href="http://www-sop.inria.fr/croap/ctcoq/ctcoq-eng.html">CtCoq</a> + is an interface for the Coq theorem prover, developed + at INRIA, Sophia Antipolis, as part of + <a href="http://www-sop.inria.fr/croap/">Projet CROAP</a>. + Like Proof General, CtCoq is based on a general approach for + building user-interfaces for theorem provers, although no other + current theorem provers are supported. Unlike Proof General, CtCoq + is based on a graphical environment with structure editing, + created with the <a + href="http://www-sop.inria.fr/croap/centaur/centaur.html">Centaur</a> + system. +</li> +</ul> +<ul> +<li> + <a href="http://www.ags.uni-sb.de/~omega/">OMEGA</a> is + a collection of web-based distributed tools for supporting + theorem proving. +</li> +</ul> +<ul> +<li> + <a href="http://www.dcs.gla.ac.uk/prosper/">Prosper</a> is a project + to develop an extensible, open proof tool architecture for + incorporating formal verification into industrial CAD/CASE tool + flows and design methodologies. The tools include novel + user-friendly interfaces. +</li> +</ul> +<ul> +<li> + As a possible foundation for generic proof environments, + <a href="http://www.nag.co.uk/projects/openmath/omsoc/">OpenMath</a> + is a standard representation form for mathematical objects, which + links in with the <a href="http://www.w3.org/Math/">MathML</a> + markup language. +</li> +</ul> +<ul> +<li> + <a href="http://www.mrg.dist.unige.it/omrs/index.html">Open Mechanized Reasoning System (OMRS)</a> +</li> +</ul> +<ul> +<li> + <a href="http://www.cs.unibo.it/~asperti/HELM/home.html">Hypertextual Electronic Library of Mathematics (HELM)</a> +</li> +</ul> +<ul> +<li> + The <a href="http://eti.cs.uni-dortmund.de/eti/servlet/ETISiteApplication">Electronic Tool Integration</a> Platform. +</li> +</ul> diff --git a/html/mailinglist b/html/mailinglist new file mode 100644 index 00000000..3f2e387f --- /dev/null +++ b/html/mailinglist @@ -0,0 +1,66 @@ +<?php + require('functions.php3'); + small_header("Proof General Mailing Lists"); + ?> + +<p> +The Proof General Users mailing list is a low-volume list +used for announcements of new versions, and occasional +discussions amongst users. +</p> +<p> +This list is <i>not</i> for those having problems with the +software: please contact +<a href="mailto:support@proofgeneral.org">support@proofgeneral.org</a> +in the first instance. +</p> + +<h3>Subscriptions</h3> +<p> +To <b>subscribe or unsubscribe</b>, visit +the +<a href="http://lists.informatics.ed.ac.uk/mailman/listinfo/proofgeneral">Mailman +web page</a> for the list. +<br> +Alternatively, you can send a message to +<a href="mailto:proofgeneral-request@informatics.ed.ac.uk"> +<tt>proofgeneral-request@informatics.ed.ac.uk</tt></a> +with the word "<tt>subscribe</tt>" (or "<tt>unsubscribe <it>password</it></tt>") +in the message body. +</p> + + +<h3>Posting</h3> +<p> +The canonical mailing list address is +<a href="mailto:users@proofgeneral.org"><tt>users@proofgeneral.org</tt></a>. +<br> +This is an alias for +<tt>proofgeneral@informatics.ed.ac.uk</tt>. +</p> +<p> +In an effort to prevent spam, posting is restricted to list members. +Please <a href="http://lists.informatics.ed.ac.uk/mailman/listinfo/proofgeneral">subscribe here</a> before attempting to post. +</p> + +<h3>Archives</h3> +<p> +Archives of the list (since July 2002) are kept +<a href="http://lists.informatics.ed.ac.uk/pipermail/proofgeneral">here</a>. +</p> + +<h3>Proof General Developers list</h3> +<p> +There is a separate mailing list for those interested in the +development of Proof General. The canonical address +for this list is <a href="mailto:devel@proofgeneral.org"><tt>devel@proofgeneral.org</tt></a>. +Again, posting is restricted to list members. +Please visit the <a href="http://lists.informatics.ed.ac.uk/mailman/listinfo/proofgeneral-devel">Mailman web page</a> for subscription details. +</p> + + + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/mailinglist.html b/html/mailinglist.html new file mode 100644 index 00000000..59a74d27 --- /dev/null +++ b/html/mailinglist.html @@ -0,0 +1,6 @@ +<?php include('mailinglist'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?> + diff --git a/html/main b/html/main new file mode 100644 index 00000000..a58717d8 --- /dev/null +++ b/html/main @@ -0,0 +1,5 @@ +<?php include('index.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?>
\ No newline at end of file diff --git a/html/main.html b/html/main.html new file mode 100644 index 00000000..f1b44eda --- /dev/null +++ b/html/main.html @@ -0,0 +1,146 @@ +<h2>What is Proof General?</h2> +<p> +<b>Proof General</b> is a generic interface for proof assistants, +currently based on the customizable text editor <i>Emacs</i>. +It works with either +<a href="http://www.xemacs.org/">XEmacs</a> or +<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>. +Proof General has been developed at the +<a href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a> +in the <a href="http://www.ed.ac.uk/">University of Edinburgh</a>. +</p> +<p> +To find out more, check the +<a href="features"> features list</a> +and look at the +<a href="screenshot">screenshots</a>. +To get Proof General, visit the +<a href="download">download page</a>. +If you're not interested in interactive proof, +see the <a href="components">standalone components</a> +developed as part of Proof General. +To contact the developers, click +<?php hlink("feedback","here","Feedback form")?>. +</p> + + + +<h2>What systems does Proof General work with?</h2> + +<p>Proof General comes ready-to-go for these proof +assistants:</p> + +<table width="90%"> + <tr> + <td align="center"> + <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/", + "<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">", + "The Isabelle Home Page"); ?> + </td> + <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> + <div style="font-size: smaller"> + By + <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a> + and + Markus Wenzel. + </div> + </td> + </tr> + <tr> + <td align="center"> + <?php hlink("http://pauillac.inria.fr/coq/", + "<img src=\"images/coqlogo4.gif\" width=66 height=61 border=0 alt=\"Coq badge\">","The Coq Home Page") ?> + </td> + <td> + <b><?php fileshow("ProofGeneral/coq/README","Coq Proof General "); ?></b> for + <?php hlink("http://pauillac.inria.fr/coq/", + "Coq","The Coq Home Page") ?> + <br> + <div style="font-size: smaller"> + By Healfdene Goguen, Patrick Loiseleur, David Aspinall, and + <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>. + </div> + </td> + </tr> + <tr> + <td align="center"> + <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html", + "<img src=\"images/phox-einstein.jpg\" width=80 height=48 border=0 alt=\"PhoX logo\">", + "The PhoX Home Page") ?> + </td> + <td><b><?php fileshow("ProofGeneral/phox/README","PhoX Proof General "); ?></b> for + <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html", + "PhoX","The PhoX Home Page") ?> + <br> + <div style="font-size: smaller"> + By + <a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</a> + and + <a href="mailto:roziere@logique.jussieu.fr">Paul Roziere</a>. + </div> + </td> + </tr> + <tr> + <td align="center"> + <?php hlink("http://www.dcs.ed.ac.uk/home/lego", + "<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">", + "The LEGO Home Page") ?> + </td> + <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> + <div style="font-size: smaller"> + By Thomas Kleymann, Dilip Sequeira, + <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a> + and + <a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>. + </div> + </td> + </tr> +</table> + +<p>There are also <i>experimental</i> or <i>in-development</i> instances +of Proof General:</p> + +<ul> +<li><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>.</li> + +<li><b><?php fileshow("ProofGeneral/twelf/README","Twelf Proof +General"); ?></b>, for <a +href="http://www.twelf.org">Twelf</a>.</li> + +<li><b><?php fileshow("ProofGeneral/acl2/README","ACL2 Proof +General"); ?></b>, for <a +href="http://www.cs.utexas.edu/users/moore/acl2">ACL2</a>.</li> + +<li><b><?php fileshow("ProofGeneral/plastic/README","Plastic Proof +General"); ?></b>, for <a +href="http://www.dur.ac.uk/CARG/plastic.html">Plastic</a> +(in development).</li> + + +<li><b><?php fileshow("ProofGeneral/lclam/README","Lambda-Clam Proof +General"); ?></b>, for <a +href="http://dream.dai.ed.ac.uk/software/systems/lambda-clam/">Lambda-CLAM</a> +(in development).</li> +</ul> + +<p>The instances of Proof General marked "in development" above are +not considered complete, but are supported by the developers of proof +systems. The other instances above are "technology demonstrations" of +Proof General for other popular provers, but only show a bare fraction +of what is possible. We are seeking volunteers to support and improve +each of these (please <a href="feedback">send a note to <tt><?php +print $project_feedback; ?></tt></a> if you're interested).</p> + +<p>Proof General is ready to be customized to new proof assistants. +It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", +"very easy"); ?> to get basic support working. Full <a +href="ProofGeneral/doc/PG-adapting.pdf">documentation on +configuration</a> is provided.</p> diff --git a/html/mission.html b/html/mission.html new file mode 100644 index 00000000..a0203092 --- /dev/null +++ b/html/mission.html @@ -0,0 +1,136 @@ +<?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. +</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 +<a href="features#script">script management</a> +and +<a href="features#pbp">proof-by-pointing</a> +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 +<a href="features#multiple">multiple files</a>. +</dd> +</dl> + + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/news b/html/news new file mode 100644 index 00000000..a58717d8 --- /dev/null +++ b/html/news @@ -0,0 +1,5 @@ +<?php include('index.php'); ?> +<?php + /* This file needs some extra characters in it for apache to work its magic. + Things work fine as link to index.html, but it's tricky to include links + in cvs. */ ?>
\ No newline at end of file diff --git a/html/news.html b/html/news.html new file mode 100644 index 00000000..5ef51adc --- /dev/null +++ b/html/news.html @@ -0,0 +1,24 @@ +<h2>News about Proof General</h2> + +<ul> +<li><b>29th August 2002</b> +<p> +<i>Proof General 3.4 is released. Happy Proving!</i> +<br> +Go to the <a href="download">download page</a> to get it. +<br> +Please report any problems to <a href="mailto:support@proofgeneral.org"><tt>support@proofgeneral.org</tt></a>. +</p> +<li><b>1st July 2002</b> +<p> +Good news! The license conditions for Proof General will shortly be +changed to the <a href="http://www.gnu.org/copyleft/gpl.html">GPL</a>. +This relaxes the current conditions in several ways, in particular, +allowing packaging and distribution of the code by others. +</p> +</ul> +<!-- da: Put this line in instead if you're not me --> +<!-- <i>(News items entered by <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a> --> +<!-- unless noted.)</i> --> +<i>News items by <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>.</i> +<i>Click <a href="oldnews.html">here</a> for old news.</i> diff --git a/html/notes.txt b/html/notes.txt new file mode 100644 index 00000000..7d73ce30 --- /dev/null +++ b/html/notes.txt @@ -0,0 +1,56 @@ +Developers' Notes about Web Pages +--------------------------------- + +NEW: server hacks needed to serve these pages, giving nice urls + + PHP3 module included + .html treated as application + + Mime magic configured: + +LoadModule mime_magic_module modules/mod_mime_magic.so +AddModule mod_mime_magic.c +MimeMagicFile /etc/httpd/conf/magic + +to recognize files beginning <?php, by + adding this to /etc/httpd/conf/magic: + +0 string <?php application/x-httpd-php3 + +Then add these links: + + news -> index.html + doc -> index.html + +etc. + +*************** + +Notes about php: + +Some functions I've written + + <?php hlink("html file","text","status message")?> + +NB: no space after text so you must write + + <?php ... ?> blah + +to get a space. Don't put "blah" onto a new line, space will +be lost! + + +************* + +Tell Thomas (& other folk?) to update his home page links to Proof General. +[Probably okay: Thomas links to image in home directory, but we'll + keep that as a copy of images/ProofGeneral.jpg] + +************* + +Suggestions for improving web pages after Rod reading them: + + - slideshow rather than single screen shot + - separate feature list + - explain what a proof script is and what script management buys you + diff --git a/html/oldnews.html b/html/oldnews.html new file mode 100644 index 00000000..89d856c7 --- /dev/null +++ b/html/oldnews.html @@ -0,0 +1,417 @@ +<?php + require('functions.php3'); + small_header("Proof General Old News"); + ?> +<ul> + + +<li><b>19th June 2002</b> +<p> +We plan to release version <b>3.4</b> of Proof General +in August. This update will have several significant +improvements +(notably to the synchronization support for Coq), and also includes +fixes and updates for recent versions of Emacs (notably GNU Emacs 21.x) +and various proof assistants. +<br> +<b>Please, please, please</b> do test some <a +href="develdownload.html">development releases</a> for us in the +meantime and <a href="feedback">report any difficulties</a>, +to help make the next release of Proof General as +robust as possible. Thanks! +</p> +</li> + +<li><b>14th December 2001</b> +<p> +The current <a href="develdownload.html">development release</a> takes +advantage of the new fancy features available in GNU Emacs 21, to add +toolbar support and other features there. As usual, maintaining the +code to work with both Emacs versions is quite troublesome, so bug +reports and patches from users are very welcome. +</p> +</li> + +<li><b>10th September 2001</b> +<p> +<a href="download">Proof General 3.3</a> is released, with +<?php fileshow("ProofGeneral-3.3/CHANGES","new features"); ?> to +increase your proof script editing efficiency. Happy proving! +</p> +</li> +<li><b>1st August 2001</b> +<p> +The past few months have seen a few more improvements and +bug fixes to Proof General: many thanks to those who have +sent us <a href="feedback">useful feedback</a>. +It's time that we made a proper release, so please try +out the <a href="develdownload.html">development release</a> +and help us iron out as many more problems as we can. +<br> +Emacs Lisp and the Emacsen libraries has to be one of the +worst moving target platforms to develop an application on, +so please help us! Once things are looking good, we'll +release PG 3.3. +</p> +<li><b>8th May 2001</b> +<p> +Proof General has had a few quiet improvements since October, which +appear in the current +<a href="develdownload.html">development release</a>. +This version also has some compatibility fixes +for the recent releases of Emacs (20.7) and XEmacs (21.4). +</p> + +<li><b>2nd October 2000</b> +<p> +Proof General 3.2 is released today. Happy proving! +</p> + +<li><b>25th Sep 2000</b> +<p> +Final week of testing for Proof General 3.2. +The last chance to report bugs or request (minor) improvements for this release. +Please help us by trying out the +<a href="develdownload.html">pre-release</a>, especially if you are +relying on an older or non-standard Emacs version. +Also check to see if the new +manuals are useful: now split into +the user manual in +<?php htmlshow("ProofGeneral/doc/ProofGeneral_toc.html","HTML","Proof General manual") ?>, +<?php download_link("ProofGeneral/doc/ProofGeneral.ps.gz", "ps") ?> +or +<?php download_link("ProofGeneral/doc/ProofGeneral.pdf", "pdf") ?>, +and the separate "adapting" manual, in +<?php htmlshow("ProofGeneral/doc/PG-adapting_toc.html","HTML","Adapting Proof General manual") ?>, +<?php download_link("ProofGeneral/doc/PG-adapting.ps.gz", "ps") ?> +or +<?php download_link("ProofGeneral/doc/PG-adapting.pdf", "pdf") ?>. +(Info files are included in the distribution). +</p> +<li><b>14th Sep 2000</b> +<p> +Improvements to web pages. Graphics made smaller, text more concise. +Please <?php hlink("feedback","send me suggestions ","Feedback form")?> +for further improvements. +(I know some pages display poorly in Netscape 4.7x because +of patchy stylesheet support; they appear much better in IE5 +or the rather impressive recent versions of KDE's Konqueror). +</p> +<li><b>28th Aug 2000</b> +<p> +We're starting the testing phase for Proof General 3.2. +It has several new features and improvements. +Please try out the <a href="develdownload.html">pre-release</a> +version, and report any problems to us. Your +feedback is very important because we have no resources available for +serious compatibility testing ourselves. +</p> +<p> +We hope to release 3.2 by the end of September. +</p> +</li> +<li><b>25th May 2000</b> +<p> +Minor patch 3.1.6 released today. This turns off toolbar enablers if +you're running XEmacs on Solaris; because of strange Solaris problems, +buttons are disabled too often there. (You can live without +this part of the patch by customizing the variable +<tt>proof-toolbar-use-button-enablers</tt>). +The patch also removes +the use of an "interval timer" when +<tt>proof-toolbar-use-button-enablers</tt> is off, since a user +reported being unable to start itimers unless +running as root (likely an operating system configuration problem). +Thanks to Markus Wenzel and Pierre Lescanne for reporting problems. +</p> +</li> +<li><b>9th May 2000</b> +<p> +New! For developers, a web-browsable +mirror of the Proof General cvs is available +<a href="http://www.proofgeneral.org/cgi-bin/cvsweb.cgi">here</a>. +</p> +<li><b>5th May 2000</b> +<p> +New! +Proof General <?php fileshow("ProofGeneral/FAQ", "FAQ");?>. +Please send questions or suggestions for inclusion to +<a href="mailto:proofgen@dcs.ed.ac.uk">proofgen@dcs.ed.ac.uk</a>, +thanks. +</p> +<li><b>28th April 2000</b> +<p> +A minor patch to Proof General 3.1 is released today. To check what +version you have, look at the variable <tt>proof-general-version</tt> +set in <tt>proof-site.el</tt>. (It is not recorded in the tar file +name or package version). The current patch, to 3.1.4, was made to +fix a problem with Isabelle and theory file retraction, accidently +introduced in 3.1. See <?php +fileshow("ProofGeneral-3.1-devel/etc/release-log.txt","the developer's +release log"); ?> for details. +NB: This patch was first made on 4th April, but didn't quite solve the +problem. Thanks to Mike Squire for sending a patch to fix the fix. +</p> +<p> +Further improvements are being introduced in the new 3.2 pre-releases, +see the +<a href="develdownload.html">development download</a> page, as usual. +</p> +<li><b>23rd March 2000</b> +<p> +Proof General 3.1 is now available from the +<a href="download">download page</a>. Enjoy! +</p> +</li> +<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/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 +basic feature set for Proof General, the result is still an enormous +improvement over shell interaction. +</p> +<p> +My hope is to entice HOL users so that one of them may improve HOL +Proof General. I don't plan to maintain or seriously improve this +instantiation myself. +</p> +<p> +The HOL support is shipping in the +current <a href="develdownload.html">development release</a>. +</p> +</li> +<li><b>15th February 2000</b> +<p> +There is now a new +<a href="devel">page for developers</a>. +I plan to apply for funding to continue managing the evolution +and development of Proof General, once my own job position +is more secure. +Now is the time to flesh out ideas +for the future! +Check the development page for the +latest proposals. These include some desirable contributions +which could be undertaken as self-contained projects. +</p> +<li><b>9th February 2000</b> +<p> +Countdown to Proof General 3.1 begins. This will be a bug fix releaase. +A few bugs have been fixed in +recent Proof General development releases, one important one is fixing +support for non-mule versions of GNU Emacs (thanks to Pierre Courtieu +for raising it to my attention). I would like to release PG 3.1 next +month so that everyone can benefit. +</p> +<p> +In the meantime, please +<?php + hlink("feedback","report any important problems ","Feedback form")?> +that you would like to see fixed, and consider trying out +the current <a href="devel">development release</a>. +</p> +<li><b>14th December 1999</b> +<p> +I'm pleased to say that Proof General will be demonstrated at +<a href="http://iks.cs.tu-berlin.de/etaps2000/etaps.html">ETAPS 2000</a>. +Here are some draft <a href="papers/pgtalk.pdf">slides</a> for +the presentation +(any <a href="mailto:da@dcs.ed.ac.uk">comments</a> would be welcome). +A presentation of Proof General based on these slides was given at +<a href="http://www.clrc.ac.uk/">Rutherford Appleton Laboratory</a> last week. +</p> +<li><b>26th November 1999</b> +<p> +Proof General 3.0 is released! +</p> +<li><b>17th November 1999</b><br> +<p> +Proof General 3.0 is currently in final testing, and will be released +in a small number of days. Please help me with this by testing the +current <a href="devel">pre-release</a>, so I can iron out as +many bugs as possible before making the release. It's very easy to +install or upgrade Proof General, so it shouldn't be much effort to +test it quickly. Particularly if you're already running an earlier +version. +</p> +<li><b>16th November 1999</b><br> +<p> +New! With Proof General 3.0, adapting to a new prover is easier +than ever before! +It includes an + <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", "example instance ");?> +of Proof General for Isabelle, which +configures the main core of the interface with less than 30 lines of +code. Not bad for getting about 4000 lines worth of code in benefit! +</p> +<li><b>9th November 1999</b><br> +<p> +Isabelle 99 was released last week, and Proof General 3.0 should +be ready for release in the next week or so. In +the meantime, please use the current +<a href="develdownload.html">pre-release</a> +for Isabelle 99. +</p> +<p> +Some recent changes have been made to the support for +<a href="http://x-symbol.sourceforge.net/">X-Symbol</a>, +so that it is easier to turn on and off, and support is now +properly generic. At the moment only Isabelle has +support implemented. +</p> +<li><b>21st October 1999</b><br> + <p> + See what Proof General 3.0 will look like! + The <a href="screenshot.html">screenshot</a> has been updated. + </p> +<li><b>14th October 1999</b><br> + <p> + The next version of Proof General will be 3.0. + </p> + <p> + There have been significant changes to the core of + Proof General and many improvements in the code. + Extra features have been added, and the ones already + there improved upon. Usability has been a particular + focus. Adding new provers has been made easier. + Installation will be made even easier. + All of these changes warrant moving to a major release! + </p> + <p> + Version 3.0 is planned for release in November. + Please test a Version 3.0 pre-release if you can + and report any problems. + </p> +<li><b>12th October 1999</b><br> + <p> + I'm very grateful to + <a href="mailto:courtieu@lri.fr">Pierre Courtieu <courtieu@lri.fr></a> + for offering to help work on Coq Proof General. + <br> + If anyone else in the Coq community would like to assist, please + offer still, + there is plenty to do to add: better recognition of proof scripts, + multiple file management, proof by pointing, etc... + </p> +<li><b>1st October 1999</b><br> + <p> + Recently there has been a flurry of work on the next version of Proof + General. It has quite a number of improvements (see the <?php + fileshow("ProofGeneral/CHANGES","CHANGES"); ?> file), made by myself + and Markus Wenzel. <br> The next version is aimed to coincide + roughly with the release of Isabelle 99. + </p> + <p> + At the moment we <b>urgently need</b> somebody from the Coq world to + maintain and improve Coq Proof General, since Patrick Loiseleur + can no longer work on it. + Support from the Coq community is vital for Proof General to + be a useful tool there. <a href="feedback">Please offer to help</a>, + it needn't be a heavy commitment. + </p> +<li><b>13th September 1999</b><br> + <p> + I've just returned from the + <a href="http://www-sop.inria.fr/types-project/types-sum-school.html">Types Summer School, Giens, France</a> + where Proof General was used for a class of + about 50 students who were learning + Coq, Isabelle, and LEGO. I received + many useful comments and feedback, + which will be + used to improve the next version. + Thanks to everyone who gave suggestions and bug reports + to me, including: + Michael Abbott, + Bernd Grobauer, + Sebastian Skalberg, + Thierry Massart, + Darmalingum Muthiayen. + <br> + </p> +<li><b>27th August 1999</b><br> + <p> + Print pictures from the new + <a href="gallery">gallery</a> + of publicity shots of Proof General! + </p> +<li><b>24th August 1999</b><br> + <p> + Proof General version 2.1 is released. + <br> + Check the <?php fileshow("ProofGeneral-2.1/CHANGES","CHANGES"); ?> file + for a summary of changes since Proof General 2.0. + </p> + <p> + It is recommended that all users upgrade except + those still using Isabelle 98-1. + <br> + Proof General 2.1 supports only the 99 version of Isabelle. + </p> +</li> + +<li><b>24th June 1999</b><br> + <p> + New Proof General web pages go live! + </p> + <p> + The general is now more serious looking. + Appropriate, because there are some serious improvements + in the pipeline... + Before that, we will release Proof General 2.1, + mainly a bug-fix improvement of 2.0. + </p> + <p> + Please explore the new web pages and report any problems + or suggestions to <?php mlink($project_email); ?>. + Please also try out the latest pre-release of Proof General, + this is the final chance to get fixes and tweaks + sorted before 2.1. + </p> +</li> + +<li><b>11th May 1999</b><br> + <p>A new instantiation of Proof General has been added by + <a href="http://www.dur.ac.uk/~dcs1pcc/">Paul Callaghan</a> + for + <a href="http://www.dur.ac.uk/CARG/plastic.html">Plastic</a>, + a new proof assistant based on + Luo's Typed Logical Framework and + implemented in Haskell. + </p> +</li> + +<li><b>16th April 1999</b><br> + <p>A new instantiation of Proof General has been added by + <a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a> + for <a href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar</a>, + a new proof language for Isabelle to be included with Isabelle 99. + </p> +</li> +</ul> +<p> +<i>News items by <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>.</i> +</p> + + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/oldrel.php b/html/oldrel.php new file mode 100644 index 00000000..c48df091 --- /dev/null +++ b/html/oldrel.php @@ -0,0 +1,162 @@ +<?php + require('functions.php3'); + small_header("Previous Releases of Proof General"); + ?> + +<p> +Please note that we do not support these old releases in any way. +</p> + +<h2>Proof General Version 3.3, released 10th September 2001</h2> +<p> +This version of Proof General has been tested +with XEmacs 21.4 and (briefly) with GNU Emacs 20.7 +(it does <b>not</b> support GNU Emacs 21.x). +It supports Coq version 7.x, LEGO version 1.3.1 and +Isabelle2002. +</p> + +<ul> + <li> gzip'ed tar file: + <?php download_link("ProofGeneral-3.3.tar.gz") ?>, + <br> + or the same thing in a zip file: + <?php download_link("ProofGeneral-3.3.zip") ?>, + </li> + <li> Linux RPM package: + <?php download_link("ProofGeneral-3.2-1.noarch.rpm") ?> + </li> +</ul> +<p> +Check the <?php fileshow("ProofGeneral-3.3/CHANGES","CHANGES"); ?> file +for a summary of changes since version 3.2. +</p> + + +<h2>Proof General Version 3.2, released 2nd October 2000</h2> +<p> +This version of Proof General has been tested +with XEmacs 21.1 and (briefly) with GNU Emacs 20.7. +It supports Coq version 6.3, LEGO version 1.3.1 and +Isabelle99-1. +</p> + +<ul> + <li> gzip'ed tar file: + <?php download_link("ProofGeneral-3.2.tar.gz") ?>, + <br> + or the same thing in a zip file: + <?php download_link("ProofGeneral-3.2.zip") ?>, + </li> + <li> Linux RPM package: + <?php download_link("ProofGeneral-3.2-1.noarch.rpm") ?> + <br> + Also a + <?php download_link("ProofGeneral-3.2-1.src.rpm", + "source RPM") ?>. + </li> +</ul> +<p> +Check the <?php fileshow("ProofGeneral-3.2/CHANGES","CHANGES"); ?> file +for a summary of changes since version 3.1. +</p> + +<h2>Proof General Version 3.1, released 23rd March 2000</h2> + +<p> +This version of Proof General has been tested +with XEmacs 21.1 and GNU Emacs 20.4. +It supports Coq version 6.3, LEGO version 1.3.1 and +Isabelle99. +</p> + +<ul> + <li> gzip'ed tar file: + <?php download_link("ProofGeneral-3.1.tar.gz") ?> + <br>or zip file: + <?php download_link("ProofGeneral-3.1.zip") ?>, + </li> + <li> RPM package: + <?php download_link("ProofGeneral-3.1-1.noarch.rpm") ?> + <br> + The + <?php download_link("ProofGeneral-3.1-1.src.rpm", + "source RPM") ?>. + </li> +</ul> +<p> +Check the <?php fileshow("ProofGeneral-3.1/CHANGES","CHANGES"); ?> file +for a summary of changes since version 3.0. +</p> + + + +<h2>Proof General Version 3.0, released 26th November 1999</h2> + +<p> +This version of Proof General has been tested +with XEmacs 20.4, XEmacs 21.1.8 and GNU Emacs 20.5.<br> +It supports Coq version 6.3, LEGO version 1.3.1 and Isabelle99. +</p> +<ul> + <li> gzip'ed tar file: + <?php download_link("ProofGeneral-3.0.tar.gz") ?> + </li> + <li> Linux RPM package: + <?php download_link("ProofGeneral-3.0-1.noarch.rpm") ?> + <br> + The source RPM is + <?php download_link("ProofGeneral-3.0-1.noarch.rpm","here") ?>. + </li> +</ul> +<p> +Check the <?php fileshow("ProofGeneral-3.0/CHANGES","CHANGES"); ?> file +for a summary of changes since version 2.1. +</p> + + + +<h2>Proof General Version 2.1, released 24th August 1999</h2> + +<p> +This version of Proof General has been tested +with XEmacs 20.4, XEmacs 21 and GNU Emacs 20.3.<br> +It supports Coq version 6.3, LEGO version 1.3.1 and +some pre-release versions of Isabelle version 99. +<ul> + <li> gzip'ed tar file: + <?php download_link("ProofGeneral-2.1.tar.gz") ?> + </li> + <li> Linux RPM package: + <?php download_link("ProofGeneral-2.1-1.noarch.rpm") ?> + <br> + The source RPM is + <?php download_link("ProofGeneral-2.1-1.noarch.rpm","here") ?>. + </li> +</ul> + + +<h2>Proof General Version 2.0, released 16th December 1998</h2> + +<p> +This version of Proof General has been tested +with XEmacs 20.4 and GNU Emacs 20.2, 20.3.<br> +It supports Coq version 6.2, LEGO version 1.3.1, and +Isabelle version 98-1.<br> +</p> +<ul> + <li> gzip'ed tar file: + <?php download_link("ProofGeneral-2.0.tar.gz") ?> + </li> + <li> Linux RPM package: + <?php download_link("ProofGeneral-2.0-1.noarch.rpm") ?> + <br> + The source RPM is + <?php download_link("ProofGeneral-2.0-1.noarch.rpm","here") ?>. + </li> +</ul> + +<?php + click_to_go_back(); + footer(); +?> diff --git a/html/papers/pgoutline.pdf b/html/papers/pgoutline.pdf Binary files differnew file mode 100644 index 00000000..e712bade --- /dev/null +++ b/html/papers/pgoutline.pdf diff --git a/html/papers/pgoutline.ps.gz b/html/papers/pgoutline.ps.gz Binary files differnew file mode 100644 index 00000000..632f431a --- /dev/null +++ b/html/papers/pgoutline.ps.gz diff --git a/html/papers/pgtalk.pdf b/html/papers/pgtalk.pdf Binary files differnew file mode 100644 index 00000000..18989c20 --- /dev/null +++ b/html/papers/pgtalk.pdf diff --git a/html/projects.html b/html/projects.html new file mode 100644 index 00000000..9f1c274d --- /dev/null +++ b/html/projects.html @@ -0,0 +1,97 @@ +<?php + require('functions.php3'); + small_header("Proof General Projects"); + ?> + +<p> +Here are some proposals for projects connected to Proof General. +</p> +<p> +The projects are designed as fairly self-contained contributions, +involving code development and possibly a portion of supporting +research. They would be ideal projects for interested students +or researchers. +</p> +<p> +The projects are divided into those which are specific to Proof +General, and those which would be useful more widely and do not depend +on Proof General. For more information on a project, click on its +title. +</p> + +<h2>A. Projects involving Proof General</h2> +<ol> +<li><?php pgproject("coqpbp","Proof-by-pointing support for Coq") ?></li> +<li><?php pgproject("coqfile","Multiple file handling support for Coq") ?></li> +<li><?php pgproject("isapbp","Proof-by-pointing support for Isabelle") ?></li> +<li><?php pgproject("outline","Integrating block-structured development and outline mode") ?></li> +<li><?php pgproject("thybrowse","A Generic Theory Browser") ?></li> +<li><?php pgproject("pgml","Specification and tools for PGML") ?></li> +<li><?php pgproject("pgip","A New Protocol for Interactive Proof in Proof General") ?></li> +<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> +<!-- <li><?php pgproject("pgkit","Proof General Kit (LFCS summer studentship)") ?></li> --> +</ol> + +<h2>B. Projects not directly involving Proof General</h2> +<ol> +<li><?php pgproject("mm","Multiplexed Modes for Emacs") ?></li> +<li><?php pgproject("scrgen","Script General") ?></li> +<!-- <li><?php pgproject("corba","An Experimental CORBA binding for ML") ?></li> --> +<!-- <li><?php pgproject("reelcase","A ClearCase-like Configuration Management tool for Linux") ?></li> --> +</ol> + +<p> +Some projects involve Emacs Lisp. This is the embedded programming +language inside Emacs. It is very easy to learn, since it is small, +has a good manual, and has an interactive interpreter. It is easy to +use, not least because of its <i>self-documenting</i> nature: each +variable or function is compiled together with documentation of its +purpose. (Other languages would do well to follow this). It also +has a powerful source-level debugger, <i>edebug</i>. +</p> + +<!-- template for project pages --> +<!-- <h2> </h2> --> +<!-- <p> --> +<!-- </p> --> +<!-- <p> --> +<!-- <b>Skills:</b> --> +<!-- </p><p> --> +<!-- <b>Proposer:</b> --> +<!-- <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>. --> +<!-- </p> --> + +<p> +If you are interested in working on any of these projects, +feel free to discuss with the project proposer or on the +<a href="devel#develmail">developer's mailing list</a>. +</p> + +<p> +If you would like to use any of these ideas as a formal project +proposal for students at your institution, please feel free +but do <?php hlink("feedback","let us know ","Feedback form")?> +if some work is begun, to help coordinate efforts. +NB: the proposer of the project does not guarantee to be available for +formal supervision or intensive help with the project (but it may be +possible to find somebody else to do that). +</p> + +<p> +If you would like to submit a project proposal +for an improvement or extension of Proof General, +please send an email or write a description on the +<?php hlink("feedback","web feedback form","Feedback form")?>. +Projects should be significant contributions rather than +incremental improvements (although we welcome the suggestion of those +too). +</p> + + +<?php + click_to_go_back(); + footer(); +?> 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ü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> diff --git a/html/proofgen.css b/html/proofgen.css new file mode 100644 index 00000000..2cd91335 --- /dev/null +++ b/html/proofgen.css @@ -0,0 +1,186 @@ +/* Style sheet for the Proof General web pages. + * David Aspinall, June 1999. + * proofgen.css,v 4.0 2000/03/13 07:36:57 da Exp + */ + +body{ + font-family: Verdana, Arial, sans-serif; /* font for the doc body */ + background: #2D1D03; /* background brown */ + background-image: + url(images/canvaswallpaper.jpg); + background-attachment: fixed; /* background shouldn't scroll */ + color: #FFFFFF; /* text colour is white */ +} +p{ + font-family: Verdana, Arial, sans-serif; /* Netscape is picky, */ + color: #FFFFFF; /* so we must set every tag */ +} +pre{ + font-family: LucidaTypewriter, monospace; + color: #FFFFFF; +} +h1{ + font-family: Verdana, Arial, sans-serif; + color: #FFFFFF; + font-size: large; + font-weight: bold; +} +h2{ + font-family: Verdana, Arial, sans-serif; + font-size: medium; + font-weight: bold; + color: #FFFFD0; + padding: 2px 4px 4px 4px; + background: #7D4D33; +} +h3{ + font-family: Verdana, Arial, sans-serif; + font-size: medium; + padding: 2px 2px 2px 2px; + margin-right: 10%; + background: #6D3D43; + 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; +} + +address{ + font-family: Verdana, Arial, sans-serif; + font-size: small; /* "smaller" is better on IE */ + color: #FFFFFF; /* but varies randomly in NN */ +} + +select { + font-family: Verdana, Arial, sans-serif; + font-size: 100%; + background: #2D1D03; + color: #FFFFFF; +} + +textarea,input { + font-family: Verdana, Arial, sans-serif; + font-size: 100%; + background: #4D2D23; + color: #FFFFFF; +} + +input[type=submit],input[type=reset],input[type=Submit] { + font-family: Verdana, Arial, sans-serif; + font-size: 80%; + padding-top: 0px; + padding-bottom: 0px; + background: #401010; +} + +#button:active{ + background: #402020; +} + +dl,ul,dir,li{ + font-family: Verdana, Arial, sans-serif; + color: #FFFFFF; +} + +dt{ font-style: italic; + padding: 2px 2px 2px 2px; + margin-left: 20px; + margin-right: 20px; + background: #6D3D43; +} + +table{ + font-family: Verdana, Arial, sans-serif; + color: #FFFFFF; +} + +table.menubar{ + font-family: Verdana, Arial, sans-serif; + font-size: smaller; + color: #FFFFFF; +} + + + + +td,tr{ + font-family: Verdana, Arial, sans-serif; +/* background-color: #2D1D03; */ + color: #FFFFFF; +} + +/* Link Elements */ +a:link,a:visited{ /* visited appears same */ + font-family: Verdana, Arial, sans-serif; + text-decoration: none; /* Remove the underline */ + color: #FFD820; +} + +/* hover is IE specific nasty but nice */ +a:active,a:hover{ + font-family: Verdana, Arial, sans-serif; + text-decoration: underline; /* Underline on mouse over */ + color: #FFF030; /* Brighter colour too */ +} + + +pre{ + background: #2D1D03; +} + +/* Specifics */ + +p.nb{ + font-size: smaller; + font-style: italic; +} + +/* These bits for Mailman pages for mailing lists */ +TD.head1old { + font-family: Verdana, Arial, sans-serif; + text-align: center; + color: #FFFFFF; + font-weight: bold; + font-size: 110%; +} +td.head1{ + font-family: Verdana, Arial, sans-serif; + font-weight: bold; + font-size: 110%; + text-align: center; + color: #FFFFFF; +} +td.head2{ + font-family: Verdana, Arial, sans-serif; + font-size: 100%; + font-weight: bold; + color: #FFFFD0; + padding: 2px 4px 4px 4px; + background: #7D4D33; +} +td.head3{ + font-family: Verdana, Arial, sans-serif; + padding: 2px 2px 2px 2px; + margin-right: 10%; + background: #6D3D43; + font-size: 80%; + color: #FFFFD0; +} +td.head4{ + font-family: Verdana, Arial, sans-serif; + font-size: 100%; + font-weight: bold; + color: #FFD0D0; +} diff --git a/html/register b/html/register new file mode 100644 index 00000000..515d44bd --- /dev/null +++ b/html/register @@ -0,0 +1,109 @@ +<?php +## +## Proof General registration form. +## +## David Aspinall, June 1999. +## +## $Id$ +## + require('functions.php3'); + + $failure= ($argv[0]=="submit" && ($name=="" || $email=="" || $site=="")); + + if ($argv[0] !="submit" || $failure): +### +### Registration form +### + small_header("Proof General Registration"); + + if ($failure): +?> +<p> + Your registration form was incomplete. Please fill in all + the fields, thank-you! +</p> +<?php else: + $mailinglist=true +?> +<p> +Please register your download using the short form below. +<br> +The information provided will only be used to help +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 <a href="download#prereq">the download page</a>. +</p> +<?php endif; ?> +<h2>Registration Form</h2> +<form method=post action="<?php print $PHP_SELF . "?submit"; ?>"> +<table width="600" border="0" cellspacing="2" cellpadding="0"> +<tr> + <td width="30%">Your name:</td> + <td width="70%"><input type=text name="name" size="40" + value="<?php echo $name;?>"></td> +</tr> +<tr> + <td width="30%">Email address:</td> + <td width="70%"><input type=text name="email" size="40" + value="<?php echo $email;?>"></td> +</tr> +<tr> + <td width="30%">Your site name:</td> + <td width="70%"><input type=text name="site" size="40" + value="<?php echo $site;?>"></td> +</tr> +<tr> + <td width="30%"><input type=checkbox name="mailinglist" + <?php if ($mailinglist) print "checked"; ?>></td> + <td width="70%">Please add me to the mailing list.</td> +</table> +<br> +<input type=submit value="Send form"> +</form> +<?php + click_to_go_back(); + footer(); + else: +## +## Process registration +## + small_header("Registration Form Sent"); + + + $message = "Registration form for using Proof General" + . "\nName:\t\t " . $name + . "\nEmail:\t\t " . $email + . "\nSite:\t\t " . $site + . "\nSubmitted:\t" . date("h:ia D jS F Y"); + mail("proofgen@dcs.ed.ac.uk", + "[Registration form from ~proofgen]", + $message); + + print "<p>Dear " . $name . ",</p>\n"; + print "<p>"; + print "Thank you for filling in the form. Your registration has been sent.<br>"; + + /* Next bit duplicated in mailinglist.html. + Could be a function in functions.php3 */ + + if ($mailinglist) { + $message = "subscribe address=$email"; + mail("proofgeneral-request@informatics.ed.ac.uk", + "[Web form from Proof General]", + $message, + "Reply-To: " . $email . "\nFrom: " . $email); + print "A subscription request has been sent for the Proof General mailing list.<br>"; + } + print "</p>\n<p>"; + + print "<p>\nClick "; + print "<a href=\"download#prereq\">here</a>"; + print " to return to the download page.<br></p>\n"; + click_to_go_back(); + + footer(); + endif; +?> + diff --git a/html/register.html b/html/register.html new file mode 100644 index 00000000..097d8441 --- /dev/null +++ b/html/register.html @@ -0,0 +1,110 @@ +<?php +## +## Proof General registration form. +## +## David Aspinall, June 1999. +## +## $Id$ +## + require('functions.php3'); + + $failure= ($argv[0]=="submit" && ($name=="" || $email=="" || $site=="")); + + if ($argv[0] !="submit" || $failure): +### +### Registration form +### + small_header("Proof General Registration"); + + if ($failure): +?> +<p> + Your registration form was incomplete. Please fill in all + the fields, thank-you! +</p> +<?php else: + $mailinglist=true +?> +<p> +Please register your download using the short form below. +<br> +The information provided will only be used to help +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 <a href="download#prereq">the download page</a>. +</p> +<?php endif; ?> +<h2>Registration Form</h2> +<form method=post action="<?php print $PHP_SELF . "?submit"; ?>"> +<table width="300" border="0" cellspacing="2" cellpadding="0"> +<tr> + <td width="30%">Your name:</td> + <td width="70%"><input type=text name="name" size="40" + value="<?php echo $name;?>"></td> +</tr> +<tr> + <td width="30%">Email address:</td> + <td width="70%"><input type=text name="email" size="40" + value="<?php echo $email;?>"></td> +</tr> +<tr> + <td width="30%">Site name:</td> + <td width="70%"><input type=text name="site" size="40" + value="<?php echo $site;?>"></td> +</tr> +<tr> + <td width="30%"><input type=checkbox name="mailinglist" + <?php if ($mailinglist) print "checked"; ?>></td> + <td width="70%">Please add me to the mailing list.</td> +</table> +<input type=submit value="Send form"> +</form> +<p> +</p> +<?php + click_to_go_back(); + footer(); + else: +## +## Process registration +## + small_header("Registration Form Sent"); + + + $message = "Registration form for using Proof General" + . "\nName:\t\t " . $name + . "\nEmail:\t\t " . $email + . "\nSite:\t\t " . $site + . "\nSubmitted:\t" . date("h:ia D jS F Y"); + mail("proofgen@dcs.ed.ac.uk", + "[Registration form from ~proofgen]", + $message); + + print "<p>Dear " . $name . ",</p>\n"; + print "<p>"; + print "Thank you for filling in the form. Your registration has been sent.<br>"; + + /* Next bit duplicated in mailinglist.html. + Could be a function in functions.php3 */ + + if ($mailinglist) { + $message = "subscribe proofgeneral"; + mail("majordomo@dcs.ed.ac.uk", + "[Web form from ~proofgen]", + $message, + "Reply-To: " . $email . "\nFrom: " . $email); + print "Your name has been added to the Proof General mailing list.<br>"; + } + print "</p>\n<p>"; + + print "<p>\nClick "; + print "<a href=\"download#prereq\">here</a>"; + print " to return to the download page.<br></p>\n"; + click_to_go_back(); + + footer(); + endif; +?> + diff --git a/html/screenshot b/html/screenshot new file mode 100644 index 00000000..bba013ba --- /dev/null +++ b/html/screenshot @@ -0,0 +1,8 @@ +<?php require('functions.php3'); ?> +<?php include('head.html'); ?> +<?php + include('header.html'); + include($WANTED . '.html'); + footer(); +?> + diff --git a/html/screenshot.html b/html/screenshot.html new file mode 100644 index 00000000..ffc9e8a4 --- /dev/null +++ b/html/screenshot.html @@ -0,0 +1,115 @@ +<p> +Here are some screenshots of Proof General 3.0 running with +different theorem provers. To see the full-size version +of a picture, click on its thumbnail. +</p> + +<!-- FIXME: update pictures. Fix vertical centering of screenshots. --> + +<table width="80%"> +<tr> +<td width="200"> +<a href="images/pg-lego-screenshot.png"> +<img src="images/pg-lego-thumb.png" alt="LEGO Proof General" width=128 height=109 border=0> +</a> +</td> +<td> +<p><font size="-1"> +Building a simple proof in LEGO with proof-by-pointing. +<br> +The top half of the window displays the proof script. +The bottom displays the output from LEGO at each +stage of the proof. Here, it shows +the current subgoals to be solved. +The part of the proof already processed by LEGO +has a blue background. +<br> +Clicking on terms in the subgoals list generates +commands which are added to the proof script. +</font></p> +<br> +</td></tr> + +<tr> +<td width="200"> +<a href="images/pg-coq-screenshot.png"> +<img src="images/pg-coq-thumb.png" alt="Coq Proof General" width=153 height=115 border=0> +</a> +</td> +<td> +<p><font size="-1"> +Coq Proof General running in multiple frame mode, +full screen shot (1024x768). +<br> +There are separate windows on the screen +for the script, goals, and response buffers. +In this picture, you can see Proof General's +indication that Coq is processing the +induction step, because the background of +the proof step is pink. It will become +blue when Coq finishes that step. +</font></p> +<br> +</td></tr> + +<tr> +<td width="200"> +<a href="images/pg-isa-screenshot.png"> +<img src="images/pg-isa-thumb.png" alt="Isabelle Proof General" width=150 height=142 border=0> +</a> +</td> +<td> +<p><font size="-1"> +Replaying a domain theory proof in Isabelle's HOLCF logic. +<br> +In Isabelle, theory files as well as ML files are coloured. +Proof General has some functions for processing and +undoing theory files, but most operations it provides +are for writing proof scripts in ML files. +<br> +Isabelle supports input and output in tokens which +display as symbols using the +<a href="http://x-symbol.sourceforge.net/">X-Symbol</a> +package in conjunction with Proof General. +Here you can see some symbols in Isabelle's output. +</font></p> +<br> +</td></tr> + +<tr> +<td width="200"> +<a href="images/pg-isar-screenshot.png"> +<img src="images/pg-isar-thumb.png" alt="Isabelle/Isar Proof General" width=150 height=142 border=0> +</a> +</td> +<td> +<p><font size="-1"> +Replaying a proof in Isar, Isabelle's declarative proof language +developed by Markus Wenzel. +</font></p> +<br> +</td></tr> + +<tr> +<td width="200"> +<a href="images/pg-lego-console.png"> +<img src="images/pg-lego-console-thumb.png" alt="LEGO Proof General (console)" width=174 height=65 border=0> +</a> +</td> +<td> +<p><font size="-1"> +LEGO Proof General running in plain console mode. +<br> +This shows that you can run Proof General even if sometimes +you need to use a plain tty or xterminal. Of course, the +graphical features are reduced! +</font></p> +<br> +</td> +</tr> +</table> + +<p> +For more pictures, see the Proof General <a href="gallery">gallery</a>. +</p> + diff --git a/html/smallheader.html b/html/smallheader.html new file mode 100644 index 00000000..ade4e6dd --- /dev/null +++ b/html/smallheader.html @@ -0,0 +1,8 @@ +<table width="80%"> +<tr> +<td width="15%"> +<a href=""> +<img src="images/PG-small.jpg" align=top width=37 height=50 border=0 alt="Proof General Home"> +</a> +</td> +<td width="85%"> diff --git a/html/smallpage.html b/html/smallpage.html new file mode 100644 index 00000000..64f538a3 --- /dev/null +++ b/html/smallpage.html @@ -0,0 +1,6 @@ +<?php + require('functions.php3'); + small_header($title); + include($file); + footer(); +?> diff --git a/html/smallpage.php b/html/smallpage.php new file mode 100644 index 00000000..ef165c6d --- /dev/null +++ b/html/smallpage.php @@ -0,0 +1,12 @@ +<?php + require('functions.php3'); + small_header($title); + if (substr($file,0,1)=="." or + substr($file,0,1)=="/" or + substr($file,0,1)=="~") { + print "Sorry, can't show you that file!\n"; + } else { + include($file); + } + footer(); +?> diff --git a/html/userman b/html/userman new file mode 100644 index 00000000..e8ccc072 --- /dev/null +++ b/html/userman @@ -0,0 +1,3 @@ +<?php require('functions.php3'); + hack_html("ProofGeneral/doc/ProofGeneral_toc.html","Proof General user manual","userman"); +?> |
