diff options
| -rw-r--r-- | INSTALL | 48 | ||||
| -rw-r--r-- | bin/proofgeneral | 6 | ||||
| -rw-r--r-- | demoisa/demoisa.el | 205 | ||||
| -rw-r--r-- | html/download.html | 35 | ||||
| -rw-r--r-- | isa/Example.ML | 123 | ||||
| -rw-r--r-- | todo | 2 |
6 files changed, 204 insertions, 215 deletions
@@ -31,8 +31,10 @@ When you load a file with one of these extensions, the corresponding Proof General mode will be entered. In case of difficulty, please check the documentation in doc/, the -notes below, and the file BUGS. If this doesn't help, then contact us -via the address below. +notes below, the README file for each prover, and the file BUGS. + +If none of these files t help, then contact us via the address below. + - David Aspinall. @@ -160,44 +162,4 @@ Emacs 20.x and XEmacs. ----------------------------------------------------------------------- - -Notes for Coq -============= - -Check the values of coq-tags and coq-prog-name in coq.el to see that -they correspond to the paths for coqtop and the library on your system. - -Install coqtags in a standard place or add <proof-home>/coq to your PATH. -NB: You may need to change the path to perl at the top of the file. - -If you are running Coq, generate a TAGS file for the library by running - coqtags `find . -name \*.v -print` -in the root directory of the library, $COQTOP/theories. If you are -running LEGO, do the same using legotags in the appropriate directory. - - ----------------------------------------------------------------------- - -Notes for LEGO -============== - -Install legotags in a standard place or add <proofgeneral-home>/lego -to your PATH. -NB: You may need to change the path to perl at the top of the file. - - ----------------------------------------------------------------------- - -Notes for Isabelle and Isabelle/Isar -==================================== - -Check the value of isabelle-prog-name. - -If you use the interface wrapper scripts isa/interface or -isar/interface, you may need to change the path to bash -on the first line. - -The distribution includes a version of Isamode's theory file mode. -Use C-h m to check on the features available. - +$Id$ diff --git a/bin/proofgeneral b/bin/proofgeneral index dec54b8b..92b029f1 100644 --- a/bin/proofgeneral +++ b/bin/proofgeneral @@ -10,8 +10,8 @@ # $Id$ # -PGHOME=/usr/share/emacs/ProofGeneral -#PGHOME=~/ProofGeneral +#PGHOME=/usr/share/emacs/ProofGeneral +PGHOME=~/ProofGeneral if which xemacs > /dev/null; then EMACS=xemacs @@ -19,4 +19,4 @@ else EMACS=emacs fi -$EMACS -l $PGHOME/generic/proof-site.el -f proof-splash-display-screen "$@" +$EMACS -q -l $PGHOME/generic/proof-site.el -f proof-splash-display-screen "$@" diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el index 1740a100..8b1c76d8 100644 --- a/demoisa/demoisa.el +++ b/demoisa/demoisa.el @@ -1,4 +1,4 @@ -;; demoisa.el Example Proof General instance for Isabelle +;; demoisa-easy.el Example Proof General instance for Isabelle ;; ;; Copyright (C) 1999 LFCS Edinburgh. ;; @@ -6,152 +6,57 @@ ;; ;; $Id$ ;; -;; ================================================================= -;; -;; See README in this directory for an introduction. -;; -;; Basic configuration is controlled by one line in `proof-site.el'. -;; It has this line in proof-assistant-table: -;; -;; (demoisa "Isabelle Demo" "\\.ML$") -;; -;; From this it loads this file "demoisa/demoisa.el" whenever -;; a .ML file is visited, and sets the mode to `demoisa-mode' -;; (defined below). -;; -;; I've called this instance "Isabelle Demo Proof General" just to -;; avoid confusion with the real "Isabelle Proof General" in case the -;; demo gets loaded by accident. -;; -;; To make the line above take precedence over the real Isabelle mode -;; later in the table, set PROOFGENERAL_ASSISTANTS=demoisa in the -;; shell before starting Emacs (or customize proof-assistants). -;; - - -(require 'proof) ; load generic parts - - -;; ======== User settings for Isabelle ======== -;; -;; Defining variables using customize is pretty easy. -;; You should do it at least for your prover-specific user options. -;; -;; proof-site provides us with two customization groups -;; automatically: (based on the name of the assistant) -;; -;; 'isabelledemo - User options for Isabelle Demo Proof General -;; 'isabelledemo-config - Configuration of Isabelle Proof General -;; (constants, but may be nice to tweak) -;; -;; The first group appears in the menu -;; ProofGeneral -> Customize -> Isabelledemo -;; The second group appears in the menu: -;; ProofGeneral -> Internals -> Isabelledemo config -;; - -(defcustom isabelledemo-prog-name "isabelle" - "*Name of program to run Isabelle." - :type 'file - :group 'isabelledemo) - -(defcustom isabelledemo-web-page - "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html" - "URL of web page for Isabelle." - :type 'string - :group 'isabelledemo-config) - - -;; -;; ======== Configuration of generic modes ======== -;; - -(defun demoisa-config () - "Configure Proof General scripting for Isabelle." - (setq - proof-terminal-char ?\; ; ends every command - proof-comment-start "(*" - proof-comment-end "*)" - proof-goal-command-regexp "^Goal" - proof-save-command-regexp "^qed" - proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" - proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" - proof-non-undoables-regexp "undo\\|back" - proof-undo-n-times-cmd "pg_repeat undo %s;" - proof-showproof-command "pr()" - proof-goal-command "Goal \"%s\";" - proof-save-command "qed \"%s\";" - proof-kill-goal-command "Goal \"PROP no_goal_set\";" - proof-assistant-home-page isabelledemo-web-page - proof-auto-multiple-files t)) - - -(defun demoisa-shell-config () - "Configure Proof General shell for Isabelle." - (setq - proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?ML>? " - proof-shell-cd-cmd "cd \"%s\"" - proof-shell-prompt-pattern "[ML-=#>]+>? " - proof-shell-interrupt-regexp "Interrupt" - proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " - proof-shell-start-goals-regexp "Level [0-9]" - proof-shell-end-goals-regexp "val it" - proof-shell-proof-completed-regexp "^No subgoals!" - proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" - proof-shell-init-cmd ; define a utility function, in a lib somewhere? - "fun pg_repeat f 0 = () - | pg_repeat f n = (f(); pg_repeat f (n-1));" - proof-shell-quit-cmd "quit();")) - - - -;; -;; ======== Defining the derived modes ======== -;; - -;; The name of the script mode is always <proofsym>-script, -;; but the others can be whatever you like. -;; -;; The derived modes set the variables, then call the -;; <mode>-config-done function to complete configuration. - -(define-derived-mode demoisa-mode proof-mode - "Isabelle Demo script" nil - (demoisa-config) - (proof-config-done)) - -(define-derived-mode demoisa-shell-mode proof-shell-mode - "Isabelle Demo shell" nil - (demoisa-shell-config) - (proof-shell-config-done)) - -(define-derived-mode demoisa-response-mode proof-response-mode - "Isabelle Demo response" nil - (proof-response-config-done)) - -(define-derived-mode demoisa-goals-mode proof-goals-mode - "Isabelle Demo goals" nil - (proof-goals-config-done)) - -;; The response buffer and goals buffer modes defined above are -;; trivial. In fact, we don't need to define them at all -- they -;; would simply default to "proof-response-mode" and "pbp-mode". - -;; A more sophisticated instantiation might set font-lock-keywords to -;; add highlighting, or some of the proof by pointing markup -;; configuration for the goals buffer. - -;; The final piece of magic here is a hook which configures settings -;; to get the proof shell running. Proof General needs to know the -;; name of the program to run, and the modes for the shell, response, -;; and goals buffers. - -(add-hook 'proof-pre-shell-start-hook 'demoisa-pre-shell-start) - -(defun demoisa-pre-shell-start () - (setq proof-prog-name isabelledemo-prog-name) - (setq proof-mode-for-shell 'demoisa-shell-mode) - (setq proof-mode-for-response 'demoisa-response-mode) - (setq proof-mode-for-goals 'demoisa-goals-mode)) - -(provide 'demoisa) +;; This is an alternative version of demoisa.el which uses the +;; proof-easy-config macro to do the work of declaring derived modes, +;; etc. +;; +;; This mechanism is in fact recommended for new instantiations of +;; Proof General since it follows a regular pattern, and we can more +;; easily adapt it in the future to new versions of Proof General. +;; It is easy to augment with additional elisp functions and +;; other settings. +;; +;; See demoisa.el and the Adapting Proof General manual for more +;; documentation. +;; +;; To test this file you must rename it demoisa.el. +;; + +(require 'proof-easy-config) ; easy configure mechanism + +(proof-easy-config + 'demoisa "Isabelle Demo" + proof-prog-name "isabelle" + proof-terminal-char ?\; + proof-comment-start "(*" + proof-comment-end "*)" + proof-goal-command-regexp "^Goal" + proof-save-command-regexp "^qed" + proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" + proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" + proof-non-undoables-regexp "undo\\|back" + proof-goal-command "Goal \"%s\";" + proof-save-command "qed \"%s\";" + proof-kill-goal-command "Goal \"PROP no_goal_set\";" + proof-showproof-command "pr()" + proof-undo-n-times-cmd "pg_repeat undo %s;" + proof-auto-multiple-files t + proof-shell-cd-cmd "cd \"%s\"" + proof-shell-prompt-pattern "[ML-=#>]+>? " + proof-shell-interrupt-regexp "Interrupt" + proof-shell-start-goals-regexp "Level [0-9]" + proof-shell-end-goals-regexp "val it" + proof-shell-quit-cmd "quit();" + proof-assistant-home-page + "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" + proof-shell-annotated-prompt-regexp + "^\\(val it = () : unit\n\\)?ML>? " + proof-shell-error-regexp + "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " + proof-shell-init-cmd + "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));" + proof-shell-proof-completed-regexp "^No subgoals!" + proof-shell-eager-annotation-start + "^\\[opening \\|^###\\|^Reading") + +(provide 'demoisa)
\ No newline at end of file diff --git a/html/download.html b/html/download.html index 19cc10fb..407d8ce1 100644 --- a/html/download.html +++ b/html/download.html @@ -8,7 +8,7 @@ If you have already registered you do not need to do so again. <p> The statistics collected from registrations will be used to help a case for support for Proof General, and nothing else. It is likely -that development of Proof General will <i>finish very soon</i> unless +that development of Proof General will <i>finish soon</i> unless we can find new resources. As a courtesy, we do not make registration compulsory and I can tell from the server logs that the majority of people downloading do not register. But if you don't register @@ -97,9 +97,8 @@ All components mentioned above are distributed under the GPL license. <br> <br> - <h2><a name="stable"> - Proof General Version 3.2, released 2nd October 2000 + Proof General Version 3.3, released 5th September 2001 </a> </h2> @@ -108,20 +107,17 @@ Proof General is available as an archive and an RPM package. </p> <ul> <li> gzip'ed tar file: - <?php download_link("ProofGeneral-3.2.tar.gz") ?>, + <?php download_link("ProofGeneral-3.3.tar.gz") ?>, <br> or the same thing in a zip file: - <?php download_link("ProofGeneral-3.2.zip") ?>, + <?php download_link("ProofGeneral-3.3.zip") ?>. </li> <li> Linux RPM package: - <?php download_link("ProofGeneral-3.2-1.noarch.rpm") ?> + <?php download_link("ProofGeneral-3.3-1.noarch.rpm") ?> <br> - You probably don't need the - <?php download_link("ProofGeneral-3.2-1.src.rpm", - "source RPM") ?>. </li> <li> individual files: - <a href="ProofGeneral-3.2">browse the package here</a>. + <a href="ProofGeneral-3.3">browse the package here</a>. </li> </tr> @@ -140,16 +136,19 @@ you may like to download the <?php download_link("ProofGeneralPortrait.eps.gz", "front page image") ?>. </p> - +<p> +We no longer offer a SRPM, since you can now build the RPM directly +from the source tarball using <tt>rpm -ta</tt>. +</p> <p> This version of Proof General has been tested -with XEmacs 21.1 and (briefly with) FSF Emacs 20.7. -It supports Coq version 6.3, LEGO version 1.3.1 and -Isabelle99-1. +with XEmacs 21.4 and (briefly with) FSF Emacs 20.7. +It supports earlier versions of both Emacsen, but +we recommend using the latest versions availab.e </p> <p> -Check the <?php fileshow("ProofGeneral-3.2/CHANGES","CHANGES"); ?> file -for a summary of changes since version 3.1. +Check the <?php fileshow("ProofGeneral-3.3/CHANGES","CHANGES"); ?> file +for >a summary of changes since version 3.2. </p> <p> Check the latest <?php fileshow("ProofGeneral/BUGS","BUGS"); ?> file @@ -171,7 +170,7 @@ please To use Proof General, simply unpack the sources with </p> <blockquote> - <tt>tar xpzf ProofGeneral-3.2.tar.gz</tt> + <tt>tar xpzf ProofGeneral-3.3.tar.gz</tt> </blockquote> <p> (use <tt>gunzip</tt> first in place of <tt>z</tt> if you don't have @@ -197,7 +196,7 @@ Use a zip file utility to unpack it somewhere, for example Further customization is possible via the Customize menus in Emacs. <br> -See the <?php fileshow("ProofGeneral-3.2/INSTALL","INSTALL")?> +See the <?php fileshow("ProofGeneral-3.3/INSTALL","INSTALL")?> file in the distribution for more details. </p> diff --git a/isa/Example.ML b/isa/Example.ML index c607390f..b1ad1ee2 100644 --- a/isa/Example.ML +++ b/isa/Example.ML @@ -12,3 +12,126 @@ Goal "A & B --> B & A"; by (assume_tac 1); qed "and_comms"; + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms2"; + + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms3"; + + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms8"; + + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms"; + + +Goal "A & B --> B & A"; + by (rtac impI + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms3"; + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms"; + + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms"; + + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms3"; + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms"; + + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms"; + + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms3"; + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms"; + + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms"; + + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); +qed "and_comms3"; + @@ -46,7 +46,7 @@ X (Low) e.g. probably not worth spending time on processing of files in major or auxiliary file types. E.g. twelf ACL2 -*** B Move 3.3 over to new better designed parsing function mechanism. +*** B Move over to new better designed parsing function mechanism. *** C ChangeLog generation still not right. Suggested fix: use the prefix that rcs2log generates, without prepending. |