-Have you any questions, comments, or suggestions about Proof General?
-
-Send us a message using this form
-or by email to
-.
-
-Receive announcements and discuss Proof General on
-our mailing
-list.
-
-The forefather of Proof General was LEGO mode, begun in 1994 at the LFCS by Thomas Kleymann. LEGO -mode was an Emacs-based front end for LEGO similar to David Aspinall's -Isamode, -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 -front page. -
--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 - -EPSRC, - - -the EC, -and the LFCS. -
- -
-David Aspinall designed the web pages and graphics for Proof General.
-
-Check the gallery for more publicity
-pictures!
-
-For more on the history of the development of -the Proof General program, see the - -
- - diff --git a/html/adaptingman b/html/adaptingman deleted file mode 100644 index 74a3152c..00000000 --- a/html/adaptingman +++ /dev/null @@ -1,3 +0,0 @@ - diff --git a/html/components b/html/components deleted file mode 100644 index 7f600582..00000000 --- a/html/components +++ /dev/null @@ -1,5 +0,0 @@ - - diff --git a/html/components.html b/html/components.html deleted file mode 100644 index 6d6a73a2..00000000 --- a/html/components.html +++ /dev/null @@ -1,72 +0,0 @@ - - -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. -
- -As usual with free software, these programs -come with no guarantees of any sort. -Nonetheless, please contact us with -any comments, suggestions, or problems. -
- --Spans are an abstraction of XEmacs extents used to help -bridge the gulf between GNU Emacs and XEmacs. In GNU Emacs, spans are -implemented using overlays. -
--The library consists of three Emacs lisp files, -
-See the files for further documentation, and -section 12.1 -of the Proof General adapting manual -for more details. -
- - --This package generates Texinfo source -fragments from Emacs - -documentation strings 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 javadoc for Emacs -Lisp, except that you must write a skeleton texi file which -contains magic comments mentioning the function or variable names you -want documented.
The package consists of one file:
which contains documentation and usage hints. For an extensive -example of it's use, see the source for the PG adapting manual. - -
-Proof General follows an open development method.
-
-We encourage code contributions, suggestions, and bug reports, from all
-users.
-
- cvs -d :pserver:anon@cvs.inf.ed.ac.uk:/disk/cvs/proofgen login --and use the password anon. Then you can check out -the CVS with: -
- cvs -d :pserver:anon@cvs.inf.ed.ac.uk:/disk/cvs/proofgen checkout ProofGeneral --For more information, see the file etc/cvs-tips.txt in the -repository. (If you want to be an "official" developer and -have write access to the CVS repository, -ask here first). -
-We have a mailing list for developers, at
-proofgeneral-devel@inf.ed.ac.uk.
-
-Posting is restricted to list members.
-To subscribe (or unsubscribe),
-visit
-this
-web page.
-
-Below is the latest pre-release of Proof General, -made available for those who wish to test the latest features or bug -fixes. For developers, this release is also available as a -complete CVS snapshot (further below), which -includes files not needed for the running program. -
--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. -
--Please register if you haven't done so already. -
- - - --The manual included with the pre-release may be -updated from that of the -last stable release. -
--Here is the pre-release documentation: the user manual in -, - -or -, -and the adapting manual, in -, - -or -. -
- - - --Check the - - file - -for a summary of changes since the last stable -version, and notes about work-in-progress.
-| gzip'ed tar file | - -- |
| zip file | -- |
| RPM package | -- |
| individual files | -http access to files in development release - |
-Emacs versions: -This version has been tested with XEmacs version 21.4.12 and with GNU -Emacs 21.2.1. XEmacs support is better tested, although use under -GNU Emacs has certain advantages (e.g., nested comments!). Please check - -for detailed notes. Older releases of Emacs -may work, but we recommend the use of these or newer versions -because backwards compatibility across different Emacs versions is far -too difficult to support. If you cannot upgrade your Emacs, consider -using an older release of Proof General. -
--Prover versions: -This version has been tested with Coq 7.4, Isabelle2003, Lego 1.3.1, -and PhoX 0.8. -
-Bundled packages: -Proof General is now bundled with several Emacs packages, to -save the effort needed of installing them separately, and to -solve compatibility problems. -This includes X-Symbol, so you don't need to download -it separately any more. If you want to override PG's preference -for it's own packages, simply load your versions into memory -before starting Proof General (e.g. with (require 'x-symbol) -in your .emacs file). --For install instructions, see -the stable version download. -
- --
--
- - - --This tarball contains all of our development files, including some -files not present in the released version of Proof General. -Specifically: -
--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). -
- - diff --git a/html/doc b/html/doc deleted file mode 100644 index a58717d8..00000000 --- a/html/doc +++ /dev/null @@ -1,5 +0,0 @@ - - \ No newline at end of file diff --git a/html/doc.html b/html/doc.html deleted file mode 100644 index 466add09..00000000 --- a/html/doc.html +++ /dev/null @@ -1,140 +0,0 @@ --There is a short FAQ and two manuals for Proof General: -
--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: -
-The PostScript files are recommended over the PDF. -Both manuals (HTML and Info formats) are included in the -download. 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 -development download. -
- --You can discuss Proof General with other users and receive -announcements by joining our mailing -list. -
- - -If you're new to Emacs, it's recommended to try the Emacs tutorial, -available inside Emacs by pressing C-h t (which means -ctrl-with-h followed by t). There are many -other C-h commands, and the Help menu inside Emacs gives access -to more help facilities. -
-For on-line reading, these links might be helpful: -
The corresponding manuals for XEmacs are -available here (xemacs.org). -
- - - - - - -Ideas for the future of Proof General are given here: -
-A technology overview of Proof General is given here: -
-Proof General supports Script Management as documented in: -
-- It has support for Proof by Pointing, as documented in: -
--Before downloading Proof General, please -register. -It's free, it only takes a moment. -If you have already registered you do not need to do so again. - -
- --You can join the -Proof General -mailing list -for announcements of new versions. -Developers and early-adopters may like to download -a development release -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 -previous releases. -
-
-Proof General is distributed under the terms of
-the
-.
-
-See below for software pre-requisites for running Proof General.
-
-Proof General is available as an archive and an RPM package. -
-| gzip'ed tar file | -- |
| zip file | -- |
| RPM package | -
- NB: to build yourself use the tar file with rpm -ta. |
-
| individual files | -browse individual files - |
-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 here. - -
- -This version of Proof General has been tested with XEmacs 21.4 and -GNU Emacs 21.2. It should work with some 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. -
--See the for more -details, or check the file for a summary -of changes since version 3.3. -
- --Check the latest file -(also - - - -) -before reporting problems. If you find a problem not already mentioned, -please -. -
- --To run Proof General, you must have: -
--There is also an optional component for using -Proof General: -
-To use Proof General, simply unpack the sources with -
-- tar xpzf ProofGeneral-3.4.tar.gz --
-(use gunzip first in place of z if you don't have
-GNU tar),
and then add this one line to your .emacs file:
-
- (load-file "directory/generic/proof-site.el") --
-Where directory is the directory in which you unpacked
-the sources.
-
-If you use the RPM package, directory is
-/usr/share/emacs/ProofGeneral
-
-If you're using Windows, then download the zip file.
-
-Use a zip file utility to unpack it somewhere, for example
-c:\ProofGeneral
-
-Further customization is possible via the Customize menus in
-Emacs.
-
-See the
-file in the distribution for more details.
-
-X-Symbol is easy to install in XEmacs and configures itself automatically. -
--Simply download the binary package file, and do something -like this to install in your home directory: -
-- mkdir -p ~/.xemacs/xemacs-packages-
- cd ~/.xemacs/xemacs-packages
- tar xpzf ../x-symbol-pkg.tar.gz
-
-For GNU Emacs, you must remove the .elc files supplied, and -add some code to your .emacs. See -this page -for details. -More installation options are given -in the the X-Symbol manual. diff --git a/html/eeproof b/html/eeproof deleted file mode 100644 index 2df23c96..00000000 --- a/html/eeproof +++ /dev/null @@ -1,5 +0,0 @@ - - diff --git a/html/eeproof.php b/html/eeproof.php deleted file mode 100644 index 445fead7..00000000 --- a/html/eeproof.php +++ /dev/null @@ -1,32 +0,0 @@ - - -
-The Engineering Electronic Proof 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. -
- --More details will be posted here in due course. -
--In the meantime, there is some related -information on the Proof General Kit -page about the next stages of development for Proof General. -
--
";
- print "This is a flattened outline file: click on a title to hide/reveal the leaf underneath it.";
- print "
Click ";
- print "here to show whole body, or ";
- print "here to hide whole body.";
- 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="
\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\.~/_@]+)","\\1",$line); - // Font-lock equivalents... - // 1. comments. Strings roughly done: ignore if quote appears after ; -// seems buggy:
-Proof General, and particularly, the Proof General -Kit is proposed as a vehicle for research into engineering -electronic proof. We want to investigate the -maintenance, combination, and reuse of formal proof developments. -
- --This project has not yet been started, and there are no public -documents available yet. -
--Some hints of our plans appear in the papers describing -the Proof General Kit. -
- --Any comments are welcomed. -
- - diff --git a/html/favicon.ico b/html/favicon.ico deleted file mode 100644 index d3faa231..00000000 Binary files a/html/favicon.ico and /dev/null differ diff --git a/html/features b/html/features deleted file mode 100644 index a58717d8..00000000 --- a/html/features +++ /dev/null @@ -1,5 +0,0 @@ - - \ No newline at end of file diff --git a/html/features.html b/html/features.html deleted file mode 100644 index ebe5bb27..00000000 --- a/html/features.html +++ /dev/null @@ -1,210 +0,0 @@ - --It doesn't matter if you're an Emacs militant or a pacifist! -
- -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 -proof engineering of interactively-constructed proofs. -
-Proof General is used by many people for organizing large proof -developments, and also for teaching interactive proof. -They enjoy the following features:
- -- 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. -
-- Take a look at these - screenshots - of Proof General to see script management in action. -
-- 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. -
-- 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). -
-- 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. -
-- Proof by pointing 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. -
- -- Using the toolbar, you can replay proofs without knowing any - low-level commands of the proof assistant or any Emacs hot-keys! -
- Additionally, the toolbar commands and many more besides are - available on menus; you don't need to know magical key presses for - any features. -
-- Proof General decorates proof scripts: proof commands are - highlighted and different fonts may be used for definitions and - assumptions, for example. -
--
- Many facilities are provided for editing proof scripts. - The completion mechanism of Emacs can be used to - help type keywords and identifier names. - The outline mode of Emacs allows hiding of parts of proof scripts; - a further special proof hiding facility is provided to - hide the body of completed proofs. - Navigation in the script is supported by a pull-down menu - which gives easy access to the theorems, definitions, and declarations - in the current buffer. -
- - --
- Most importantly, Proof General is generic, so you can adapt it to - a new proof assistant with surprisingly little effort. -
- 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 - . - 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. -
- Please feel free to download Proof General to customize it for a new - system, and - - how you get on. --For (even) more details of Proof General's features, see the manuals and -papers on the documentation page. -
- diff --git a/html/feedback b/html/feedback deleted file mode 100644 index 94066bcf..00000000 --- a/html/feedback +++ /dev/null @@ -1,6 +0,0 @@ - - - diff --git a/html/feedback.php b/html/feedback.php deleted file mode 100644 index e599bfcd..00000000 --- a/html/feedback.php +++ /dev/null @@ -1,89 +0,0 @@ - - --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 -
--You can also report a bug using this form, although it would -be more helpful to do this from within Emacs, using the -"Proof General -> Submit bug report" menu command. -
- - - -Dear " . $from . ",\n"; }; - print ""; - print "Thank-you for sending us feedback"; - if ($subject != "") { print " about " . $subject; }; - print ".
\n"; - 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 "
"; - - 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 deleted file mode 100644 index ded131d6..00000000 --- a/html/fileshow.php +++ /dev/null @@ -1,8 +0,0 @@ - diff --git a/html/footer.html b/html/footer.html deleted file mode 100644 index 77709857..00000000 --- a/html/footer.html +++ /dev/null @@ -1,10 +0,0 @@ - -[" . $text . "]
"; -} - -/* 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 "" . $text . ""; -} - -/* 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 ""; - if ($linkname == "") { - print $filename; - } else { - print $linkname; - }; - print ""; - 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 ""; 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 "\n"; -// print "\n"; /* Naughty stuff for older browsers, shouldn't do if V4 */ - print "\n"; - print "\n"; -} - -function click_to_go_back() { - // FIXME: the empty href no longer refers to the root, - // so this use of "/" breaks relative linking. - print "
\nClick here to go back to the "; - print $project_title; // FIXME: doesn't work, prints nothing. - print " front page.
\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 "\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 "\n";
- print "-- - --Here are some publicity pictures for Proof General. They were created -by David Aspinall in his spare time, using the excellent freeware -programs GIMP and Blender. The General himself is -based on a commercial mesh given away by -Viewpoint. -
--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! -
-Copyright for the images is held by -David Aspinall. -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 contact us. -
- - --For pictures of what Proof General looks like in use, -see the screenshots page. -
-
-
-
-
- |
-
-
-Proof General portrait |
-
-
-
- |
-
-
-New Recruits Wanted |
-
-
-
- |
-
-
-Scary boots! |
-
-
-
- |
-
-
- Organize your proofs!- ';
- $urlbits = parse_url($REQUEST_URI);
- $file = ereg_replace("^(.*/)+","",$urlbits["path"]);
- $WANTED = ereg_replace(".html","",$file);
- print " |
-The Proof General Kit project is in an early experimental stage at -the moment. If you are interested in collaborating, or have ideas -or suggestions to contribute, please send a note to -da+pg-kit@inf.ed.ac.uk -
- --Ideas for the future of Proof General are described in these papers: -
--Work which is currently in progress includes: -
-We hope to make an alpha version of some software available in the -not-too-distant future. -
- - diff --git a/html/links b/html/links deleted file mode 100644 index a58717d8..00000000 --- a/html/links +++ /dev/null @@ -1,5 +0,0 @@ - - \ No newline at end of file diff --git a/html/links.html b/html/links.html deleted file mode 100644 index f18d20f0..00000000 --- a/html/links.html +++ /dev/null @@ -1,71 +0,0 @@ --Here are some links to related things. -If you have any suggestions -for links to include here, please -. -
- --The Proof General Users mailing list is a low-volume list -used for announcements of new versions, and occasional -discussions amongst users. -
--This list is not for those having problems with the -software: please contact -da+pg-support@inf.ed.ac.uk -in the first instance. -
- -
-To subscribe or unsubscribe, visit
-the
-Mailman
-web page for the list.
-
-Alternatively, you can send a message to
-
-proofgeneral-request@informatics.ed.ac.uk
-with the word "subscribe" (or "unsubscribe
-The canonical mailing list address is
-da+pg-users@inf.ed.ac.uk.
-
-This is an alias for
-proofgeneral@informatics.ed.ac.uk.
-
-In an effort to prevent spam, posting is restricted to list members. -Please subscribe here before attempting to post. -
- --Archives of the list (since July 2002) are kept -here. -
- --There is a separate mailing list for those interested in the -development of Proof General. The canonical address -for this list is da+pg-devel@inf.ed.ac.uk. -Again, posting is restricted to list members. -Please visit the Mailman web page for subscription details. -
- - - - diff --git a/html/mailinglist.html b/html/mailinglist.html deleted file mode 100644 index 59a74d27..00000000 --- a/html/mailinglist.html +++ /dev/null @@ -1,6 +0,0 @@ - - - diff --git a/html/main b/html/main deleted file mode 100644 index a58717d8..00000000 --- a/html/main +++ /dev/null @@ -1,5 +0,0 @@ - - \ No newline at end of file diff --git a/html/main.html b/html/main.html deleted file mode 100644 index fdffc920..00000000 --- a/html/main.html +++ /dev/null @@ -1,145 +0,0 @@ --Proof General is a generic interface for proof assistants, -currently based on the customizable text editor Emacs. -It works with either -XEmacs or -GNU Emacs. -Proof General has been developed at the -LFCS -in the University of Edinburgh. -
--To find out more, check the - features list -and look at the -screenshots. -To get Proof General, visit the -download page. -If you're not interested in interactive proof, -see the standalone components -developed as part of Proof General. -To contact the developers, click -. -
- - - -Proof General comes ready-to-go for these proof -assistants:
- -| - ", - "The Isabelle Home Page"); ?> - | - for
-
- -
- By
- David Aspinall
- and
- Markus Wenzel.
-
- |
-
| - ","The Coq Home Page") ?> - | -
- for
-
- -
- By Healfdene Goguen, Patrick Loiseleur, David Aspinall, and
- Pierre Courtieu.
-
- |
-
| - ", - "The PhoX Home Page") ?> - | - for
-
- -
- By
- Christophe Raffalli
- and
- Paul Roziere.
-
- |
-
| - ", - "The LEGO Home Page") ?> - | - for
-
- -
- By Thomas Kleymann, Dilip Sequeira,
- David Aspinall
- and
- Paul Callaghan.
-
- |
-
There are also experimental or in-development instances -of Proof General:
- -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 send a note to if you're interested).
- -Proof General is ready to be customized to new proof assistants. -It can be to get basic support working. Full documentation on -configuration is provided.
diff --git a/html/mission.html b/html/mission.html deleted file mode 100644 index a0203092..00000000 --- a/html/mission.html +++ /dev/null @@ -1,136 +0,0 @@ - - --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. -
--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. -
- --
--Please update your links!. The server zermelo.dcs.ed.ac.uk -hosting Proof General for the last 5 years has now been retired. -Moroever, the Proof General .org domain has been poached from us. -
--Please refer to the web site using the URL -proofgeneral.inf.ed.ac.uk -and do not send any email to the old .org addresses (contact -David Aspinall directly). Also, beware that the old addresses are built -into the help function of Proof General and the bug reporting commands. -Please download the upcoming pre-release (available soon) -which has offending addresses removed. -
--There is a new development version of -Proof General released today. There are some minor fixes, and an -updated version of X-Symbol bundled. Please test it and let me know -how you get on. It would be nice to release the final version 3.5 at -last. -
-The Proof General Kit page has been -updated to mention current development efforts. - --Anonymous access to the Proof General CVS repository is now available! -Details are here. -
-
-Proof General 3.4 is released. Happy Proving!
-
-Go to the download page to get it.
-
-Please report any problems to da+pg-support@inf.ed.ac.uk.
-
-Good news! The license conditions for Proof General will shortly be -changed to the GPL. -This relaxes the current conditions in several ways, in particular, -allowing packaging and distribution of the code by others. -
-
-We plan to release version 3.4 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.
-
-Please, please, please do test some development releases for us in the
-meantime and report any difficulties,
-to help make the next release of Proof General as
-robust as possible. Thanks!
-
-The current development release 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. -
--Proof General 3.3 is released, with - to -increase your proof script editing efficiency. Happy proving! -
-
-The past few months have seen a few more improvements and
-bug fixes to Proof General: many thanks to those who have
-sent us useful feedback.
-It's time that we made a proper release, so please try
-out the development release
-and help us iron out as many more problems as we can.
-
-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.
-
-Proof General has had a few quiet improvements since October, which -appear in the current -development release. -This version also has some compatibility fixes -for the recent releases of Emacs (20.7) and XEmacs (21.4). -
- --Proof General 3.2 is released today. Happy proving! -
- --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 -pre-release, 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 -, - -or -, -and the separate "adapting" manual, in -, - -or -. -(Info files are included in the distribution). -
--Improvements to web pages. Graphics made smaller, text more concise. -Please -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). -
--We're starting the testing phase for Proof General 3.2. -It has several new features and improvements. -Please try out the pre-release -version, and report any problems to us. Your -feedback is very important because we have no resources available for -serious compatibility testing ourselves. -
--We hope to release 3.2 by the end of September. -
--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 -proof-toolbar-use-button-enablers). -The patch also removes -the use of an "interval timer" when -proof-toolbar-use-button-enablers 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. -
--New! -Proof General . -Please send questions or suggestions for inclusion to -proofgen@dcs.ed.ac.uk, -thanks. -
--A minor patch to Proof General 3.1 is released today. To check what -version you have, look at the variable proof-general-version -set in proof-site.el. (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 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. -
--Further improvements are being introduced in the new 3.2 pre-releases, -see the -development download page, as usual. -
--Proof General 3.1 is now available from the -download page. Enjoy! -
--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. -
--New: HOL Proof General! -It took me only a couple of hours to add a basic instantiation of -ProofGeneral for -HOL98. -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. -
--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. -
--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. -
--The HOL support is shipping in the -current development release. -
--There is now a new -page for developers. -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. -
--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. -
--In the meantime, please - -that you would like to see fixed, and consider trying out -the current development release. -
--I'm pleased to say that Proof General will be demonstrated at -ETAPS 2000. -Here are some draft slides for -the presentation -(any comments would be welcome). -A presentation of Proof General based on these slides was given at -Rutherford Appleton Laboratory last week. -
--Proof General 3.0 is released! -
--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 pre-release, 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. -
--New! With Proof General 3.0, adapting to a new prover is easier -than ever before! -It includes an - -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! -
--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 -pre-release -for Isabelle 99. -
--Some recent changes have been made to the support for -X-Symbol, -so that it is easier to turn on and off, and support is now -properly generic. At the moment only Isabelle has -support implemented. -
-- See what Proof General 3.0 will look like! - The screenshot has been updated. -
-- The next version of Proof General will be 3.0. -
-- 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! -
-- Version 3.0 is planned for release in November. - Please test a Version 3.0 pre-release if you can - and report any problems. -
-
- I'm very grateful to
- Pierre Courtieu <courtieu@lri.fr>
- for offering to help work on Coq Proof General.
-
- 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...
-
- Recently there has been a flurry of work on the next version of Proof
- General. It has quite a number of improvements (see the file), made by myself
- and Markus Wenzel.
The next version is aimed to coincide
- roughly with the release of Isabelle 99.
-
- At the moment we urgently need 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. Please offer to help, - it needn't be a heavy commitment. -
-
- I've just returned from the
- Types Summer School, Giens, France
- 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.
-
-
- Print pictures from the new - gallery - of publicity shots of Proof General! -
-
- Proof General version 2.1 is released.
-
- Check the file
- for a summary of changes since Proof General 2.0.
-
- It is recommended that all users upgrade except
- those still using Isabelle 98-1.
-
- Proof General 2.1 supports only the 99 version of Isabelle.
-
- New Proof General web pages go live! -
-- 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. -
-- Please explore the new web pages and report any problems - or suggestions to . - 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. -
-A new instantiation of Proof General has been added by - Paul Callaghan - for - Plastic, - a new proof assistant based on - Luo's Typed Logical Framework and - implemented in Haskell. -
-A new instantiation of Proof General has been added by - Markus Wenzel - for Isabelle/Isar, - a new proof language for Isabelle to be included with Isabelle 99. -
--News items by David Aspinall. -
- - - diff --git a/html/oldrel.php b/html/oldrel.php deleted file mode 100644 index c48df091..00000000 --- a/html/oldrel.php +++ /dev/null @@ -1,162 +0,0 @@ - - --Please note that we do not support these old releases in any way. -
- --This version of Proof General has been tested -with XEmacs 21.4 and (briefly) with GNU Emacs 20.7 -(it does not support GNU Emacs 21.x). -It supports Coq version 7.x, LEGO version 1.3.1 and -Isabelle2002. -
- --Check the file -for a summary of changes since version 3.2. -
- - --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. -
- --Check the file -for a summary of changes since version 3.1. -
- --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. -
- --Check the file -for a summary of changes since version 3.0. -
- - - -
-This version of Proof General has been tested
-with XEmacs 20.4, XEmacs 21.1.8 and GNU Emacs 20.5.
-It supports Coq version 6.3, LEGO version 1.3.1 and Isabelle99.
-
-Check the file -for a summary of changes since version 2.1. -
- - - -
-This version of Proof General has been tested
-with XEmacs 20.4, XEmacs 21 and GNU Emacs 20.3.
-It supports Coq version 6.3, LEGO version 1.3.1 and
-some pre-release versions of Isabelle version 99.
-
-This version of Proof General has been tested
-with XEmacs 20.4 and GNU Emacs 20.2, 20.3.
-It supports Coq version 6.2, LEGO version 1.3.1, and
-Isabelle version 98-1.
-
-Here are some proposals for projects connected to Proof General. -
--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. -
--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. -
- --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 self-documenting 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, edebug. -
- - - - - - - - - - - - --If you are interested in working on any of these projects, -feel free to discuss with the project proposer or on the -developer's mailing list. -
- --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 -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). -
- --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 -. -Projects should be significant contributions rather than -incremental improvements (although we welcome the suggestion of those -too). -
- - - diff --git a/html/projects/acs.html b/html/projects/acs.html deleted file mode 100644 index d3768c17..00000000 --- a/html/projects/acs.html +++ /dev/null @@ -1,36 +0,0 @@ --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. -
--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. -
--This improvement should allow support for Coq's Section command, -LEGO's Discharge and simplified support for Isabelle/Isar, -by removing some of the prover-specific code. -
--References: -Proof General manual -(), and proof assistant manuals.
--Skills: -Good Emacs Lisp, understanding of "granularity" problem -for proof assistant history mechanisms.
--Proposer: -David Aspinall -(based on an original idea by Thomas Kleymann). -
- diff --git a/html/projects/coqfile.html b/html/projects/coqfile.html deleted file mode 100644 index 35d48eb1..00000000 --- a/html/projects/coqfile.html +++ /dev/null @@ -1,22 +0,0 @@ --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. -
--Skills: - Some understanding of Coq implementation, co-operation with - the Coq developers to get any Coq modifications (if any) incorporated. - Some Emacs Lisp knowledge. -
-Proposer: -David Aspinall. -
diff --git a/html/projects/coqpbp.html b/html/projects/coqpbp.html deleted file mode 100644 index 366feb7c..00000000 --- a/html/projects/coqpbp.html +++ /dev/null @@ -1,17 +0,0 @@ --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. -
--Skills: - Some understanding of Coq implementation, co-operation with - the Coq developers to get any Coq modifications (if any) incorporated. - Minimal Emacs Lisp knowledge. -
-Proposer: -David Aspinall. -
diff --git a/html/projects/corba.html b/html/projects/corba.html deleted file mode 100644 index 35faa73f..00000000 --- a/html/projects/corba.html +++ /dev/null @@ -1,37 +0,0 @@ --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. -
--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. -
--An CORBA binding for Haskell would also be an interesting project. -
--See -Claudio Russo's -project suggestion for a similar proposal, including useful links. -
--Skills: -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. -
-Proposers: -Markus Wenzel and -David Aspinall. -
diff --git a/html/projects/hol.html b/html/projects/hol.html deleted file mode 100644 index 6828899a..00000000 --- a/html/projects/hol.html +++ /dev/null @@ -1,40 +0,0 @@ --It is fairly easy to get basic support for Proof General for -HOL, 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. -
--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 Boomburg-HOL 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. -
--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). -
--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. -
-Skills: -Some Standard ML, some Emacs Lisp. Basic understanding of -proof assistant behaviour, interest in HOL. -
-Proposer: -David Aspinall. -
diff --git a/html/projects/isapbp.html b/html/projects/isapbp.html deleted file mode 100644 index c08ea85e..00000000 --- a/html/projects/isapbp.html +++ /dev/null @@ -1,25 +0,0 @@ --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 - -patch by Burkhart Wolff -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. -
--Skills: - 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. -
-Proposer: -David Aspinall. -
- diff --git a/html/projects/outline.html b/html/projects/outline.html deleted file mode 100644 index 67680b8f..00000000 --- a/html/projects/outline.html +++ /dev/null @@ -1,26 +0,0 @@ --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. -
-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). -
-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). -
--Skills: -Some understanding of the workings of Emacs outline mode and Proof -General script management. Good portion of Emacs lisp knowledge. -
-Proposer: -Markus Wenzel. -
- diff --git a/html/projects/pgip.html b/html/projects/pgip.html deleted file mode 100644 index 073edd06..00000000 --- a/html/projects/pgip.html +++ /dev/null @@ -1,22 +0,0 @@ --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 white paper. 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. -
--Skills: -Interest in interactive proof and basic understanding -of interaction mechanisms with at least one of -LEGO, Coq, Isabelle. Programmming in Emacs Lisp. -
-Proposer: -David Aspinall. -
diff --git a/html/projects/pgml.html b/html/projects/pgml.html deleted file mode 100644 index 46cdd960..00000000 --- a/html/projects/pgml.html +++ /dev/null @@ -1,26 +0,0 @@ --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 -here, 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. -
--Skills: -Understanding of markup languages and tools for using and specifying them. -Interest in representation of mathematical content. -Necessary programming skills. -
-Proposer: -David Aspinall. -
- diff --git a/html/projects/reelcase.html b/html/projects/reelcase.html deleted file mode 100644 index f5fa2f04..00000000 --- a/html/projects/reelcase.html +++ /dev/null @@ -1,34 +0,0 @@ --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 Rational -ClearCase. -
--The crucial way that ClearCase goes beyond CVS is in providing a view -of a configuration directly through a special mountpoint on -the filesystem. -
--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. -
--Skills: -Expert C programmer, with ability to understand and work on Linux -kernel code. Understanding of configuration management principles. -
-Proposers: -David Aspinall -from an idea by -Christoph Lüth -
diff --git a/html/projects/scrgen.html b/html/projects/scrgen.html deleted file mode 100644 index d65b477f..00000000 --- a/html/projects/scrgen.html +++ /dev/null @@ -1,26 +0,0 @@ --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. -
--An alternative version of this project is to implement a -generic basis for script management which does not 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. -
-Skills: -Proficient Emacs Lisp (or other programming language), -knowledge of scripting languages desirable. -
-Proposer: -David Aspinall. -
diff --git a/html/projects/test.html b/html/projects/test.html deleted file mode 100644 index f9d5ecf0..00000000 --- a/html/projects/test.html +++ /dev/null @@ -1,24 +0,0 @@ --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. -
--Skills: -An interesting in testing user interfaces. -Basic knowledge of Emacs Lisp. -
-Proposer: -David Aspinall. -
- diff --git a/html/projects/thybrowse.html b/html/projects/thybrowse.html deleted file mode 100644 index 8993d942..00000000 --- a/html/projects/thybrowse.html +++ /dev/null @@ -1,34 +0,0 @@ --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 theory browser 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 dired-like buffer. -
--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 here). 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). -
--(For a related idea, see the browser integrated with OCaml). -
--Skills: -Interface programming skills. -Basic understanding of what theories are for several different proof -assistants. -
-Proposer: -David Aspinall. -
- diff --git a/html/projects/webreplay.html b/html/projects/webreplay.html deleted file mode 100644 index 1754e2df..00000000 --- a/html/projects/webreplay.html +++ /dev/null @@ -1,24 +0,0 @@ --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 white paper would -be followed. -
--Skills: -Strong web programming skills using scripting languages, -dynamic HTML, etc. -
-Proposer: -David Aspinall. -
- - diff --git a/html/projects/xmlpgip.html b/html/projects/xmlpgip.html deleted file mode 100644 index 30828a97..00000000 --- a/html/projects/xmlpgip.html +++ /dev/null @@ -1,40 +0,0 @@ --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 white paper. 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. -
--Skills: -Interest in interactive proof and basic understanding -of interaction mechanisms with at least one of -LEGO, Coq, Isabelle. Programmming in Emacs Lisp. -
-Proposer: -David Aspinall. -
- - - -- Your registration form was incomplete. Please fill in all - the fields, thank-you! -
- -
-Please register your download using the short form below.
-
-The information provided will only be used to help
-provide a case for support for Proof General in the future.
-
-If you have already registered you do not need to fill in the form -again, so return to the download page. -
- -";
- print "Thank you for filling in the form. Your registration has been sent.
";
-
- /* 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.
";
- }
- print "
"; - - print "
\nClick ";
- print "here";
- print " to return to the download page.
- Your registration form was incomplete. Please fill in all - the fields, thank-you! -
- -
-Please register your download using the short form below.
-
-The information provided will only be used to help
-provide a case for support for Proof General in the future.
-
-If you have already registered you do not need to fill in the form -again, so return to the download page. -
- --
-Dear " . $name . ",\n"; - print "";
- print "Thank you for filling in the form. Your registration has been sent.
";
-
- /* Next bit duplicated in mailinglist.html.
- Could be a function in functions.php3 */
-
- if ($mailinglist) {
- $message = "subscribe proofgeneral";
- mail("mailman@inf.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.
";
- }
- print "
"; - - print "
\nClick ";
- print "here";
- print " to return to the download page.
-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. -
- - - -
-
-
-
- |
-
-
-Building a simple proof in LEGO with proof-by-pointing.
- - |
-
-
-
- |
-
-
-Coq Proof General running in multiple frame mode,
-full screen shot (1024x768).
- - |
-
-
-
- |
-
-
-Replaying a domain theory proof in Isabelle's HOLCF logic.
- - |
-
-
-
- |
-
- -Replaying a proof in Isar, Isabelle's declarative proof language -developed by Markus Wenzel. - -- |
-
-
-
- |
-
-
-LEGO Proof General running in plain console mode.
- - |
-
-For more pictures, see the Proof General gallery. -
- diff --git a/html/smallheader.html b/html/smallheader.html deleted file mode 100644 index ade4e6dd..00000000 --- a/html/smallheader.html +++ /dev/null @@ -1,8 +0,0 @@ -
-
-
-
- |
-diff --git a/html/smallpage.html b/html/smallpage.html deleted file mode 100644 index 64f538a3..00000000 --- a/html/smallpage.html +++ /dev/null @@ -1,6 +0,0 @@ - diff --git a/html/smallpage.php b/html/smallpage.php deleted file mode 100644 index ef165c6d..00000000 --- a/html/smallpage.php +++ /dev/null @@ -1,12 +0,0 @@ - diff --git a/html/userman b/html/userman deleted file mode 100644 index e8ccc072..00000000 --- a/html/userman +++ /dev/null @@ -1,3 +0,0 @@ - -- cgit v1.2.3 |