diff options
| -rw-r--r-- | etc/ProofGeneral.spec | 4 | ||||
| -rw-r--r-- | generic/proof-site.el | 393 | ||||
| -rw-r--r-- | html/devel.html | 38 | ||||
| -rw-r--r-- | html/develdownload.php | 18 |
4 files changed, 30 insertions, 423 deletions
diff --git a/etc/ProofGeneral.spec b/etc/ProofGeneral.spec index abd55689..0c2d9b2b 100644 --- a/etc/ProofGeneral.spec +++ b/etc/ProofGeneral.spec @@ -1,12 +1,12 @@ Summary: Proof General, Emacs interface for Proof Assistants Name: ProofGeneral -Version: 3.4pre020718 +Version: 3.4pre020719 Release: 1 Group: Applications/Editors/Emacs Copyright: LFCS, University of Edinburgh Url: http://www.proofgeneral.org/ Packager: David Aspinall <da@dcs.ed.ac.uk> -Source: http://www.proofgeneral.org/ProofGeneral-3.4pre020718.tar.gz +Source: http://www.proofgeneral.org/ProofGeneral-3.4pre020719.tar.gz BuildRoot: /tmp/ProofGeneral-root PreReq: /sbin/install-info Prefixes: /usr/share/emacs /usr/bin /usr/info diff --git a/generic/proof-site.el b/generic/proof-site.el index d4e83b25..e69de29b 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -1,393 +0,0 @@ -;; proof-site.el -- Loading stubs for Proof General. -;; Configuration for site and choice of provers. -;; -;; Copyright (C) 1998-2002 LFCS Edinburgh. -;; Author: David Aspinall <da@dcs.ed.ac.uk> -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ -;; -;; NB: Normally you will not need to edit this file. -;; - -(if (featurep 'proof-site) - nil ; don't load twice - -(if (or (not (boundp 'emacs-major-version)) - (< emacs-major-version 20)) - (error "Proof General is not compatible with Emacs %s" emacs-version)) - -(defgroup proof-general nil - "Customization of Proof General." - :group 'external - :group 'processes - :prefix "proof-") - - -;; This customization group gathers together -;; the internals of Proof General which control -;; configuration to different proof assistants. -;; This is for development purposes rather than -;; user-level customization, so this group does -;; not belong to 'proof-general (or any other group). -(defgroup proof-general-internals nil - "Customization of Proof General internals." - :prefix "proof-") - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; Directories -;; -(defun proof-home-directory-fn () - "Used to set proof-home-directory" - (let ((s (getenv "PROOFGENERAL_HOME"))) - (if s - (if (string-match "/$" s) s (concat s "/")) - (let ((curdir - (or - (and load-in-progress (file-name-directory load-file-name)) - (file-name-directory (buffer-file-name))))) - (file-name-directory (substring curdir 0 -1)))))) - -(defcustom proof-home-directory - (proof-home-directory-fn) - "Directory where Proof General is installed. Ends with slash. -Default value taken from environment variable `PROOFGENERAL_HOME' if set, -otherwise based on where the file `proof-site.el' was loaded from. -You can use customize to set this variable." - :type 'directory - :group 'proof-general-internals) - -(defcustom proof-images-directory - (concat proof-home-directory "images/") - "Where Proof General image files are installed. Ends with slash." - :type 'directory - :group 'proof-general-internals) - -(defcustom proof-info-directory - (concat proof-home-directory "doc/") - "Where Proof General Info files are installed. Ends with slash." - :type 'directory - :group 'proof-general-internals) - -;; Add the info directory to the end of Emacs Info path if need be. -;; It's easier to do this after Info has loaded because of the -;; complicated way the Info-directory-list is set. - -(eval-after-load - "info" - '(or (member proof-info-directory Info-directory-list) - (progn - (setq Info-directory-list - (cons proof-info-directory - Info-directory-list)) - ;; Clear cache of info dir - (setq Info-dir-contents nil)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; Master table of supported proof assistants. -;; -(defcustom proof-assistant-table - (apply - 'append - (mapcar - ;; Discard entries whose directories have been removed. - (lambda (dne) - (let ((atts (file-attributes (concat proof-home-directory - (symbol-name (car dne)))))) - (if (and atts (eq 't (car atts))) - (list dne) - nil))) - '(;; For demonstration instance of Proof General, - ;; export PROOFGENERAL_ASSISTANTS=demoisa. - ;; - ;; To use Isabelle/Isar instead of classic Isabelle, - ;; export PROOFGENERAL_ASSISTANTS=isar - ;; - (demoisa "Isabelle Demo" "\\.ML$") - (isa "Isabelle" "\\.ML$\\|\\.thy$") - (isar "Isabelle/Isar" "\\.thy$") - (lego "LEGO" "\\.l$") - (coq "Coq" "\\.v$") - (phox "PhoX" "\\.phx$") - ;; The following provers are not fully supported, - ;; and have only preliminary support written - ;; (please volunteer to improve them!) - (hol98 "HOL" "\\.sml$") - (acl2 "ACL2" "\\.acl2$") - (twelf "Twelf" "\\.elf$") - ;; The following provers have experimental support - (plastic "Plastic" "\\.lf$") - ;; Next line for testing only - ;; (pgip "PGIP/Isa" "\\.ML$\\|\\.thy$") - ))) - "*Proof General's table of supported proof assistants. -Extend this table to add a new proof assistant. -Each entry is a list of the form - - (SYMBOL NAME AUTOMODE-REGEXP) - -The NAME is a string, naming the proof assistant. -The SYMBOL is used to form the name of the mode for the -assistant, `SYMBOL-mode', run when files with AUTOMODE-REGEXP -are visited. SYMBOL is also used to form the name of the -directory and elisp file for the mode, which will be - - PROOF-HOME-DIRECTORY/SYMBOL/SYMBOL.el - -where `PROOF-HOME-DIRECTORY' is the value of the -variable proof-home-directory." - :type '(repeat (list symbol string string)) - :group 'proof-general-internals) - - - - - -;; A utility function. Is there an alternative? -(defun proof-string-to-list (s separator) - "Return the list of words in S separated by SEPARATOR. -If S is nil, return empty list." - (if s - (let ((end-of-word-occurence (string-match (concat separator "+") s))) - (if (not end-of-word-occurence) - (if (string= s "") - nil - (list s)) - (cons (substring s 0 end-of-word-occurence) - (proof-string-to-list - (substring s - (string-match (concat "[^" separator "]") - s end-of-word-occurence)) - separator)))))) - -(defcustom proof-assistants nil - (concat - "*Choice of proof assistants to use with Proof General. -A list of symbols chosen from:" - (apply 'concat (mapcar (lambda (astnt) - (concat " '" (symbol-name (car astnt)))) - proof-assistant-table)) -".\nEach proof assistant defines its own instance of Proof General, -providing session control, script management, etc. Proof General -will be started automatically for the assistants chosen here. -To avoid accidently invoking a proof assistant you don't have, -only select the proof assistants you (or your site) may need. - -You can select which proof assistants you want by setting this -variable before `proof-site.el' is loaded, or by setting -the environment variable `PROOFGENERAL_ASSISTANTS' to the -symbols you want, for example \"lego isa\". Or you can -edit the file `proof-site.el' itself. - -Note: to change proof assistant, you must start a new Emacs session.") - :type (cons 'set - (mapcar (lambda (astnt) - (list 'const ':tag (car (cdr astnt)) (car astnt))) - proof-assistant-table)) - :group 'proof-general) - - -;; Extend load path for the generic files. -(let ((proof-lisp-path - (concat proof-home-directory "generic/"))) - (or (member proof-lisp-path load-path) - (setq load-path - (cons proof-lisp-path load-path)))) - -;; During compilation from the Makefile, generic is on the load path. -;; Add all of the prover directories. -;; FIXME: this doesn't work quite right. We want to test -;; whether we are running during a compilation. How? -; (eval-when-compile -; (dolist (assistant proof-assistant-table) -; (let ((path (concat proof-home-directory -; (concat (symbol-name (car assistant)) "/")))) -; (or (member path load-path) -; (setq load-path -; (cons path load-path)))))) - -(defun proof-ready-for-assistant (assistant-name assistantsym) - "Configure PG for ASSISTANT-NAME, symbol ASSISTANTSYM." - (let* - ((sname (symbol-name assistantsym)) - (cusgrp-rt - ;; Normalized a bit to remove spaces and funny characters - ;; FIXME UGLY compatibility hack - ;; (can use cl macro `substitute' but want to avoid cl here) - (if (fboundp 'replace-in-string) - ;; XEmacs - (replace-in-string (downcase assistant-name) "/\\|[ \t]+" "-") - ;; FSF - (subst-char-in-string - ?/ ?\- - (subst-char-in-string ?\ ?\- (downcase assistant-name))))) - ;; END compatibility hack - (cusgrp (intern cusgrp-rt)) - (cus-internals (intern (concat cusgrp-rt "-config"))) - ;; NB: Dir name for each prover is the same as its symbol name! - (elisp-dir sname) - (loadpath-elt (concat proof-home-directory elisp-dir "/"))) - (eval `(progn - ;; Make a customization group for this assistant - (defgroup ,cusgrp nil - ,(concat "Customization of user options for " assistant-name - " Proof General.") - :group 'proof-general) - ;; And another one for internals - (defgroup ,cus-internals nil - ,(concat "Customization of internal settings for " - assistant-name " configuration.") - :group 'proof-general-internals - :prefix ,(concat sname "-")) - - ;; Set the proof-assistant configuration variables - ;; NB: tempting to use customize-set-variable: wrong! - ;; Here we treat customize as extended docs for these - ;; variables. - (setq proof-assistant-cusgrp (quote ,cusgrp)) - (setq proof-assistant-internals-cusgrp (quote ,cus-internals)) - (setq proof-assistant ,assistant-name) - (setq proof-assistant-symbol (quote ,assistantsym)) - ;; Extend the load path if necessary - (if (not (member ,loadpath-elt load-path)) - (setq load-path (cons ,loadpath-elt load-path))))))) - -;; Now add auto-loads and load-path elements to support the -;; proof assistants selected, and define a stub -(let ((assistants - (or (mapcar 'intern - (proof-string-to-list - (getenv "PROOFGENERAL_ASSISTANTS") " ")) - proof-assistants - (mapcar (lambda (astnt) (car astnt)) proof-assistant-table)))) - (while assistants - (let* - ((assistant (car assistants)) ; compiler bogus warning here - (nameregexp - (or - (cdr-safe - (assoc assistant - proof-assistant-table)) - (error "proof-site: symbol " (symbol-name assistant) - "is not in proof-assistant-table"))) - (assistant-name (car nameregexp)) - (regexp (car (cdr nameregexp))) - (sname (symbol-name assistant)) - ;; NB: File name for each prover is the same as its symbol name! - (elisp-file sname) - ;; NB: Mode name for each prover is <symbol name>-mode! - (proofgen-mode (intern (concat sname "-mode"))) - ;; NB: Customization group for each prover is its l.c.'d name! - - ;; Stub to do some automatic initialization and load - ;; the specific code. - (mode-stub - `(lambda () - ,(concat - "Major mode for editing scripts for proof assistant " - assistant-name - ".\nThis is a stub which loads the real function.") - (interactive) - ;; Give a message and stop loading if proof-assistant is - ;; already set: things go wrong if proof general is - ;; loaded for more than one prover. - (cond - ((and (boundp 'proof-assistant) - (not (string-equal proof-assistant ""))) - (or (string-equal proof-assistant ,assistant-name) - ;; If Proof General was partially loaded last time - ;; and mode function wasn't redefined, be silent. - (message - (concat - ,assistant-name - " Proof General error: Proof General already in use for " - proof-assistant)))) - (t - ;; prepare variables and load path - (proof-ready-for-assistant ,assistant-name - (quote ,assistant)) - ;; load the real mode and invoke it. - (load-library ,elisp-file) - (,proofgen-mode)))))) - - (setq auto-mode-alist - (cons (cons regexp proofgen-mode) auto-mode-alist)) - - (fset proofgen-mode mode-stub) - - (setq assistants (cdr assistants)) - ))) - -;; WARNING: do not edit below here -;; (the next constant is set automatically, also its form is -;; relied upon in proof-config.el, for proof-splash-contents) -(defconst proof-general-version "Proof General Version 3.4pre020718. Released by da." - "Version string identifying Proof General release.") - -;; Now define a few autoloads and basic variables. - -;; 1.8.01: add a dummy package-provide command so proof-autoloads -;; is compatible with FSF Emacs. Needed for next provide -;; (otherwise would be in proof-compat.el). -(or (fboundp 'package-provide) - (defun package-provide (name &rest attributes) - "Dummy version of XEmacs function for FSF compatibility.")) - - -(require 'proof-autoloads) ; autoloaded functions - -(defcustom proof-assistant-cusgrp nil - "Symbol for the customization group of the user options for the proof assistant. -Do not change this variable! It is set automatically by the mode -stub defined in proof-site, from the name given in -proof-assistant-table." - :type 'sexp - :group 'prover-config) - -(defcustom proof-assistant-internals-cusgrp nil - "Symbol for the customization group of the PG internal settings proof assistant. -Do not change this variable! It is set automatically by the mode -stub defined in proof-site, from the name given in -proof-assistant-table." - :type 'sexp - :group 'prover-config) - -(defcustom proof-assistant "" - "Name of the proof assistant Proof General is using. -Do not change this variable! It is set automatically by the mode -stub defined in proof-site, from the name given in -proof-assistant-table." - :type 'string - :group 'prover-config) - -(defcustom proof-assistant-symbol nil - "Symbol for the proof assistant Proof General is using. -Used for automatic configuration based on standard variable names. -Settings will be found by looking for names beginning with this -symbol as a prefix. -Do not change this variable! It is set automatically by the mode -stub defined in proof-site, from the symbols given in -proof-assistant-table." - :type 'sexp - :group 'prover-config) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; -;;; Architecture flags -;;; - -(eval-and-compile -(defvar proof-running-on-XEmacs (string-match "XEmacs" emacs-version) - "Non-nil if Proof General is running on XEmacs.") -(defvar proof-running-on-Emacs21 (and (not proof-running-on-XEmacs) - (>= emacs-major-version 21)) - "Non-nil if Proof General is running on GNU Emacs 21 or later.") -;; rough test for XEmacs on win32, anyone know about GNU Emacs on win32? -(defvar proof-running-on-win32 (fboundp 'win32-long-file-name) - "Non-nil if Proof General is running on a win32 system.")) - -(provide 'proof-site)) -;; proof-site.el ends here diff --git a/html/devel.html b/html/devel.html index cc912c42..f3460042 100644 --- a/html/devel.html +++ b/html/devel.html @@ -10,14 +10,14 @@ users. <li> Download the latest <a href="develdownload.html">development release: <!-- WARNING! Line below automatically edited by makefile. --> - <b>ProofGeneral-3.4pre020718</b></a> + <b>ProofGeneral-3.4pre020719</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.4pre020718/CHANGES","CHANGES"); ?> file +<?php fileshow("ProofGeneral-3.4pre020719/CHANGES","CHANGES"); ?> file <!-- End Warning. --> for a summary of changes since the last stable version. </li> @@ -52,7 +52,7 @@ Take a look at some Proof General <a href="projects.html">project proposals</a>. <li> Read the developer's -<?php fileshow("ProofGeneral-3.4pre020718/README.devel","README file"); ?>, +<?php fileshow("ProofGeneral-3.4pre020719/README.devel","README file"); ?>, with development hints and tips. </li> </ul> @@ -61,7 +61,7 @@ with development hints and tips. <ul> <li> Read the brief list of planned -<?php fileshow("ProofGeneral-3.4pre020718/TODO","things to do "); ?> +<?php fileshow("ProofGeneral-3.4pre020719/TODO","things to do "); ?> for Proof General. </ul> <ul> @@ -69,14 +69,14 @@ for Proof General. <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.4pre020718/todo","generic base"); ?>, + <?php fileshow("ProofGeneral-3.4pre020719/todo","generic base"); ?>, <br> and for each prover: - <?php fileshow("ProofGeneral-3.4pre020718/lego/todo","lego to do"); ?>, - <?php fileshow("ProofGeneral-3.4pre020718/coq/todo","coq to do"); ?>, - <?php fileshow("ProofGeneral-3.4pre020718/isa/todo","isa to do"); ?>, - <?php fileshow("ProofGeneral-3.4pre020718/isar/todo","isar to do"); ?>, - <?php fileshow("ProofGeneral-3.4pre020718/hol98/todo","hol to do"); ?>. + <?php fileshow("ProofGeneral-3.4pre020719/lego/todo","lego to do"); ?>, + <?php fileshow("ProofGeneral-3.4pre020719/coq/todo","coq to do"); ?>, + <?php fileshow("ProofGeneral-3.4pre020719/isa/todo","isa to do"); ?>, + <?php fileshow("ProofGeneral-3.4pre020719/isar/todo","isar to do"); ?>, + <?php fileshow("ProofGeneral-3.4pre020719/hol98/todo","hol to do"); ?>. <!-- end WARNING --> </li> </ul> @@ -93,15 +93,15 @@ which can be used in other programs. <!-- <ul> --> <!-- <li> --> <!-- Browse source files from the current pre-release: --> -<!-- <?php fileshow("ProofGeneral-3.4pre020718/generic/proof.el") ?>, --> -<!-- <?php fileshow("ProofGeneral-3.4pre020718/generic/proof-site.el") ?>, --> -<!-- <?php fileshow("ProofGeneral-3.4pre020718/generic/proof-config.el") ?>, --> -<!-- <?php fileshow("ProofGeneral-3.4pre020718/generic/proof-script.el") ?>, --> -<!-- <?php fileshow("ProofGeneral-3.4pre020718/generic/proof-shell.el") ?>, --> -<!-- <?php fileshow("ProofGeneral-3.4pre020718/generic/proof-toolbar.el") ?>, --> -<!-- <?php fileshow("ProofGeneral-3.4pre020718/generic/proof-syntax.el") ?>, --> -<!-- <?php fileshow("ProofGeneral-3.4pre020718/generic/proof-splash.el") ?>, --> -<!-- <?php fileshow("ProofGeneral-3.4pre020718/generic/proof-easy-config.el") ?>. --> +<!-- <?php fileshow("ProofGeneral-3.4pre020719/generic/proof.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.4pre020719/generic/proof-site.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.4pre020719/generic/proof-config.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.4pre020719/generic/proof-script.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.4pre020719/generic/proof-shell.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.4pre020719/generic/proof-toolbar.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.4pre020719/generic/proof-syntax.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.4pre020719/generic/proof-splash.el") ?>, --> +<!-- <?php fileshow("ProofGeneral-3.4pre020719/generic/proof-easy-config.el") ?>. --> <!-- </ul> --> diff --git a/html/develdownload.php b/html/develdownload.php index 11996dea..80126bdd 100644 --- a/html/develdownload.php +++ b/html/develdownload.php @@ -24,7 +24,7 @@ Please <a href="register">register</a> if you haven't done so already. <!-- WARNING! Line below automatically edited by makefile. --> -<h2><a name="doc">Manual for ProofGeneral-3.4pre020718</a></h2> +<h2><a name="doc">Manual for ProofGeneral-3.4pre020719</a></h2> <!-- End Warning. --> <p> The manual included with the pre-release may be @@ -46,27 +46,27 @@ or <!-- WARNING! Line below automatically edited by makefile. --> -<h2><a name="prerel">Pre-release: ProofGeneral-3.4pre020718</a></h2> +<h2><a name="prerel">Pre-release: ProofGeneral-3.4pre020719</a></h2> <p> Check the <!-- WARNING! Line below automatically edited by makefile. --> -<?php fileshow("ProofGeneral-3.4pre020718/CHANGES","CHANGES"); ?> file +<?php fileshow("ProofGeneral-3.4pre020719/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.4pre020718.tar.gz") ?></td> +<td><?php download_link("ProofGeneral-3.4pre020719.tar.gz") ?></td> </tr> <tr> <td>zip file</td> -<td><?php download_link("ProofGeneral-3.4pre020718.zip") ?></td> +<td><?php download_link("ProofGeneral-3.4pre020719.zip") ?></td> </tr> <tr> <td>RPM package </td> -<td><?php download_link("ProofGeneral-3.4pre020718-1.noarch.rpm") ?></td> +<td><?php download_link("ProofGeneral-3.4pre020719-1.noarch.rpm") ?></td> </tr> <tr> <td>individual files</td> @@ -105,7 +105,7 @@ the <a href="download#install">stable version download</a>. <!-- WARNING! Line below automatically edited by makefile. --> -<h2><a name="devel">Complete archive of ProofGeneral-3.4pre020718 for developers</a></h2> +<h2><a name="devel">Complete archive of ProofGeneral-3.4pre020719 for developers</a></h2> <!-- End Warning. --> <p> @@ -114,7 +114,7 @@ This archive is a snapshot from our CVS repository. <ul> <li> gzip'ed tar file: <!-- WARNING! Line below automatically edited by makefile. --> - <?php download_link("ProofGeneral-3.4pre020718-devel.tar.gz") ?> + <?php download_link("ProofGeneral-3.4pre020719-devel.tar.gz") ?> <!-- End Warning. --> </li> </ul> @@ -127,7 +127,7 @@ The complete archive also includes: (see <a href="devel#lowleveltodo">the developers page</a>) and the detailed <!-- WARNING! Line below automatically edited by makefile. --> - <?php fileshow("ProofGeneral-3.4pre020718/ChangeLog","ChangeLog"); ?>, + <?php fileshow("ProofGeneral-3.4pre020719/ChangeLog","ChangeLog"); ?>, <!-- End Warning. --> </li> <li> developer's Makefile used to generate documentation files |