diff options
| -rw-r--r-- | AUTHORS | 2 | ||||
| -rw-r--r-- | INSTALL | 2 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 30 | ||||
| -rw-r--r-- | etc/README | 11 | ||||
| -rw-r--r-- | etc/mailinglist-bait | 28 | ||||
| -rw-r--r-- | etc/testing-log.txt | 4 |
6 files changed, 50 insertions, 27 deletions
@@ -1,7 +1,7 @@ Current Authors/Maintainers: David Aspinall <da@dcs.ed.ac.uk> - doc, etc, generic, html, images, isa + doc, etc, generic, html, images, isa, demoisa Markus Wenzel <wenzelm@informatik.tu-muenchen.de> isar Paul Callaghan <P.C.Callaghan@durham.ac.uk> @@ -26,6 +26,8 @@ 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. + - David Aspinall. + Proof General maintainer <proofgen@dcs.ed.ac.uk> LFCS, diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 2dd0dbd2..3b160640 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1544,9 +1544,17 @@ menu version 2.63, which suggests the following code for your (we have found that the extra @code{t} argument to @code{add-hook} may be important although it isn't suggested in @file{func-menu.el}). + If you have another version of Emacs, you should check the @file{func-menu.el} (or @file{fume-func.el}) file supplied with it. +FSF Emacs 20.4 does not have the function menu library built in, but you +may be able to download it from the elisp archives. A similar mode +which is supported is @code{imenu}, also in XEmacs. Proof General would +be grateful if anyone can send patches for using @code{imenu} +as an alternative to function menu. + + @node Support for outline mode @section Support for outline mode @cindex outline mode @@ -1947,7 +1955,7 @@ information about what Proof General is doing. To avoid erasing the messages shortly after they're printed, you should set @samp{@code{proof-tidy-response}} to nil. -The default value is @code{t}. +The default value is @code{nil}. @end defopt @@ -4163,7 +4171,7 @@ scripting. @code{proof-assert-next-command} is a variant of this function. @c TEXI DOCSTRING MAGIC: proof-assert-next-command -@defun proof-assert-next-command &optional unclosed-comment-fun ignore-proof-process-p dont-move-forward for-new-command +@deffn Command proof-assert-next-command &optional unclosed-comment-fun ignore-proof-process-p dont-move-forward for-new-command Process until the end of the next unprocessed command after point.@* If inside a comment, just process until the start of the comment. @@ -4172,7 +4180,7 @@ If @var{ignore-proof-process-p} is set, no commands will be added to the queue. Afterwards, move forward to near the next command afterwards, unless @var{dont-move-forward} is non-nil. If @var{for-new-command} is non-nil, a space or newline will be inserted automatically. -@end defun +@end deffn The main command for retracting parts of a script is @code{proof-retract-until-point}. @@ -4410,7 +4418,7 @@ Input is actually inserted into the shell buffer and sent to the process by the low-level function @code{proof-shell-insert}. @c TEXI DOCSTRING MAGIC: proof-shell-insert -@defun proof-shell-insert string action +@defun proof-shell-insert string &optional action Insert @var{string} at the end of the proof shell, call @code{comint-send-input}. First call @code{proof-shell-insert-hook}. The argument @var{action} may be @@ -4577,7 +4585,7 @@ information about what Proof General is doing. To avoid erasing the messages shortly after they're printed, you should set @samp{@code{proof-tidy-response}} to nil. -The default value is @code{t}. +The default value is @code{nil}. @end defopt For more information about debugging Emacs lisp, consult the Emacs Lisp @@ -4732,14 +4740,14 @@ you're doing. Compilation of the Emacs lisp files improves efficiency but can sometimes cause compatibility problems, especially if you use more than -one version of Emacs at the same time. Furthermore, we develop Proof -General with source files so may miss problems with the byte compiled -versions. If you discover problems using the byte-compiled @code{.elc} -files which aren't present using the source @code{.el} files, please -report them to us. +one version of Emacs with the same @code{.elc} files. Furthermore, we +develop Proof General with source files so may miss problems with the +byte compiled versions. If you discover problems using the +byte-compiled @code{.elc} files which aren't present using the source +@code{.el} files, please report them to us. You can compile Proof General by typing @code{make} in the directory -where you installed it. +where you installed it. @unnumberedsubsec Site-wide installation @@ -9,9 +9,18 @@ announce Announcement lego Files for testing LEGO Proof General isa Isabelle Proof General isar Isar PG +demoisa Isabelle Demo PG + README this file example test protocol for example proof scripts -notes.txt Misc notes
\ No newline at end of file +notes.txt Misc notes + +debugging-tips.txt Notes on debugging +profiling.txt profiling + +testing-log.txt Notes on tests carried out + +release-log.txt A record of official releases
\ No newline at end of file diff --git a/etc/mailinglist-bait b/etc/mailinglist-bait index 395e67d4..6fa15b9c 100644 --- a/etc/mailinglist-bait +++ b/etc/mailinglist-bait @@ -2,27 +2,27 @@ Dear Proof General users, This is a newsy note to tell you that Proof General 3.0 is ready for release Very Soon Now. In the meantime, I'd be very grateful to -anyone who can test a pre-release and tell me how it goes. (I try to -do as much testing as I can, but it's getting more difficult as more -proof assistants are supported). +anyone who can test a pre-release and tell me how it goes. I'm quite excited about this release. I've concentrated on usability, making the code clean and robust, and making PG easier to adapt for new proof assistants. But there are some important new features too... -David von Oheimb's patches for X-Symbol have been made generic now, -and easy to turn on and off. I've added some basic support for Coq -and LEGO, so Greek letters and symbols like /\ and -> display as you -would like. Break free from ASCII! +David von Oheimb's patches for X-Symbol have been made a proper +generic part of Proof General now, and easy to turn on and off. +I've added some basic support for Coq and LEGO, so Greek letters and +symbols like /\ and -> display as you would like. Break free +from ASCII! -Proof-by-pointing has been resurrected! The interface relies on the +Proof-by-pointing has been resurrected. The interface relies on the proof assistant to construct the proof commands, and the only prover -supported currently LEGO. One reason PBP was disabled was that LEGO's -implementation is experimental and incomplete. But I hope that people -can see PBP almost working in LEGO and be encouraged to implement it -for other provers. We can certainly hope for support in Coq, since -the CtCoq proof-by-pointing code has been moved into the Coq kernel -now. I hope the Coq community can encourage somebody to do this. +supported currently is LEGO. One reason PBP was disabled was that +LEGO's implementation is experimental and incomplete. But I hope that +people can see PBP almost working in LEGO and be encouraged to +implement it for other provers. We can certainly hope for support in +Coq, since the CtCoq proof-by-pointing code has been moved into the +Coq kernel now. I hope the Coq community can encourage somebody to do +this. Visit http://zermelo.dcs.ed.ac.uk/~proofgen/ for more. diff --git a/etc/testing-log.txt b/etc/testing-log.txt index 08528479..2010c27f 100644 --- a/etc/testing-log.txt +++ b/etc/testing-log.txt @@ -1,3 +1,7 @@ +Wed Nov 17 13:43:11 GMT 1999 + + Tested compiled version. Seems to work well for XEmacs! + Tue Nov 16 15:28:51 GMT 1999 Tested automatic multiple file handling: see etc/demoisa |