From 670761dd6bd6321d65beeacdc81d68c0a2ebe92b Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 13 Mar 2000 05:14:23 +0000 Subject: Updated web pages. --- html/devel.phtml | 25 +++++++-- html/develdownload.phtml | 45 ++++++++-------- html/download.phtml | 40 ++++++++------ html/elispmarkup.php3 | 134 +++++++++++++++++++++++++++++++++++++++++++++ html/features.phtml | 18 ++++--- html/fileshow.phtml | 8 ++- html/main.phtml | 33 +++++++----- html/mission.phtml | 138 +++++++++++++++++++++++++++++++++++++++++++++++ html/news.phtml | 14 ++++- html/projects/hol.html | 7 ++- html/proofgen.css | 13 +++++ 11 files changed, 404 insertions(+), 71 deletions(-) create mode 100644 html/elispmarkup.php3 create mode 100644 html/mission.phtml (limited to 'html') diff --git a/html/devel.phtml b/html/devel.phtml index fa9dc1ed..75c5af17 100644 --- a/html/devel.phtml +++ b/html/devel.phtml @@ -46,18 +46,33 @@ for Proof General. + + + + + + + + + + + + + +For install instructions, see +the . + +

+

+

+

+ +

Complete Archive of ProofGeneral-3.1pre000310 for Developers

@@ -64,31 +73,19 @@ What's the difference from the user's pre-release above? The complete archive also includes:

Note: there are no pre-built documentation files in the developer's diff --git a/html/download.phtml b/html/download.phtml index 3078bff5..4d692215 100644 --- a/html/download.phtml +++ b/html/download.phtml @@ -57,7 +57,7 @@ of XEmacs ftp mirror may help).
-or version 20.2 or later (20.4 recommended) of the much poorer +or version 20.2 or later (20.5 recommended) of the much poorer FSF GNU Emacs.
Both Emacsen are available for a variety of platforms, including @@ -85,21 +85,21 @@ package. for installation notes.
X-Symbol presently only works with XEmacs. -

  • -For FSF Emacs, a version of func-menu.el to get -. -
    Unfortunately I can't find a version of this that -works with current FSF Emacs releases. I'd be grateful -for a pointer to one. -
    -(The package -imenu.el may be a suitable replacement, -and it ships with both Emacsen. Perhaps -somebody could contribute patches to use that -instead of func-menu). + + + + + + + + + + + +

    -All components mentioned are distributed under the GPL license. +All components mentioned above are distributed under the GPL license.



    @@ -150,15 +150,21 @@ Check the file for a summary of changes since version 2.1.

    Check the latest file -before reporting problems. If you find a problem not mentioned -there, please +(also + + + + +) +before reporting problems. If you find a problem not already mentioned, +please .



    -

    Easy installation!

    +

    Easy installation!

    To use Proof General, simply unpack the sources with

    diff --git a/html/elispmarkup.php3 b/html/elispmarkup.php3 new file mode 100644 index 00000000..a18586c9 --- /dev/null +++ b/html/elispmarkup.php3 @@ -0,0 +1,134 @@ +" . $text . "\n"; +} + +// FIXME: this is a nonsense really. Might be okay if it +// used dynamic HTML but it's too much of a faff at the moment. +// Also, we should use the tree structure properly and keep a stack! + +function outline_markup($filename,$thispage,$expanded) { + if ($title=="") { $title=$filename; }; + $outline = false; + $file = file($filename); + $i = 0; + $level=0; + $headingno=0; + /* Now parse file, watching for outline headers */ + for (;$i < count($file);$i++) { + $line = $file[$i]; + // HTML escapes + $line = htmlentities($line); + // Anchors for URLs + $line = ereg_replace("((http://|mailto:)[-a-zA-Z0-9\.~/_@]+)","\\1",$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 "

    "; + print "This is a flattened outline file: click on a title to hide/reveal the leaf underneath it."; + print "
    Click "; + print "here to show body, or "; + print "here to hide all."; + print "

    \n"; + } elseif ($outline) { + if (ereg("^ *\n",$line)) { + // if (!newpara) { print "

    \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 "

    \n"; } + $headingno++; + $level=$newlevel; + $text="$heading[2]"; + link_toggle($headingno,$text,$thispage,$filename,$expanded); + } elseif (isexpanded($headingno,$expanded)) { + if ($newpara && $level==0) { print "

    \n"; } + print $line; + $newpara=false; + $level=0; + } + } else { + print $line; + } + } +} + +// +// For browsing source. Unfinished. +// + +function elisp_markup($filename,$thispage,$title="") { + if ($title=="") { $title=$filename; }; + $file = file($filename); + $i = 0; + $level=0; + $headingno=0; + /* Now parse file, watching for outline headers */ + for (;$i < count($file);$i++) { + $line = $file[$i]; + // HTML escapes + $line = htmlentities($line); + // Anchors for URLs + $line = ereg_replace("((http://|mailto:)[-a-zA-Z0-9\.~/_@]+)","\\1",$line); + // Font-lock equivalents... + // 1. comments + $line = ereg_replace("(;+.*\n)", + "

    \\1
    ", + $line); + // 2. keywords + // FIXME: this inserts CR's. + $line = ereg_replace("^\(def(macro|un|var|custom|const|group)", + "(
    def\\1
    ", + $line); + // FIXME: add hrefs for keywords, looking up in TAGS file. + // FIXME: add line numbers + // FIXME: parse strings + print $line; + } +} diff --git a/html/features.phtml b/html/features.phtml index c2c6dc89..89ad9fd1 100644 --- a/html/features.phtml +++ b/html/features.phtml @@ -67,10 +67,11 @@ If not, read on…
    Script management in Proof General can work across many script - files. When a script is visited in the editor, it is locked - (coloured) to reflect whether the proof assistant has loaded it in - this session. When a file is unlocked, all of the files which - depend on it are automatically unlocked too. + files, integrating with the file handling of + the proof assistant. When a script is visited in the editor, it + is locked (coloured) to reflect whether the proof assistant has + loaded it in this session. When a file is unlocked, all of the + files which depend on it are automatically unlocked too.

    Dependencies between script files are either communicated from the proof assistant to Proof General, or maintained automatically by @@ -128,8 +129,9 @@ If not, read on… Instead of seeing "not P", you see "¬ P", instead of "a * b", you see "a × b", etc.
    - [the examples above are simple so they will work on most browsers - without needing images] + (Those examples are simple so they will work on most browsers + without needing images, see the + screenshots for more examples.)

    @@ -153,8 +155,8 @@ If not, read on…
    Tags are an editing feature which allow you to quickly locate the definition or declaration of a particular identifier. Proof General - is supplied with utilities to make tag indexes for Emacs, for the - proof assistants LEGO and Coq. This makes it easy to quickly access + is supplied with utilities to make tag indexes for Emacs. + This makes it easy to quickly access definitions from a standard library, for example, and in large proof developments split across multiple files. diff --git a/html/fileshow.phtml b/html/fileshow.phtml index 6e984bdf..741ef556 100644 --- a/html/fileshow.phtml +++ b/html/fileshow.phtml @@ -1,7 +1,9 @@ \n"; @@ -10,8 +12,10 @@ substr($filename,0,1)=="/" or substr($filename,0,1)=="~") { print "Sorry, can't show you that file!\n"; - } else { - markup_plain_text($filename); + } elseif (substr($filename,-3)==".el") { + elisp_markup($filename,"fileshow.phtml"); + else { + outline_markup($filename,"fileshow.phtml",$expanded); } print "\n"; print "
    "; diff --git a/html/main.phtml b/html/main.phtml index e6d9f997..5c0a3068 100644 --- a/html/main.phtml +++ b/html/main.phtml @@ -16,6 +16,15 @@ For detailed version numbers, check the

    +

    +To read more about what features Proof General +provides, +. +
    +To see what Proof General looks like in use, have a look at these +screenshots. +

    +

    Proof General is ready-customized for several proof assistants, including: @@ -28,7 +37,7 @@ including: "\"Coq","The Coq Home Page") ?> - Coq Proof General for + for
    @@ -47,7 +56,7 @@ including: "\"LEGO", "The LEGO Home Page") ?> - LEGO Proof General for + for
    @@ -69,7 +78,7 @@ including: "\"Isabelle", "The Isabelle Home Page"); ?> - Isabelle Proof General for + for
    @@ -78,7 +87,7 @@ including: David Aspinall.
    Additional maintainance, support for - Isabelle/Isar + by Markus Wenzel. @@ -86,6 +95,13 @@ including:

    +There is also a preliminary version of +, for +HOL98. +We are seeking a volunteer from the HOL community to support +and improve this (perhaps also supporting other HOL variants). +

    +

    Proof General is ready to be customized to new proof assistants.
    It can be -

    -To read more about what features Proof General -provides, -. -
    -To see what Proof General looks like in use, have a look at these -screenshots. -

    -

    You can download Proof General diff --git a/html/mission.phtml b/html/mission.phtml new file mode 100644 index 00000000..00f7b60f --- /dev/null +++ b/html/mission.phtml @@ -0,0 +1,138 @@ + + +

    +

    Mission Statement

    +

    Proof General Developers

    +

    March 2000

    +
    + +

    +We seek to provide an interface suite for helping users interact with +proof assistants. +

    + +

    +Our approach is based on these principles: +

    +

    +

    +Above all, we take a pragmatic approach to constructing +interfaces. Our primary aim is to provide a tool which is +immediately useful for proof engineering, rather than +to provide publications by conducting research in +human-computer interaction. +

    +

    +This aim means that we harness a range of +proven techniques +reimplemented in our generic system. +Nevertheless, by the act of constructing Proof General, we do invent +and incorporate some novel advances which +contribute to research in the field. +

    + +
    +

    +

    +

    Footnotes and elaboration

    + +
    + +
    +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 proof +script, which is a file containing a user-level representation +of the proof or how it was constructed. +
    + +
    +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. +
    + +
    +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. +
    + +
    +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. +
    + +
    +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. +
    + +
    +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. +
    + +
    +Amongst other features, Proof General currently includes + +and +, +both championed in +Projet CROAP. +
    + +
    +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 +. +
    +
    + + + diff --git a/html/news.phtml b/html/news.phtml index 9131d56b..579c424c 100644 --- a/html/news.phtml +++ b/html/news.phtml @@ -6,15 +6,26 @@