diff options
Diffstat (limited to 'etc')
79 files changed, 2755 insertions, 0 deletions
diff --git a/etc/ProofGeneral.menu b/etc/ProofGeneral.menu new file mode 100644 index 00000000..5f1022cd --- /dev/null +++ b/etc/ProofGeneral.menu @@ -0,0 +1,7 @@ +?package(ProofGeneral):\ + needs=X11\ + section="Applications/Sciences/Computer science"\ + title="Proof General"\ + longtitle="A generic interface for interactive theorem provers"\ + command="/usr/bin/proofgeneral"\ + icon="pgicon.png" diff --git a/etc/ProofGeneral.spec b/etc/ProofGeneral.spec new file mode 100644 index 00000000..89605785 --- /dev/null +++ b/etc/ProofGeneral.spec @@ -0,0 +1,110 @@ +Summary: Proof General, Emacs interface for Proof Assistants +Name: ProofGeneral +Version: 3.4pre020214 +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.4pre020214.tar.gz +BuildRoot: /tmp/ProofGeneral-root +PreReq: /sbin/install-info +Prefixes: /usr/share/emacs /usr/bin /usr/info +BuildArchitectures: noarch + +%description +Proof General is a generic Emacs interface for proof assistants, +suitable for use by pacifists and Emacs militants alike. +It is supplied ready-customized for LEGO, Coq, and Isabelle. +You can adapt Proof General to other proof assistants if you know a +little bit of Emacs Lisp. + +To use Proof General, use the command `proofgeneral', which launches +XEmacs (or Emacs) for you, or add the line: + + (load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el") + +to your .emacs file so Proof General is available whenever +you run Emacs. + +%changelog +* Fri May 4 2001 David Aspinall <da@dcs.ed.ac.uk> +- Changelog in CVS now; official spec file developed with source. + +%prep +%setup + +%build +[ -n "${RPM_BUILD_ROOT}" ] && rm -rf ${RPM_BUILD_ROOT} + +%install +mkdir -p ${RPM_BUILD_ROOT}/usr/share/emacs/ProofGeneral + +# Put binaries in proper place +mkdir -p ${RPM_BUILD_ROOT}/usr/bin +mv bin/proofgeneral lego/legotags coq/coqtags ${RPM_BUILD_ROOT}/usr/bin + +# Put info file in proper place, compress it. +mkdir -p ${RPM_BUILD_ROOT}/usr/info +mv doc/ProofGeneral.info doc/ProofGeneral.info-* ${RPM_BUILD_ROOT}/usr/info +mv doc/PG-adapting.info doc/PG-adapting.info-* ${RPM_BUILD_ROOT}/usr/info +gzip ${RPM_BUILD_ROOT}/usr/info/ProofGeneral.info ${RPM_BUILD_ROOT}/usr/info/ProofGeneral.info-* +gzip ${RPM_BUILD_ROOT}/usr/info/PG-adapting.info ${RPM_BUILD_ROOT}/usr/info/PG-adapting.info-* +# Remove duff bits +rm -f doc/dir doc/localdir + +# Put icons and menu entry into suitable place (at least for Mandrake) +mkdir -p ${RPM_BUILD_ROOT}/usr/share/icons/mini +cp images/pgmini.xpm ${RPM_BUILD_ROOT}/usr/share/icons/mini +cp images/pgicon.png ${RPM_BUILD_ROOT}/usr/share/icons +mkdir -p ${RPM_BUILD_ROOT}/usr/lib/menu +mv etc/ProofGeneral.menu ${RPM_BUILD_ROOT}/usr/lib/menu/ProofGeneral + +cp -pr phox acl2 twelf coq lego isa isar hol98 images generic ${RPM_BUILD_ROOT}/usr/share/emacs/ProofGeneral + +%clean +if [ "X" != "${RPM_BUILD_ROOT}X" ]; then + rm -rf $RPM_BUILD_ROOT +fi + +%post +/sbin/install-info /usr/info/ProofGeneral.info.* /usr/info/dir +/sbin/install-info /usr/info/PG-adapting.info.* /usr/info/dir + +%preun +/sbin/install-info --delete /usr/info/ProofGeneral.info.* /usr/info/dir +/sbin/install-info --delete /usr/info/PG-adapting.info.* /usr/info/dir + +%files +%attr(-,root,root) %doc AUTHORS BUGS CHANGES COPYING INSTALL README README.devel REGISTER doc/* */README +%attr(-,root,root) /usr/info/ProofGeneral.info.* +%attr(-,root,root) /usr/info/ProofGeneral.info-*.* +%attr(-,root,root) /usr/info/PG-adapting.info.* +%attr(-,root,root) /usr/info/PG-adapting.info-*.* +%attr(-,root,root) /usr/bin/proofgeneral +%attr(-,root,root) /usr/bin/coqtags +%attr(-,root,root) /usr/bin/legotags +%attr(-,root,root) /usr/share/icons/pgicon.png +%attr(-,root,root) /usr/share/icons/mini/pgmini.xpm +%attr(-,root,root) /usr/lib/menu/ProofGeneral +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral/images +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral/generic +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral/coq +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral/lego +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral/isa +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral/isar +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral/hol98 +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral/phox +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral/acl2 +%attr(0755,root,root) %dir /usr/share/emacs/ProofGeneral/twelf +%attr(-,root,root) /usr/share/emacs/ProofGeneral/images/* +%attr(-,root,root) /usr/share/emacs/ProofGeneral/generic/* +%attr(-,root,root) /usr/share/emacs/ProofGeneral/coq/* +%attr(-,root,root) /usr/share/emacs/ProofGeneral/lego/* +%attr(-,root,root) /usr/share/emacs/ProofGeneral/isa/* +%attr(-,root,root) /usr/share/emacs/ProofGeneral/isar/* +%attr(-,root,root) /usr/share/emacs/ProofGeneral/hol98/* +%attr(-,root,root) /usr/share/emacs/ProofGeneral/phox/* +%attr(-,root,root) /usr/share/emacs/ProofGeneral/acl2/* +%attr(-,root,root) /usr/share/emacs/ProofGeneral/twelf/* diff --git a/etc/README b/etc/README new file mode 100644 index 00000000..2e88cdf6 --- /dev/null +++ b/etc/README @@ -0,0 +1,31 @@ +Files in this directory (not all part of standard distribution - some only in devel) +===================================================================================== + +ProofGeneral.spec For building the Proof General RPM. + Use "rpm -tb" to build from tarball. + +ProofGeneral.menu Menu file for some Linux versions. + Install in /usr/lib/menu. + +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 + +bug-notes.txt Test cases for Emacs or PG bugs +cvs-tips.txt Notes on cvs with PG project +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/TESTS b/etc/TESTS new file mode 100644 index 00000000..222e5958 --- /dev/null +++ b/etc/TESTS @@ -0,0 +1,95 @@ +Some test cases for Proof General. +================================== + +See testing-log.txt for log of tests conducted. +Please add to that file! + + +22.3.00 FILENAME ESCAPES PROBLEM [All provers, probably] +======================================================== + + Filename substitution %s in settings including proof-shell-cd-cmd, + proof-shell-inform-file-{retracted,processed}-cmd, may need + to add escape characters peculiar to the proof assistant syntax. + + Test cases: + + ln -s ProofGeneral \\backslash + ln -s ProofGeneral \"quote + + Then try scripting with example files for each prover, + i.e. \"quote/coq/example.v, etc. + + +1.2.99 FILE RECOGNITION PROBLEM [Isabelle] +=========================================== + + Bug in regexp caused ML files to be recognized as + theory files when "thy" appeared in path. + Test case in etc/isa/thy/test.ML. + + +15.1.99 LONG-LINE AND BACKSLASH PROBLEM ON SOLARIS +=================================================== + + Test that etc/isa/long-line-backslash.ML can be processed + successfully. + + +16.12.98 KILLING THE PROOF PROCESS +================================== + + Process some proof script buffer. Invoke + + M-x proof-shell-exit + + Process should exit cleanly. + +11.12.98 RUDELY KILLING THE ACTIVE SCRIPTING BUFFER +==================================================== + + Start scripting with some buffer, after + having processed another buffer. + + Kill it when scripting is only partly finished. + + Scripting should be cleanly turned off and it + should be possible to resume retraction in the + first buffer. + + Moreover, this ensures that if the file is on the included + files list, yet has been only partly processed (e.g. because + Undo steps were taken), then it will be retracted and + removed from the included files list. + + FIXME: Using C-x C-v to revert to saved version doesn't + seem to work because it renames the buffer or something. + +8.12.98 INHIBIT VARIABLES +========================== + + Test with proof-splash-inhibit=t + + Test with proof-toolbar-inhibit=t + + +8.12.98 SCRIPTING FOR BUFFERS WITHOUT FILES. +============================================= + + Switch to a fresh buffer FOO which doesn't visit a file. + Do M-x isa-mode RET. + Should succeed. + Try asserting commands, e.g. Goal "P-->P"; + + Switch to another fresh buffer BAR, turn on isa-mode. + Should succeed again. + Try asserting commands here, e.g. Goal "Q&Q --> Q"; + Should give error "Cannot have more than one active scripting buffer". + + Exit emacs. Should query whether we want to save these + scripting buffers (maybe XEmacs only). + + + + + diff --git a/etc/announce b/etc/announce new file mode 100644 index 00000000..1dbda9ff --- /dev/null +++ b/etc/announce @@ -0,0 +1,78 @@ +To: coq-club@pauillac.inria.fr, + isabelle-users@cl.cam.ac.uk, + lego-club@dcs.ed.ac.uk, + uitp@dcs.gla.ac.uk, + bra-types@cs.chalmers.se, + info-hol@leopard.cs.byu.edu, + pvs@csl.sri.com, + qed@mcs.anl.gov, + theorem-provers@ai.mit.edu, + types@cis.upenn.edu, + formal-methods@cs.uidaho.edu, + reliable_computing@interval.usl.edu, + prog-lang@diku.dk + + Also newsgroups: + comp.lang.ml + comp.lang.functional + gnu.emacs.sources + comp.emacs.xemacs + comp.os.linux.announce + freshmeat.net + +tag for comp.lang.ml, comp.lang.functional: + +[Posted here because ML and functional languages generally are + traditional for implementing interactive theorem provers. + Implementors of such systems may be interested in Proof General. + Apologies for multiple copies] + + + + +Subject: Proof General --- Version 3.3 release + + Announcing Proof General Version 3.3 + A Generic Emacs interface for Interactive Proof Assistants + http://www.proofgeneral.org + + contact: David Aspinall <da@proofgeneral.org> + +Proof General is a generic (X)Emacs interface for proof assistants. +It can be instantiated for the proof assistant of your choice, and is +supplied ready-customised for Isabelle, Coq, LEGO, and PhoX, and, +experimentally, for HOL, Twelf, and ACL2. + +Proof General includes these features, amongst others: + +. Script management: proof assistant state reflected in editor +. Toolbar and menus: commands for building and replaying proofs +. Syntax highlighting of proof scripts and prover output; hiding proofs +. Display of real logical symbols, greek letters, etc +. Simplified communication: proof assistant verbosity hidden +. Menu for jumping to theorems in a proof script +. Provision to easily run proof assistant on a remote host +. Works on any platform Emacs does, in window system or plain console + +Summary of changes since 3.2: + +. Visibility control for completed proofs +. Dependency browsing/highlighting (currently Isabelle only) +. Bug fixes +. Compatibility improvements: XEmacs 21.4, Coq 7, Windows + +For details of changes since 3.2, see +http://www.proofgeneral.org/fileshow.php?file=ProofGeneral-3.3%2FCHANGES + +For the latest user manual, see http://www.proofgeneral.org/doc + +Proof General needs a recent version of Emacs to run with, and it much +prefers XEmacs to FSF GNU Emacs. Proof General 3.3 has been tested +with XEmacs 21.4 and Emacs 20.7. (It may work back to XEmacs 20.4 and +Emacs 20.2, though). + +Installing Proof General is easy. Why not give it a try? + + - David Aspinall <da@dcs.ed.ac.uk> + September 2001. + diff --git a/etc/bug-notes.txt b/etc/bug-notes.txt new file mode 100644 index 00000000..c4aaf21d --- /dev/null +++ b/etc/bug-notes.txt @@ -0,0 +1,48 @@ +-*- outline -*- + +$Id$ + +Test cases for PG and/or Emacs bugs. + +---------------- + +* Coq, and others bug: synchronization not gained until second line. + +Test in Coq buffer: + + Print foo. + +Should give error, but PG ignores it and colours command blue. +Similar errors for some other provers. + +[ Now fixed in 3.2pre ] + + + + +---------------- + +* XEmacs bug: buffer-syntactic-context-depth returns weird values + +Seems to depend on previous history. Test in Coq buffer: + + X + (* comment one *) + Y + (* comment two *) + Z + +Evaluate (buffer-syntactic-context-depth) at X, Y, then Z. +Values 0, 1, 2. Evaluate at point Y. Now get 0. +Perhaps caches previous value, and bases parse on moving point +forwards from previous value? Anyway, doesn't do well with +block comments. Also bad with line comments, use same test +case with buffer in lisp mode, except with lisp comments. + +Shame, would be nice to use this to help parse lisp-like +syntax for PAs, fitting in with present scheme. + + + + + diff --git a/etc/coq/multiple/.cvsignore b/etc/coq/multiple/.cvsignore new file mode 100644 index 00000000..41995687 --- /dev/null +++ b/etc/coq/multiple/.cvsignore @@ -0,0 +1 @@ +*.vo diff --git a/etc/coq/multiple/README b/etc/coq/multiple/README new file mode 100644 index 00000000..48f64110 --- /dev/null +++ b/etc/coq/multiple/README @@ -0,0 +1,27 @@ +New in 3.3: experimental proper handling of multiple files. + Not expected to be robust, see comments in coq.el + Should be improved for new versions of Coq 7, I hope! + Test also for automatic compilation. + +Expected behaviour: + + 1) At the end of scripting foo.v (i.e. when activing scripting is + switched off), "Reset Initial. Compile Module <foo>" is + automatically issued. This clears the context and writes a .vo file, + to keep your .vo files up to date. It means that when using PG Coq, + you should use the correct commands ("Require foo.") to load all + the modules you depend on, so that scripting can continue in the + next file. + + 2) PG tracks file dependencies by noticing "Reinterning" messages + from Coq. When a file "b.v" is processed which has a "Require a", + command, PG will try to find "a.v" and will automatically lock + it. (This part of the process is fragile, for two reasons: it + is hard to find the directory for a.v, since Coq doesn't report + it, and the reinterning message is only issued the first time the + file is reinterned). + + 3) When a file is retracted, PG attempts to automatically unlock + all the dependent files, by issuing a coqdep command to determine + the dependencies. (This is a rather nasty hack, it's hoped for + the future that Coq will support this functionality directly). diff --git a/etc/coq/multiple/a.v b/etc/coq/multiple/a.v new file mode 100644 index 00000000..253db19d --- /dev/null +++ b/etc/coq/multiple/a.v @@ -0,0 +1,11 @@ +(* Simple tests for multiple file handling *) + +Goal (A,B:Prop)(and A B) -> (and B A). +Intros A B H. +Induction H. +Apply conj. +Assumption. +Assumption. +Save and_comms_a. + + diff --git a/etc/coq/multiple/b.v b/etc/coq/multiple/b.v new file mode 100644 index 00000000..55c89b76 --- /dev/null +++ b/etc/coq/multiple/b.v @@ -0,0 +1,11 @@ +(* Simple tests for multiple file handling *) + +Goal (A,B:Prop)(and A B) -> (and B A). +Intros A B H. +Induction H. +Apply conj. +Assumption. +Assumption. +Save and_comms_b. + + diff --git a/etc/coq/multiple/c.v b/etc/coq/multiple/c.v new file mode 100644 index 00000000..490c3250 --- /dev/null +++ b/etc/coq/multiple/c.v @@ -0,0 +1,14 @@ +(* Simple tests for multiple file handling *) + +Require a. +Require b. + +Goal (A,B:Prop)(and A B) -> (and B A). +Intros A B H. +Induction H. +Apply conj. +Assumption. +Assumption. +Save and_comms_c. + + diff --git a/etc/coq/unnamed_thm.v b/etc/coq/unnamed_thm.v new file mode 100644 index 00000000..2bd82b7b --- /dev/null +++ b/etc/coq/unnamed_thm.v @@ -0,0 +1,30 @@ +(* + Test for Unnamed_thm + + $Id$ +*) + +(* Coq calls this "Unamed_thm", so must forget it like any other *) + +(* test: do, undo, then check shell buffer to see "Reset Unnamed_thm" *) + +Goal (A,B:Prop)(and A B) -> (and B A). +Intros A B H. +Induction H. +Apply conj. +Assumption. +Assumption. +Save. + +(* Odd side effect: two unnamed theorems in a row are not possible! *) + +Goal (A,B:Prop)(and A B) -> (and B A). +Intros A B H. +Induction H. +Apply conj. +Assumption. +Assumption. +Save. + + + diff --git a/etc/cvs-tips.txt b/etc/cvs-tips.txt new file mode 100644 index 00000000..495aef3c --- /dev/null +++ b/etc/cvs-tips.txt @@ -0,0 +1,113 @@ +Using CVS to access Proof General repository +============================================ + +Here are some notes on how to access the PG repository remotely +using CVS, using ssh with an account at dcs.ed.ac.uk + + +1. First configure ssh so that you can do `ssh ssh.dcs.ed.ac.uk' +without a password (or passphrase). For this you need to run +ssh-keygen and give an empty passphrase. Then you need to copy +your ~/.ssh/identity.pub at home into ~/.ssh/authorized_keys at +dcs.ed. + +(NB: a more secure alternative would be to use ssh-agent to provide +your passphrase as needed. The point is that you don't want to +keep typing passwords on every CVS command). + +2. The CVS repository for PG is in ~proofgen/src at dcs.ed.ac.uk To +use this, you need to set CVSROOT and CVS_RSH. I use the script below +(the last line isn't essential but makes the settings inside a running +emacs too) + +3. Where you want to develop PG, do: + + cvs checkout ProofGeneral + + Inside the ProofGeneral directory, to retrieve the latest updates, + do: + + cvs update + + To commit some changes to file <filename>, do: + + cvs commit -m"<message here>" <filename> + + +See "man cvs" for (much) more. + +#! /bin/bash +MACHINE=ssh +export CVSROOT=:ext:da@$MACHINE.dcs.ed.ac.uk:/home/proofgen/src +export CVS_RSH=ssh +export EDITOR=gnuclient +gnudoit '(setenv "CVSROOT" ":ext:da@$MACHINE.dcs.ed.ac.uk:/home/proofgen/src")' '(setenv "CVS_RSH" "ssh")' '(message "set environment for CVS to /home/proofgen/src !")' + + + +----------------------------------------------------------------- + +Making a branch to patch a previous release: +============================================ + + cvs checkout -r Release-3-1-3 ProofGeneral + cd ProofGeneral + cvs tag -b Release-3-1-branch + # Drop this repo, has sticky tag for 3-1-3. + cd .. ; cvs release -d ProofGeneral + # Get new one + cvs checkout -r Release-3-1-branch ProofGeneral + cd ProofGeneral + patch ... blah ... + cvs commit ... blah .. + +Then make release as ~proofgen: + + mkdir oldbranch + cd oldbranch + cvs checkout -r Release-3-1-branch ProofGeneral + make devel.releaseall VERSION=3.1 FULLVERSION=3.1.99 + +NB: See warning in Makefile.devel about this (it will +downgrade web pages). + +Then perhaps merge in branch changes into main stream: + + cd projects/proofgen/ProofGeneral + cvs update -jRelease-3-1-branch + +NB: this merging will always create conficts with +$Id$ tags in source. (Is there a way to avoid this?) + + +----------------------------------------------------------------- + +Overriding the CVS/Root setting temporarily: +============================================ + + Use + cvs -d $CVSROOT + +NB: This doesn't alter CVS/Root, but uses NEWROOT in preference. +($CVSROOT does not overide CVS/Root at all). + +Useful command: + + alias cvs='cvs -d $CVSROOT' + +to force this behaviour. + +This is needed to solve "localssh.dcs" versus "ssh.dcs" problem. + + +----------------------------------------------------------------- + +Moving to a new branch +====================== + + find * -path '*/CVS' -prune -o -path 'CVS' -prune -o -print | tr '\n' '\0' | xargs -0 cvs commit -m"Updating branch" -f -r 4.0 + +(The tr is needed because of some nasty filenames, e.g. etc/isa/\backslashname) + + + diff --git a/etc/debugging-tips.txt b/etc/debugging-tips.txt new file mode 100644 index 00000000..a2650754 --- /dev/null +++ b/etc/debugging-tips.txt @@ -0,0 +1,10 @@ +Tips for Debugging Proof General -- David Aspinall, Oct 1999. +-------------------------------- + +Make these settings: + + (setq proof-tidy-response nil) ; response buffer never clears + (setq proof-show-debug-messages t) ; debug messages appear in response buffer + +And use the standard elisp package "edebug" to single-step at source +level, and set breakpoints in code. diff --git a/etc/demoisa/A.ML b/etc/demoisa/A.ML new file mode 100644 index 00000000..69126156 --- /dev/null +++ b/etc/demoisa/A.ML @@ -0,0 +1 @@ +1;
\ No newline at end of file diff --git a/etc/demoisa/B.ML b/etc/demoisa/B.ML new file mode 100644 index 00000000..85fa53ce --- /dev/null +++ b/etc/demoisa/B.ML @@ -0,0 +1 @@ +2;
\ No newline at end of file diff --git a/etc/demoisa/C.ML b/etc/demoisa/C.ML new file mode 100644 index 00000000..33fefea4 --- /dev/null +++ b/etc/demoisa/C.ML @@ -0,0 +1 @@ +3;
\ No newline at end of file diff --git a/etc/demoisa/D.ML b/etc/demoisa/D.ML new file mode 100644 index 00000000..06b33ae0 --- /dev/null +++ b/etc/demoisa/D.ML @@ -0,0 +1 @@ +4;
\ No newline at end of file diff --git a/etc/demoisa/README b/etc/demoisa/README new file mode 100644 index 00000000..be06a076 --- /dev/null +++ b/etc/demoisa/README @@ -0,0 +1,11 @@ +This is a test for automatic multiple file handling. + +Assert each of A.ML, B.ML, C.ML, D.ML in turn. + +Then retract B.ML. + +D.ML and C.ML should be automatically retracted. + +Set proof-tidy-response=nil to track what happens. + + - da. diff --git a/etc/doc-notes.txt b/etc/doc-notes.txt new file mode 100644 index 00000000..0cf83b88 --- /dev/null +++ b/etc/doc-notes.txt @@ -0,0 +1,196 @@ +Developers' Notes about Documentation +------------------------------------- + + + + +* Plan for outline of improved documentation. (Completed) + + Terminology: I suggest "proof mode" should become "proof script + mode", aka "the proof script mode of Proof General". We should + be careful here, e.g. present docs speak of buffers in proof + mode, etc, but no buffer is directly in that mode, which is + confusing to the users, at least! + + 1. Introduction [da] + 1.1 Quick start guide + 1.2 Feature list, xref'd to later chaps. + 1.2 Supported Proof Assistants, xref'd too. + Support for new instances, xref'd to later chaps. + + 2. Basics of script management [da] + + 2.1 What a proof script is + 2.2 Locked region and queue region + 2.3 Script processing commands + 2.4 Toolbar commands + 2.5 Other commands + 2.4 Walkthrough example [maybe in appendix?] + + 3. Advanced script management [done] + 3.1 Proof General's view of processed files + 3.2 Switching between proof scripts + 3.3 Retracting across files + 3.4 Handy hints and tips (e.g. C-c C-b stuff?) + 3.5 Using the proof shell + [ 3.6 Re-synchronizing with the proof assistant - if added ] + + 4. Customizing Proof General [da] + 4.1 Setting user options, what they are: + proof-splash-inhibit + etc. + 4.2 Using proof assistant on another machine + 4.3 Examining configuration settings (xref'd later) + + 5. LEGO Proof General [done] + 5.1 LEGO commands + 5.2 LEGO customizations + + 6. Coq Proof General [anon] + 6.1 Coq commands + 6.2 Coq customizations + + 7. Isabelle Proof General [da] + 7.1 Isabelle commands + 7.2 Isabelle customizations + 7.3 Notes about multiple files + + 8. Adapting Proof General to New Provers [da] + 8.1 Files and directories. Skeleton code. + 8.2 Settings for proof scripts + 8.3 Settings for proof shell + -- Special annotations + + 9. Internals of Proof General. [tms] + 9.1 Proof script mode: + - fontification hacks + - spans in locked region + 9.2 Proof shell mode + - proof-action-list + - proof-shell-exec-loop + - proof-shell-output-filter + - eager annotations + + 10. Credits and history [done] + + APPENDIX + + A. Obtaining and installing the software [da] + B. Known bugs [done] + C. Future ideas and plans [da] + + +********* + +Support for Function Menus + +fume-func is a handy package which makes a menu from the function +declarations in a buffer. Proof General configures fume-func so +that you can quickly jump to particular proofs in a script buffer. + +If you want to use fume-func, you may need to enable it for +yourself. It is distributed with XEmacs (and FSF GNU Emacs) +but by not enabled by default. To enable it you should find +the file func-menu.el and follow the instructions there. +At the time of writing, the current version of XEmacs is 20.4 and +it has these instructions: + +(require 'func-menu) +(define-key global-map 'f8 'function-menu) +(add-hook 'find-file-hooks 'fume-add-menubar-entry) +(define-key global-map "\C-cl" 'fume-list-functions) +(define-key global-map "\C-cg" 'fume-prompt-function-goto) +(define-key global-map '(shift button3) 'mouse-function-menu) +(define-key global-map '(meta button1) 'fume-mouse-function-goto) + +If you have any other version of Emacs, you should check the +fume-func.el file + + + +********* + + +Isabelle with multiple files. + +Proper multiple file support only works for .ML files which are read +via the theory loader, with use_thy. If you want to load .ML files +which aren't associated with theories, it's best to use a dummy +theory, see [Reference to Isabelle manual] + + +***************************************************************** + +Notes for writing a paper describing Proof General +------------------------------------------------- + + +Thesis/introduction +=================== + +As programming languages have evolved, environments for developing and +debugging programs have also improved. However, discounting various +"visual" programming languages, a program is usually still a piece of +text which can be directly edited by a programmer, a situation which +hasn't changed since the early days when VDUs replaced punched cards. + +Similarly, whilst the history of languages for proof assistants is +much shorter, we believe that a proof script, describing the +operations needed to construct a proof, will remain the fundamental +form of input for proof systems. + +... +- interactive proof assistants geared to developing proof scripts + interactively, but may not come with integrated editing support. + Problem of shell-like interaction is that input has to be + tediously reassembled after or during proof to get a successful + proof script. + +- script management [refs] aims to make this process easier. + + + +Aspects of design +================= + +- Generic. Fits inside Emacs architecture. (Compare with comint). + +- Extensive use of Emacs Customization mechanism to make it easy + to set/inspect configuration as well as user-options. + +- Script management with multiple files + + +Seen one proof assistant, use them all +====================================== + +- Same interface for different underlying systems + +- Compare: web technology, where "browsing" works for + different protocols: http, ftp, etc + +- Anyone can use Proof General to browse and replay proofs from + other systems, without needing to know how to invoke + the system, etc. + +- However, proof script language and output remains particular to + each prover. It would be another (interesting) project to attempt to + map input and output into an interchange format for proof systems. + + + +A Specification for a proof assistant interface +=============================================== + +The settings to instantiate Proof General can be seen as a set of +requirements for a proof assistant interface. + + + +Example of API design guidlines +=============================== + +1. Use a different prompt for continued lines during input +communication. Helps parsing output. + + diff --git a/etc/isa/\backslashname/test.ML b/etc/isa/\backslashname/test.ML new file mode 100644 index 00000000..0691e38e --- /dev/null +++ b/etc/isa/\backslashname/test.ML @@ -0,0 +1,11 @@ +(* Scripting here tests quotation mechanism for filenames. *) + +(* At the moment this trips a bug in Isabelle which objects + to filename of this directory. + + Easy way to test for other provers is with a link, + \bizzare \\<rightarrow> ProofGeneral/ then load \bizarre/coq/example.v, etc + +*) + +val a = 1; diff --git a/etc/isa/\backslashname/test.thy b/etc/isa/\backslashname/test.thy new file mode 100644 index 00000000..2ca5331f --- /dev/null +++ b/etc/isa/\backslashname/test.thy @@ -0,0 +1 @@ +test = Pure diff --git a/etc/isa/depends/Fib.ML b/etc/isa/depends/Fib.ML new file mode 100644 index 00000000..eba2f0e0 --- /dev/null +++ b/etc/isa/depends/Fib.ML @@ -0,0 +1,106 @@ +(* Title: HOL/ex/Fib + ID: $Id$ + Author: Lawrence C Paulson + Copyright 1997 University of Cambridge + +Fibonacci numbers: proofs of laws taken from + + R. L. Graham, D. E. Knuth, O. Patashnik. + Concrete Mathematics. + (Addison-Wesley, 1989) +*) + + +(** The difficulty in these proofs is to ensure that the induction hypotheses + are applied before the definition of "fib". Towards this end, the + "fib" equations are not added to the simpset and are applied very + selectively at first. +**) + +Delsimps fib.Suc_Suc; + +val [fib_Suc_Suc] = fib.Suc_Suc; +val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc; + +(*Concrete Mathematics, page 280*) +Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n"; +by (res_inst_tac [("u","n")] fib.induct 1); +(*Simplify the LHS just enough to apply the induction hypotheses*) +by (asm_full_simp_tac + (simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3); +by (ALLGOALS + (asm_simp_tac (simpset() addsimps + ([fib_Suc_Suc, add_mult_distrib, add_mult_distrib2])))); +qed "fib_add"; + + +Goal "fib (Suc n) ~= 0"; +by (res_inst_tac [("u","n")] fib.induct 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc]))); +qed "fib_Suc_neq_0"; + +(* Also add 0 < fib (Suc n) *) +Addsimps [fib_Suc_neq_0, [neq0_conv, fib_Suc_neq_0] MRS iffD1]; + +Goal "0<n ==> 0 < fib n"; +by (rtac (not0_implies_Suc RS exE) 1); +by Auto_tac; +qed "fib_gr_0"; + +(*Concrete Mathematics, page 278: Cassini's identity. + It is much easier to prove using integers!*) +Goal "int (fib (Suc (Suc n)) * fib n) = \ +\ (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \ +\ else int (fib(Suc n) * fib(Suc n)) + #1)"; +by (res_inst_tac [("u","n")] fib.induct 1); +by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2); +by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1); +by (asm_full_simp_tac + (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, + mod_Suc, zmult_int RS sym] @ zmult_ac) 1); +qed "fib_Cassini"; + + + +(** Towards Law 6.111 of Concrete Mathematics **) + +Goal "gcd(fib n, fib (Suc n)) = 1"; +by (res_inst_tac [("u","n")] fib.induct 1); +by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3); +by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc]))); +qed "gcd_fib_Suc_eq_1"; + +val gcd_fib_commute = + read_instantiate_sg (sign_of thy) [("m", "fib m")] gcd_commute; + +Goal "gcd(fib m, fib (n+m)) = gcd(fib m, fib n)"; +by (simp_tac (simpset() addsimps [gcd_fib_commute]) 1); +by (case_tac "m=0" 1); +by (Asm_simp_tac 1); +by (clarify_tac (claset() addSDs [not0_implies_Suc]) 1); +by (simp_tac (simpset() addsimps [fib_add]) 1); +by (asm_simp_tac (simpset() addsimps [add_commute, gcd_non_0]) 1); +by (asm_simp_tac (simpset() addsimps [gcd_non_0 RS sym]) 1); +by (asm_simp_tac (simpset() addsimps [gcd_fib_Suc_eq_1, gcd_mult_cancel]) 1); +qed "gcd_fib_add"; + +Goal "m <= n ==> gcd(fib m, fib (n-m)) = gcd(fib m, fib n)"; +by (rtac (gcd_fib_add RS sym RS trans) 1); +by (Asm_simp_tac 1); +qed "gcd_fib_diff"; + +Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"; +by (res_inst_tac [("n","n")] less_induct 1); +by (stac mod_if 1); +by (Asm_simp_tac 1); +by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq, + not_less_iff_le, diff_less]) 1); +qed "gcd_fib_mod"; + +(*Law 6.111*) +Goal "fib(gcd(m,n)) = gcd(fib m, fib n)"; +by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); +by (Asm_simp_tac 1); +by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1); +by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1); +qed "fib_gcd"; diff --git a/etc/isa/depends/Fib.thy b/etc/isa/depends/Fib.thy new file mode 100644 index 00000000..9272ed8c --- /dev/null +++ b/etc/isa/depends/Fib.thy @@ -0,0 +1,17 @@ +(* Title: ex/Fib + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1997 University of Cambridge + +The Fibonacci function. Demonstrates the use of recdef. +*) + +Fib = Usedepends + Divides + Primes + + +consts fib :: "nat => nat" +recdef fib "less_than" + zero "fib 0 = 0" + one "fib 1 = 1" + Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)" + +end diff --git a/etc/isa/depends/Primes.ML b/etc/isa/depends/Primes.ML new file mode 100644 index 00000000..102419da --- /dev/null +++ b/etc/isa/depends/Primes.ML @@ -0,0 +1,197 @@ +(* Title: HOL/ex/Primes.ML + ID: $Id$ + Author: Christophe Tabacznyj and Lawrence C Paulson + Copyright 1996 University of Cambridge + +The "divides" relation, the greatest common divisor and Euclid's algorithm + +See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992) +*) + +eta_contract:=false; + +(************************************************) +(** Greatest Common Divisor **) +(************************************************) + +(*** Euclid's Algorithm ***) + + +val [gcd_eq] = gcd.simps; + + +val prems = goal thy + "[| !!m. P m 0; \ +\ !!m n. [| 0<n; P n (m mod n) |] ==> P m n \ +\ |] ==> P (m::nat) (n::nat)"; +by (res_inst_tac [("u","m"),("v","n")] gcd.induct 1); +by (case_tac "n=0" 1); +by (asm_simp_tac (simpset() addsimps prems) 1); +by Safe_tac; +by (asm_simp_tac (simpset() addsimps prems) 1); +qed "gcd_induct"; + + +Goal "gcd(m,0) = m"; +by (Simp_tac 1); +qed "gcd_0"; +Addsimps [gcd_0]; + +Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)"; +by (Asm_simp_tac 1); +qed "gcd_non_0"; + +Delsimps gcd.simps; + +Goal "gcd(m,1) = 1"; +by (simp_tac (simpset() addsimps [gcd_non_0]) 1); +qed "gcd_1"; +Addsimps [gcd_1]; + +(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) +Goal "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"; +by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0]))); +by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1); +qed "gcd_dvd_both"; + +bind_thm ("gcd_dvd1", gcd_dvd_both RS conjunct1); +bind_thm ("gcd_dvd2", gcd_dvd_both RS conjunct2); + + +(*Maximality: for all m,n,f naturals, + if f divides m and f divides n then f divides gcd(m,n)*) +Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"; +by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod]))); +qed_spec_mp "gcd_greatest"; + +(*Function gcd yields the Greatest Common Divisor*) +Goalw [is_gcd_def] "is_gcd (gcd(m,n)) m n"; +by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_dvd_both]) 1); +qed "is_gcd"; + +(*uniqueness of GCDs*) +Goalw [is_gcd_def] "[| is_gcd m a b; is_gcd n a b |] ==> m=n"; +by (blast_tac (claset() addIs [dvd_anti_sym]) 1); +qed "is_gcd_unique"; + +(*USED??*) +Goalw [is_gcd_def] + "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"; +by (Blast_tac 1); +qed "is_gcd_dvd"; + +(** Commutativity **) + +Goalw [is_gcd_def] "is_gcd k m n = is_gcd k n m"; +by (Blast_tac 1); +qed "is_gcd_commute"; + +Goal "gcd(m,n) = gcd(n,m)"; +by (rtac is_gcd_unique 1); +by (rtac is_gcd 2); +by (asm_simp_tac (simpset() addsimps [is_gcd, is_gcd_commute]) 1); +qed "gcd_commute"; + +Goal "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"; +by (rtac is_gcd_unique 1); +by (rtac is_gcd 2); +by (rewtac is_gcd_def); +by (blast_tac (claset() addSIs [gcd_dvd1, gcd_dvd2] + addIs [gcd_greatest, dvd_trans]) 1); +qed "gcd_assoc"; + +Goal "gcd(0,m) = m"; +by (stac gcd_commute 1); +by (rtac gcd_0 1); +qed "gcd_0_left"; + +Goal "gcd(1,m) = 1"; +by (stac gcd_commute 1); +by (rtac gcd_1 1); +qed "gcd_1_left"; +Addsimps [gcd_0_left, gcd_1_left]; + + +(** Multiplication laws **) + +(*Davenport, page 27*) +Goal "k * gcd(m,n) = gcd(k*m, k*n)"; +by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); +by (Asm_full_simp_tac 1); +by (case_tac "k=0" 1); + by (Asm_full_simp_tac 1); +by (asm_full_simp_tac + (simpset() addsimps [mod_geq, gcd_non_0, mod_mult_distrib2]) 1); +qed "gcd_mult_distrib2"; + +Goal "gcd(m,m) = m"; +by (cut_inst_tac [("k","m"),("m","1"),("n","1")] gcd_mult_distrib2 1); +by (Asm_full_simp_tac 1); +qed "gcd_self"; +Addsimps [gcd_self]; + +Goal "gcd(k, k*n) = k"; +by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1); +by (Asm_full_simp_tac 1); +qed "gcd_mult"; +Addsimps [gcd_mult]; + +Goal "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m"; +by (subgoal_tac "m = gcd(m*k, m*n)" 1); +by (etac ssubst 1 THEN rtac gcd_greatest 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym]))); +qed "relprime_dvd_mult"; + +Goalw [prime_def] "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1"; +by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1); +by Auto_tac; +qed "prime_imp_relprime"; + +(*This theorem leads immediately to a proof of the uniqueness of factorization. + If p divides a product of primes then it is one of those primes.*) +Goal "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"; +by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime]) 1); +qed "prime_dvd_mult"; + + +(** Addition laws **) + +Goal "gcd(m, m+n) = gcd(m,n)"; +by (res_inst_tac [("n1", "m+n")] (gcd_commute RS ssubst) 1); +by (rtac (gcd_eq RS trans) 1); +by Auto_tac; +by (asm_simp_tac (simpset() addsimps [mod_add_self1]) 1); +by (stac gcd_commute 1); +by (stac gcd_non_0 1); +by Safe_tac; +qed "gcd_add"; + +Goal "gcd(m, n+m) = gcd(m,n)"; +by (asm_simp_tac (simpset() addsimps [add_commute, gcd_add]) 1); +qed "gcd_add2"; + +Goal "gcd(m, k*m+n) = gcd(m,n)"; +by (induct_tac "k" 1); +by (asm_simp_tac (simpset() addsimps [gcd_add, add_assoc]) 2); +by (Simp_tac 1); +qed "gcd_add_mult"; + + +(** More multiplication laws **) + +Goal "gcd(m,n) dvd gcd(k*m, n)"; +by (blast_tac (claset() addIs [gcd_greatest, dvd_trans, + gcd_dvd1, gcd_dvd2]) 1); +qed "gcd_dvd_gcd_mult"; + +Goal "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"; +by (rtac dvd_anti_sym 1); +by (rtac gcd_dvd_gcd_mult 2); +by (rtac ([relprime_dvd_mult, gcd_dvd2] MRS gcd_greatest) 1); +by (stac mult_commute 2); +by (rtac gcd_dvd1 2); +by (stac gcd_commute 1); +by (asm_simp_tac (simpset() addsimps [gcd_assoc RS sym]) 1); +qed "gcd_mult_cancel"; diff --git a/etc/isa/depends/Primes.thy b/etc/isa/depends/Primes.thy new file mode 100644 index 00000000..fac39463 --- /dev/null +++ b/etc/isa/depends/Primes.thy @@ -0,0 +1,33 @@ +(* Title: HOL/ex/Primes.thy + ID: $Id$ + Author: Christophe Tabacznyj and Lawrence C Paulson + Copyright 1996 University of Cambridge + +The Greatest Common Divisor and Euclid's algorithm + +The "simpset" clause in the recdef declaration used to be necessary when the +two lemmas where not part of the default simpset. +*) + +Primes = Main + + + +consts + is_gcd :: [nat,nat,nat]=>bool (*gcd as a relation*) + gcd :: "nat*nat=>nat" (*Euclid's algorithm *) + coprime :: [nat,nat]=>bool + prime :: nat set + +recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)" +(* simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" *) + "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" + +defs + is_gcd_def "is_gcd p m n == p dvd m & p dvd n & + (ALL d. d dvd m & d dvd n --> d dvd p)" + + coprime_def "coprime m n == gcd(m,n) = 1" + + prime_def "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}" + +end diff --git a/etc/isa/depends/Usedepends.ML b/etc/isa/depends/Usedepends.ML new file mode 100644 index 00000000..7557d6e8 --- /dev/null +++ b/etc/isa/depends/Usedepends.ML @@ -0,0 +1,3 @@ +use "~/ProofGeneral/isa/depends.ML"; + + diff --git a/etc/isa/depends/Usedepends.thy b/etc/isa/depends/Usedepends.thy new file mode 100644 index 00000000..4f8eb516 --- /dev/null +++ b/etc/isa/depends/Usedepends.thy @@ -0,0 +1,5 @@ +(* dummy theory to load depends.ML *) +theory Usedepends = Main: +end + + diff --git a/etc/isa/goal-matching.ML b/etc/isa/goal-matching.ML new file mode 100644 index 00000000..843e2ca5 --- /dev/null +++ b/etc/isa/goal-matching.ML @@ -0,0 +1,10 @@ +(* + Test case sent by David von Oheimb. + Bug in matching case-insensitively meant that + the SELECT_GOAL line was considered a goal. +*) + +Goal "x"; +by (SELECT_GOAL all_tac 1); + + diff --git a/etc/isa/long-line-backslash.ML b/etc/isa/long-line-backslash.ML new file mode 100644 index 00000000..66435c1b --- /dev/null +++ b/etc/isa/long-line-backslash.ML @@ -0,0 +1,20 @@ +(* + + long-line-backslash.ML + + Test for long lines with backslashes in them. + Cause problem with pty communication where line length + is limited to 256 characters sometimes (e.g. on Solaris). + +*) + +val nasty_string="\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\"; + +(* Test subsequent commands can be processed *) + +val one = 1; +val two = 2; +val three = 3; + +(* Test something with eager annotations *) + diff --git a/etc/isa/message-test.ML b/etc/isa/message-test.ML new file mode 100644 index 00000000..4afd7120 --- /dev/null +++ b/etc/isa/message-test.ML @@ -0,0 +1,16 @@ +(* Testing different kinds of markup in Isabelle output *) + +(* ordinary output between prompts *) +print "ordinary"; +print "ordinary\n"; (* final newline no difference *) + +(* eager annotation: displayed as soon as it's seen *) +writeln "eager to be seen!"; + +print "more ordinary\n"; + +Goal "P-->P"; + +(* C-c RET to here should show eager annotation, as well as + updating goals buffer properly. *) +error "something went wrong"; diff --git a/etc/isa/multiple/A.ML b/etc/isa/multiple/A.ML new file mode 100644 index 00000000..771a5f1a --- /dev/null +++ b/etc/isa/multiple/A.ML @@ -0,0 +1,11 @@ +(* Scripting buffer for theory A *) + +1; + +(* A few commands so that we can test partial-retraction. *) + +2; + +3; + + diff --git a/etc/isa/multiple/A.thy b/etc/isa/multiple/A.thy new file mode 100644 index 00000000..fc585327 --- /dev/null +++ b/etc/isa/multiple/A.thy @@ -0,0 +1,7 @@ +(* + File: /home/da/proofgen/ProofGeneral/etc/isa/multiple/A.thy + Theory Name: A + Logic Image: Pure +*) + +A = Pure diff --git a/etc/isa/multiple/B.ML b/etc/isa/multiple/B.ML new file mode 100644 index 00000000..e0226516 --- /dev/null +++ b/etc/isa/multiple/B.ML @@ -0,0 +1,4 @@ +(* Scripting buffer for theory B *) + +val b = 0; +val b1 = 1; diff --git a/etc/isa/multiple/B.thy b/etc/isa/multiple/B.thy new file mode 100644 index 00000000..a896bca2 --- /dev/null +++ b/etc/isa/multiple/B.thy @@ -0,0 +1,7 @@ +(* + File: /home/da/proofgen/ProofGeneral/etc/isa/multiple/B.thy + Theory Name: B + Logic Image: Pure +*) + +B = Pure diff --git a/etc/isa/multiple/C.ML b/etc/isa/multiple/C.ML new file mode 100644 index 00000000..4ad965a2 --- /dev/null +++ b/etc/isa/multiple/C.ML @@ -0,0 +1,4 @@ +(* Scripting buffer for theory C *) + +val c1 = 4; +val c = 5; diff --git a/etc/isa/multiple/C.thy b/etc/isa/multiple/C.thy new file mode 100644 index 00000000..3316eaee --- /dev/null +++ b/etc/isa/multiple/C.thy @@ -0,0 +1,10 @@ +(* + File: /home/da/proofgen/ProofGeneral/etc/isa/multiple/C.thy + Theory Name: C + Logic Image: Pure +*) + +theory C = A + B +files "foobar/foo.ML": + +end diff --git a/etc/isa/multiple/D.ML b/etc/isa/multiple/D.ML new file mode 100644 index 00000000..76dd89c1 --- /dev/null +++ b/etc/isa/multiple/D.ML @@ -0,0 +1,3 @@ +(* Scripting buffer for theory D *) + +val it = (); diff --git a/etc/isa/multiple/D.thy b/etc/isa/multiple/D.thy new file mode 100644 index 00000000..afacc20e --- /dev/null +++ b/etc/isa/multiple/D.thy @@ -0,0 +1,7 @@ +(* + File: /home/da/proofgen/ProofGeneral/etc/isa/multiple/D.thy + Theory Name: D + Logic Image: Pure +*) + +D = Pure diff --git a/etc/isa/multiple/Err.ML b/etc/isa/multiple/Err.ML new file mode 100644 index 00000000..177da5ce --- /dev/null +++ b/etc/isa/multiple/Err.ML @@ -0,0 +1,5 @@ +(* Test to see that scripting is *not* turned on + if an error occurs during activation +*) + +val x = 1; diff --git a/etc/isa/multiple/Err.thy b/etc/isa/multiple/Err.thy new file mode 100644 index 00000000..d36a5af2 --- /dev/null +++ b/etc/isa/multiple/Err.thy @@ -0,0 +1,3 @@ +(* Dummy file to cause an error in use_thy *) + +Err = blah
\ No newline at end of file diff --git a/etc/isa/multiple/README b/etc/isa/multiple/README new file mode 100644 index 00000000..8ffa6fba --- /dev/null +++ b/etc/isa/multiple/README @@ -0,0 +1,102 @@ +Test files for multiple file handling with Isabelle. + + +Test schedule +============= + +[C depends on A and B, D is independent] + +Notation: A means that buffer A.l is unlocked + A+ means that buffer A.l is partly locked + A* means that buffer A.l is locked + ? means that behaviour might be different for proof systems + with non-linear contexts + +Borrowed from Thomas's lego tests: (v 1.2) + + 1) visit A.ML EFFECTS A + 2) visit C.ML EFFECTS A C + 3) assert C EFFECTS A* C* + 4) visit B.ML,B.thy,C.thy EFFECTS A* B* C* C.thy* B.thy* + 5) visit D.ML,D.thy EFFECTS A* B* C* D D.thy + 6) retract to middle of B EFFECTS A* B C D B.thy* (*thy remains locked*) + 7) assert first command of B EFFECTS A* B+ C D + 8) assert C EFFECTS A* B+ C D [error message, correctly] + 9) assert B EFFECTS A* B* C D +10) assert D EFFECTS A* B* C D* D.thy* +11) retract B EFFECTS A* B C D? [D* D.thy* for Isabelle] +12) assert C EFFECTS A* B* C* D? +13) retract B EFFECTS A* B C D? [B.thy* D*,D.thy* again] +14) assert B EFFECTS A* B* C D? +15) assert C EFFECTS A* B* C* D? [everything locked] + BROKEN 11.12.98: B.ML *may* not be locked? + +16) retract to middle of B EFFECTS A* B+ C D? + BROKEN! Now retracts whole thing. +14) M-x proof-shell-restart EFFECTS A B C D + + +MORE TESTS NEEDED FOR ISABELLE: +=============================== + +Should test assertion of theory files, and watch what happens to ML files. + +Because of theory loader's odd behaviour, must watch what happens +to ML files of autoloaded children. + + +1) visit example.ML, example.thy EFFECT: ML thy +2) assert .ML EFFECT: ML* thy* +3) retract thy EFFECT: ML thy + + +1) visit example.ML, example.thy ML thy +2) assert thy ML* thy* (reads theory too) + + +(* Test case for outdating a child theory *) + +1) assert C.thy A*, B*, C* +2) retract B.thy A* +3) edit B.thy to touch timestamp +4) assert B.thy A*, B*, C Message: "C out of date" +5) assert C.thy A*, B*, C* + + +(* Test case for removing a dependency from a theory: + this automatically unlocks the orphaned theory, + is this right?? +*) + +1) assert C.thy A*, B*, C* +2) retract C.thy A*, B*, C +3) edit C.thy to C=A, remove dependency on B +4) assert C.thy A*, B, C* (B automatically unlocked) + + + + + +----------------------------------------------------------------- + +Question: + +We assert script A. +We assert script B. +Can we retract to middle of A? Yes, we should be able to! + + + +----------------------------------------------------------------- + +Tester: + +Visit A.ML. Assert partly. + +Visit C.thy. Assert it. + +This should lock remainder of A.ML, since it has now been read +completely. + + + diff --git a/etc/isa/multiple/foobar/foo.ML b/etc/isa/multiple/foobar/foo.ML new file mode 100644 index 00000000..25084a22 --- /dev/null +++ b/etc/isa/multiple/foobar/foo.ML @@ -0,0 +1,4 @@ + +val foo = "foo"; + +val bar = 1; diff --git a/etc/isa/settings.ML b/etc/isa/settings.ML new file mode 100644 index 00000000..3250f9ca --- /dev/null +++ b/etc/isa/settings.ML @@ -0,0 +1,21 @@ +(* + Simple test for variable setting mechanism ML -> PG. + This kind of protocol is included in PGIP for setting config variables. + Here we can use it for executing arbitrary elisp, in fact (eek!) +*) + +fun pg_setvar var exp = writeln ("Proof General, please set the variable " ^ var ^ " to: #" ^ exp ^ "#."); + +pg_setvar "wag" "(+ 33 44)"; (* C-h v wag RET gives 77 *) + +fun pgset var = pg_setvar var "t"; +fun pgreset var = pg_setvar var "nil"; + +pgset "isa-show-types"; (* sets show-types in menu *) + +(* What might be nice is to override 'set' 'reset' fuctions to mirror + settings in PG automatically, but then we'd need to retrieve the + names of the ML values from the 'set' and 'reset' functions... *) + +(* test failure case: prints a debug message if proof-show-debug-messages<>nil *) +pg_setvar "wig" "blah 12 x12" diff --git a/etc/isa/thy/test.ML b/etc/isa/thy/test.ML new file mode 100644 index 00000000..6a434570 --- /dev/null +++ b/etc/isa/thy/test.ML @@ -0,0 +1,5 @@ +(* Test case for wrong file type + bug report by jv@ddre.dk + + This file should be ML, not theory! +*)
\ No newline at end of file diff --git a/etc/isa/xsym.ML b/etc/isa/xsym.ML new file mode 100644 index 00000000..797bad69 --- /dev/null +++ b/etc/isa/xsym.ML @@ -0,0 +1,18 @@ +(* a few token characters to exercise X-Symbol *) + +Goal "A \\<and> B \\<longrightarrow> B \\<and> A"; +by (rtac impI 1); +by (etac conjE 1); +by (rtac conjI 1); +by (assume_tac 1); +by (assume_tac 1); +qed "and_comms"; + +3; + +4; + +print "hello"; + +writeln "hello"; +error "hello"; diff --git a/etc/isar/CommentParsingBug.thy b/etc/isar/CommentParsingBug.thy new file mode 100644 index 00000000..e279fb68 --- /dev/null +++ b/etc/isar/CommentParsingBug.thy @@ -0,0 +1,3 @@ +(**)(**) +theory Scratch = Main: + diff --git a/etc/isar/Parsing.thy b/etc/isar/Parsing.thy new file mode 100644 index 00000000..4bd7e0a3 --- /dev/null +++ b/etc/isar/Parsing.thy @@ -0,0 +1,37 @@ +(* Not really a theory of parsing, but a test of Proof General's + parsing for Isabelle/Isar.... *) + +(* First, start with successive comments before a real command *) + +theory Parsing = Main: + +(* Then a comment *after* a command. Also one which mentions + the names of commands, such as theory or theorem or proof itself, + never mind thus assume end qed. *) + +text {* Isar theories can have arbitrary literal text, + so the text must be ignored as well; thus. *} + +(* Let's do my favourite proof. *) + +theorem and_comms: "A & B --> B & A" +proof + assume "A & B" (* it's "important" that we test "strings" I guess *) + thus "B & A" + proof + assume A B (* blah boo bah *) + show ?thesis (* bah boo bah *) + .. + qed +qed + +(* Now the end of file is coming up. Funny things happen + because PG only knows how commands start, not how they end. +*) + +end +(* That's the final command and it includes any text which follows it. + An oddity is that if there is a syntax error - unclosed comment + or whatever, after the last end, PG will say that it can't find + a complete command! *) + diff --git a/etc/isar/README b/etc/isar/README new file mode 100644 index 00000000..b2f5ffb2 --- /dev/null +++ b/etc/isar/README @@ -0,0 +1,8 @@ +bad1.thy: + Bug test case: parser would silently skip bad command "foo". + Resolved as of 13.9.00 + +bad2.thy: + Bug test case: synchronization problem on starting Isar process, + doesn't catch the first error. + Resolved as of 17.9.00 diff --git a/etc/isar/XEmacsSyntacticContextProb.thy b/etc/isar/XEmacsSyntacticContextProb.thy new file mode 100644 index 00000000..d910a6ba --- /dev/null +++ b/etc/isar/XEmacsSyntacticContextProb.thy @@ -0,0 +1,20 @@ +(* Demonstrates a bug with XEmacs 21.1: after procesing, between + two terms, buffer-syntactic-context returns "string". + But _before_ processing, it correctly returns "nil". + Even when regions are removed, still get "string" returned + after processing started. + + Bug doesn't occur in GNU Emacs (using imp of buffer-syntactic context + provided in proof-compat.el), nor in XEmacs 21.4 + + Workaround added Fri Aug 10 13:55:28 BST 2001 +*) + +theory XEmacsSyntacticContextProb = Main: + +term " +(f x)" + +term "(f x)" + +end diff --git a/etc/isar/bad1.thy b/etc/isar/bad1.thy new file mode 100644 index 00000000..a355389f --- /dev/null +++ b/etc/isar/bad1.thy @@ -0,0 +1,3 @@ +(*foo*) +foo +end diff --git a/etc/isar/bad2.thy b/etc/isar/bad2.thy new file mode 100644 index 00000000..11fecd77 --- /dev/null +++ b/etc/isar/bad2.thy @@ -0,0 +1 @@ +theory A = unknown: diff --git a/etc/isar/multiple/A.thy b/etc/isar/multiple/A.thy new file mode 100644 index 00000000..7ad1ddf6 --- /dev/null +++ b/etc/isar/multiple/A.thy @@ -0,0 +1,7 @@ + +theory A = Pure:; + +consts foo :: 'a; +consts bar :: 'a; + +end; diff --git a/etc/isar/multiple/B.thy b/etc/isar/multiple/B.thy new file mode 100644 index 00000000..2828c655 --- /dev/null +++ b/etc/isar/multiple/B.thy @@ -0,0 +1,4 @@ + +theory B = Pure:; + +end; diff --git a/etc/isar/multiple/C.thy b/etc/isar/multiple/C.thy new file mode 100644 index 00000000..d295f55a --- /dev/null +++ b/etc/isar/multiple/C.thy @@ -0,0 +1,5 @@ +(* -*- isar -*- *) + +theory C = A + B:; + +end; diff --git a/etc/isar/multiple/D.thy b/etc/isar/multiple/D.thy new file mode 100644 index 00000000..ed405e30 --- /dev/null +++ b/etc/isar/multiple/D.thy @@ -0,0 +1,4 @@ + +theory D = Pure:; + +end; diff --git a/etc/isar/multiple/README b/etc/isar/multiple/README new file mode 100644 index 00000000..ad57b449 --- /dev/null +++ b/etc/isar/multiple/README @@ -0,0 +1,3 @@ + +Test files for multiple file handling with Isabelle/Isar +(see also isa/multiple/README). diff --git a/etc/isar/trace_simp.thy b/etc/isar/trace_simp.thy new file mode 100644 index 00000000..430d37f5 --- /dev/null +++ b/etc/isar/trace_simp.thy @@ -0,0 +1,18 @@ + +theory trace_simp = Main: + +text {* + this produces massive amount of simplifier trace, but terminates + eventually: *} + +ML {* set trace_simp *} +ML {* reset quick_and_dirty *} + +datatype ord = Zero | Succ ord | Limit "nat => ord" + + +text {* this one loops forever *} + +lemma "ALL x. f x = g(f(g(x))) ==> f [] = f [] @ []" + apply simp + diff --git a/etc/junk.el b/etc/junk.el new file mode 100644 index 00000000..1ca27608 --- /dev/null +++ b/etc/junk.el @@ -0,0 +1,157 @@ +;;; junk.el +;;; +;;; $Id$ +;;; +;;; Bits and pieces of code +;;; removed from main PG (or never added). +;;; Left here in case they're useful later. +;;; +;;; Also some testing code. +;;; + +;;; TESTING FRAGMENTS + +;;; special display regexps +(setq special-display-regexps + (cons "\\*isabelle-\\(goals\\|response\\)\\*" + special-display-regexps)) + + +;;; dump str to buffer ug for testing. +(defun ugit (str) + (save-excursion + (set-buffer (get-buffer-create "ug")) + (goto-char (point-max)) + (insert str) + (newline) + (newline))) + + + + +;;; OLD CODE + +(defun proof-set-toggle (sym value) + "Try to set a boolean variable <blah>-enable using function <blah>-toggle." + (save-match-data + (let* ((nm (symbol-name sym)) + (i (string-match "-enable" nm)) + (tgfn (if i (intern (concat (substring nm 0 i) "-toggle"))))) + (if (and tgfn (fboundp tgfn)) + (funcall tgfn (if value 1 0)))))) + + +;; Was in proof-shell.el +(defun proof-shell-popup-eager-annotation () + "Process urgent messages. +Eager annotations are annotations which the proof system produces +while it's doing something (e.g. loading libraries) to say how much +progress it's made. Obviously we need to display these as soon as they +arrive." +;; FIXME: highlight eager annotation-end : fix proof-shell-handle-output +;; to highlight whole string. + (let ((str (proof-shell-handle-output + proof-shell-eager-annotation-start + proof-shell-eager-annotation-end + 'proof-eager-annotation-face)) + (proof-shell-message str)))) + + +; (cond +; ((string-match "FSF" emacs-version) +; ;; setting font-lock-defaults explicitly is required by FSF Emacs +; ;; 20.2's version of font-lock +; (make-local-variable 'font-lock-defaults) +; (setq font-lock-defaults '(font-lock-keywords))) +; ;; In XEmacs, we must make a new variable to hold +; ;; the defaults. +; ;; (FIXME: this makes toggling font-lock robust now, before +; ;; it was ropy. Should check whether this is the right +; ;; was for FSF too). +; (t +; (let +; ((flks (intern (concat (symbol-name major-mode) +; "-font-lock-defaults")))) +; ;; Take a copy of current font-lock-keywords to make them +; ;; the default in future. Then font-lock-mode can be +; ;; safely switched on and off. +; (set flks font-lock-keywords) +; (make-local-variable 'proof-font-lock-defaults) +; (setq proof-font-lock-defaults font-lock-keywords) +; (setq font-lock-defaults '(proof-font-lock-defaults))))) + ; (put major-mode 'font-lock-defaults (list flks))))) + + + +;; was is proof-shell, never used. +(defun proof-shell-strip-eager-annotation-specials (string) + "Strip special eager annotations from STRING, returning cleaned up string. +The input STRING should be annotated with expressions matching +proof-shell-eager-annotation-start and eager-annotation-end. +We only strip specials from the annotations." + (let* ((mstart (progn + (string-match proof-shell-eager-annotation-start string) + (match-end 0))) + (mend (string-match proof-shell-eager-annotation-end string)) + (msg (substring string mstart mend)) + (strtan (substring string 0 mstart)) + (endan (substring string mend))) + (concat + (proof-shell-strip-special-annotations strtan) + msg + (proof-shell-strip-special-annotations endan)))) + + + +;; 2. proof-find-and-forget-fn +;; +;; This calculates undo operations outwith a proof. If we retract +;; before a "Goal" command, proof-kill-goal-command is sent, followed +;; by whatever is calculated by this function. +;; +;; Isabelle has no concept of a linear context, and you can happily +;; redeclare values in ML. So forgetting back to the declaration of a +;; particular something makes no real sense. +;; The function is given a trivial implementation in this case. +;; +;; Find LEGO or Coq's implementation of this function to see how to +;; write it for proof assistants that can do this. + + + +;; FIXME: this is supposed to be a handy way of swapping +;; between goals and response buffer. Never mind. +;(defun proof-bury-buffer-after (buf) +; (if (and (string-match "XEmacs" emacs-version) ; XEmacs speciality +; (buffer-live-p buf)) +; (bury-buffer (current-buffer) buf) +; (bury-buffer))) + +;(defun proof-bury-buffer-after-goals () +; (interactive) +; (proof-bury-buffer-after proof-goals-buffer)) + + + +;(defun proof-bury-buffer-after-response () +; (interactive) +; (if proof-response-buffer +; (with-current-buffer proof-response-buffer +; (proof-bury-buffer-after proof-goals-buffer)))) + + + +;; This was added in proof-config.el. +;; +;; Better strategy to be less zippy about adding hooks is this: +;; +;; 1. Only add a hook if it is needed in *generic* code +;; 2. Only add a hook if it seems likely to be needed for different +;; provers, with different effects. +;; +;; This hook doesn't meet criteria! + +(defcustom proof-xsym-toggle-hook '(proof-x-symbol-toggle-clean-buffers) + "Hooks run when X-Symbol support is turned on or off." + :type 'string + :group 'proof-x-symbol) diff --git a/etc/lego/GoalGoal.l b/etc/lego/GoalGoal.l new file mode 100644 index 00000000..c4826e0d --- /dev/null +++ b/etc/lego/GoalGoal.l @@ -0,0 +1,13 @@ +Module GoalGoal; + +Goal first : {A:Prop}A->A; +intros; Immed; +(* no Save *) + +Goal second : {A:Prop}A->A; +intros; Immed; +Save second; +(* asserting until here caused Proof General to swap first and second. +This is a bug for LEGO. Thanks to Martin Hofmann for pointing this +out. An obvious bug fix would be to make the function +proof-lift-global Coq specific. *)
\ No newline at end of file diff --git a/etc/lego/error-eg.l b/etc/lego/error-eg.l new file mode 100644 index 00000000..f6872c90 --- /dev/null +++ b/etc/lego/error-eg.l @@ -0,0 +1,16 @@ +Init LF; + +[prop:Type]; +[prf:prop->Type]; +[type:Type]; +[el:type->Type]; + +[FA : {A:type}((el A) -> prop) -> prop]; +[LL : {A:type}{P:(el A) -> prop} + ({x:el A}prf(P(x)))-> + (********************************) + prf(FA A P)]; + +[P_FA : {A:type}{P:(el A) -> prop}{C_FA:prf(FA A P) -> prop} + ((g:{x:el A}prf(P(x)))prf(C_FA(LL A P g))) -> + {z:prf(FA A P)}prf(C_FA(z))];
\ No newline at end of file diff --git a/etc/lego/lego-site.el b/etc/lego/lego-site.el new file mode 100644 index 00000000..55098331 --- /dev/null +++ b/etc/lego/lego-site.el @@ -0,0 +1,23 @@ +;;; lego-site.el Site-specific Emacs support for LEGO +;;; Copyright (C) 1998 LFCS Edinburgh +;;; Author: Thomas Kleymann <T.Kleymann@ed.ac.uk> +;;; Maintainer: lego@dcs.ed.ac.uk + +(let ((version (getenv "PROOFGENERAL"))) + (cond ((not version) ;default + (setq load-path + (cons "/usr/local/share/elisp/script-management" load-path)) + (setq load-path + (cons "/usr/local/share/elisp/script-management/lego" load-path)) + (setq auto-mode-alist (cons '("\\.l$" . lego-mode) auto-mode-alist)) + (autoload 'lego-mode "lego" "Major mode for editing Lego proof scripts." t)) + ((string= version "ancient") + (setq load-path (cons "/usr/local/share/elisp/lego" load-path)) + (setq auto-mode-alist (cons '("\\.l$" . lego-mode) auto-mode-alist)) + (autoload 'lego-mode "lego" "Major mode for editing Lego proof scripts." t) + (autoload 'lego-shell "lego" "Inferior shell invoking lego." t)) + ((string= version "latest") + (load-file "/usr/local/share/elisp/ProofGeneral/generic/proof-site.el")))) + + +
\ No newline at end of file diff --git a/etc/lego/long-line-backslash.l b/etc/lego/long-line-backslash.l new file mode 100644 index 00000000..c85dcdc6 --- /dev/null +++ b/etc/lego/long-line-backslash.l @@ -0,0 +1,22 @@ +(* + + long-line-backslash.l + + Test for long lines with backslashes in them. + Cause problem with pty communication where line length + is limited to 256 characters sometimes (e.g. on Solaris). + +*) + +echo "\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\"; + +(* Test subsequent commands can be processed *) + +[one = Prop]; +[two = Prop -> Prop]; +[three = Prop -> two]; + +(* Test something with eager annotations *) + +Make "/usr/local/share/lego/lib-alpha/lib_Type/lib_logic"; + diff --git a/etc/lego/multiple/A.l b/etc/lego/multiple/A.l new file mode 100644 index 00000000..d45f8db8 --- /dev/null +++ b/etc/lego/multiple/A.l @@ -0,0 +1 @@ +Module A;
\ No newline at end of file diff --git a/etc/lego/multiple/B.l b/etc/lego/multiple/B.l new file mode 100644 index 00000000..3a8df7b2 --- /dev/null +++ b/etc/lego/multiple/B.l @@ -0,0 +1,4 @@ +(* B.l Module with a comment *) +Module B; + +[prop = Prop];
\ No newline at end of file diff --git a/etc/lego/multiple/C.l b/etc/lego/multiple/C.l new file mode 100644 index 00000000..5a3afdd6 --- /dev/null +++ b/etc/lego/multiple/C.l @@ -0,0 +1 @@ +Module C Import A B;
\ No newline at end of file diff --git a/etc/lego/multiple/D.l b/etc/lego/multiple/D.l new file mode 100644 index 00000000..b794253b --- /dev/null +++ b/etc/lego/multiple/D.l @@ -0,0 +1 @@ +Module D;
\ No newline at end of file diff --git a/etc/lego/multiple/README b/etc/lego/multiple/README new file mode 100644 index 00000000..11f2152a --- /dev/null +++ b/etc/lego/multiple/README @@ -0,0 +1,33 @@ +Handling of Multiple Files +========================== + +[C depends on A and B] + +Notation: A means that buffer A.l is unlocked + A+ means that buffer A.l is partly locked + A* means that buffer A.l is locked + ? means that behaviour might be different for proof systems + with non-linear contexts + + +Test Protocol +------------- + + 1) visit A.l EFFECTS A + 2) visit C.l EFFECTS A C + 3) assert C EFFECTS A* C* + 4) visit B.l EFFECTS A* B* C* + 5) visit D.l EFFECTS A* B* C* D + 6) retract to middle of B EFFECTS A* B C D + 7) assert first command of B EFFECTS A* B+ C D + 8) assert C EFFECTS A* B+ C D [error message] + 9) assert B EFFECTS A* B* C D +10) assert D EFFECTS A* B* C D* +11) retract B EFFECTS A* B C D? +12) assert C EFFECTS A* B* C* D? +13) retract B EFFECTS A* B C D? +14) assert B EFFECTS A* B* C D? +15) assert C EFFECTS A* B* C* D? +16) retract to middle of B EFFECTS A* B+ C D? +14) M-x proof-shell-restart EFFECTS A B C D + diff --git a/etc/lego/unsaved-goals.l b/etc/lego/unsaved-goals.l new file mode 100644 index 00000000..dd9c9646 --- /dev/null +++ b/etc/lego/unsaved-goals.l @@ -0,0 +1,54 @@ +(* + Some test cases for closing off unsaved goals, + and the setting proof-completed-proof-behaviour. + + David Aspinall, November 1999. + + Things work fairly well in lego with + + proof-completed-proof-behaviour='closeany + + In that case, undoing/redoing later declarations + (E and F) following the completed proof works okay, and + in the absence of declarations, things work fine. + + Declarations in LEGO are global, and forgetting a + declaration when a proof is still open (even if complete) + aborts the proof! So a proper handling would need to + trigger a *further* retraction when the "Forget D" is + issued undoing the definition of D. Never mind. + + With proof-completed-proof-behaviour='closegoal or 'extend, + undoing the first goal doesn't forget the declarations. + + This file even causes internal errors in LEGO! + + Warning: forgetting a finished proof + + LEGO detects unexpected exception named "InfixInternal" + + Test with undoing and redoing, and various settings + for proof-completed-proof-behaviour +*) + + + +Module unsaved Import lib_logic; + +Goal {A,B:Prop}(and A B) -> (and B A); +intros; +Refine H; +intros; +andI; +Immed; +[D = Type]; +[E = Type]; +[F = Type]; + +Goal {A,B:Prop}(and A B) -> (and B A); +intros; +Refine H; +intros; +andI; +Immed; + diff --git a/etc/patches/duplicated-short-messages-fix.txt b/etc/patches/duplicated-short-messages-fix.txt new file mode 100644 index 00000000..45b8727f --- /dev/null +++ b/etc/patches/duplicated-short-messages-fix.txt @@ -0,0 +1,107 @@ +This change should have gone into 3.0, but I forgot to make the +setting and so it missed testing. + +Minor bug without it is that Isabelle (others?) will sometimes +display messages less than 10 characters long twice, since +the urgent message scanner gets moved too far back. + +Sould probably also add this fix in proof-shell/proof-shell-insert: + + ;; FIXME: possible improvement. Make for post 3.0 releases + ;; in case of problems. + ;; (set-marker proof-shell-urgent-message-marker (point)) + ;; (set-marker proof-shell-urgent-message-scanner (point)) + + - da. + + + + +? etc/duplicated-short-messages-fix.txt +Index: coq/coq.el +=================================================================== +RCS file: /home/proofgen/src/ProofGeneral/coq/coq.el,v +retrieving revision 3.0 +diff -c -r3.0 coq.el +*** coq.el 1999/11/17 20:39:08 3.0 +--- coq.el 1999/11/29 13:22:14 +*************** +*** 502,507 **** +--- 502,508 ---- + proof-shell-field-char ?\374 ; not done + proof-shell-goal-char ?\375 ; done + proof-shell-eager-annotation-start "\376" ; done ++ proof-shell-eager-annotation-start-length 1 + proof-shell-eager-annotation-end "\377" ; done + proof-shell-annotated-prompt-regexp + (concat proof-shell-prompt-pattern +Index: isa/isa.el +=================================================================== +RCS file: /home/proofgen/src/ProofGeneral/isa/isa.el,v +retrieving revision 3.4 +diff -c -r3.4 isa.el +*** isa.el 1999/11/29 12:14:05 3.4 +--- isa.el 1999/11/29 13:22:15 +*************** +*** 172,177 **** +--- 172,178 ---- + proof-shell-quit-cmd "quit();" + + proof-shell-eager-annotation-start "\360\\|\362" ++ proof-shell-eager-annotation-start-length 1 + proof-shell-eager-annotation-end "\361\\|\363" + + ;; Some messages delimited by eager annotations +Index: isar/isar.el +=================================================================== +RCS file: /home/proofgen/src/ProofGeneral/isar/isar.el,v +retrieving revision 3.1 +diff -c -r3.1 isar.el +*** isar.el 1999/11/18 15:00:57 3.1 +--- isar.el 1999/11/29 13:22:15 +*************** +*** 250,255 **** +--- 250,256 ---- + proof-shell-restart-cmd "ProofGeneral.restart;" + proof-shell-quit-cmd (isar-verbatim "quit();") + ++ proof-shell-eager-annotation-start-length 1 + proof-shell-eager-annotation-start "\360\\|\362" + proof-shell-eager-annotation-end "\361\\|\363" + +Index: lego/lego.el +=================================================================== +RCS file: /home/proofgen/src/ProofGeneral/lego/lego.el,v +retrieving revision 3.1 +diff -c -r3.1 lego.el +*** lego.el 1999/11/24 21:48:24 3.1 +--- lego.el 1999/11/29 13:22:16 +*************** +*** 453,458 **** +--- 453,459 ---- + proof-shell-field-char ?\374 + proof-shell-goal-char ?\375 + proof-shell-eager-annotation-start "\376" ++ proof-shell-eager-annotation-start-length 1 + proof-shell-eager-annotation-end "\377" + proof-shell-annotated-prompt-regexp "Lego> \371" + proof-shell-result-start "\372 Pbp result \373" +Index: plastic/plastic.el +=================================================================== +RCS file: /home/proofgen/src/ProofGeneral/plastic/plastic.el,v +retrieving revision 3.1 +diff -c -r3.1 plastic.el +*** plastic.el 1999/11/22 18:52:47 3.1 +--- plastic.el 1999/11/29 13:22:16 +*************** +*** 538,543 **** +--- 538,546 ---- + proof-shell-field-char ?\374 + proof-shell-goal-char ?\375 + proof-shell-eager-annotation-start "\376" ++ ;; FIXME da: if p-s-e-a-s is implemented, you should set ++ ;; proof-shell-eager-annotation-start-length=1 to ++ ;; avoid possibility of duplicating short messages. + proof-shell-eager-annotation-end "\377" + + proof-shell-annotated-prompt-regexp "LF> \371" diff --git a/etc/patches/fix-attempt-for-eager-cleaning.txt b/etc/patches/fix-attempt-for-eager-cleaning.txt new file mode 100644 index 00000000..519df708 --- /dev/null +++ b/etc/patches/fix-attempt-for-eager-cleaning.txt @@ -0,0 +1,66 @@ +Patch below doesn't work because it examines the head of the +proof-action-list which is empty by the time +proof-handle-delayed-output gets called! + +Best thing may be to temporarily extend +proof-handle-delayed-output-hook with a function to clear the erase +flag... BUT can't remove it from proof-shell-done-invisible, +because that's too early!!! Argh. + +Maybe we need a special test in the exec loop for just one element in +the action list, and then call the callback *after* handling delayed +output? + +Um. Not for 3.0, then. + + + + +*** ProofGeneral.prev/generic/proof-shell.el Thu Nov 18 13:07:33 1999 +--- ProofGeneral/generic/proof-shell.el Thu Nov 18 13:03:25 1999 +*************** +*** 676,682 **** + ;; Erase the response buffer if need be, maybe also removing the + ;; window. Indicate that it should be erased before the next + ;; output. +! (proof-shell-maybe-erase-response t t) + + (set-buffer proof-goals-buffer) + +--- 676,684 ---- + ;; Erase the response buffer if need be, maybe also removing the + ;; window. Indicate that it should be erased before the next + ;; output. +! (proof-shell-maybe-erase-response +! (or proof-shell-erase-response-flag t) ; preserve invisible cmd o/p +! t) + + (set-buffer proof-goals-buffer) + +*************** +*** 829,835 **** + (unless proof-shell-leave-annotations-in-output + (setq str (proof-shell-strip-special-annotations str))) + +! (proof-shell-maybe-erase-response t nil) + (proof-response-buffer-display str) + (proof-display-and-keep-buffer proof-response-buffer)) + ;; +--- 831,847 ---- + (unless proof-shell-leave-annotations-in-output + (setq str (proof-shell-strip-special-annotations str))) + +! (proof-shell-maybe-erase-response +! ;; Magical detection of invisible commands, whose output +! ;; gets preserved specially. +! (if (and +! (not (eq proof-shell-erase-response-flag 'invisible)) +! (eq (nth 2 (car-safe proof-action-list)) +! 'proof-shell-done-invisible)) +! 'invisible +! t) ; erase next time, probably +! t) ; clean. +! + (proof-response-buffer-display str) + (proof-display-and-keep-buffer proof-response-buffer)) + ;; diff --git a/etc/pgkit/xmltest1.xml b/etc/pgkit/xmltest1.xml new file mode 100644 index 00000000..08ff0984 --- /dev/null +++ b/etc/pgkit/xmltest1.xml @@ -0,0 +1,3 @@ +<a>test a<b>test b<c>test</c></b>end test a</a> + + diff --git a/etc/pgkit/xmltest2.xml b/etc/pgkit/xmltest2.xml new file mode 100644 index 00000000..cfc8b1e8 --- /dev/null +++ b/etc/pgkit/xmltest2.xml @@ -0,0 +1,23 @@ +<root> + <q req_id="default_id"/> + <p fixed="bad fixed value" enum="bad enum"/> + <p> + <b/> + <c> + <unexpected/> + <undefined/> + </c> + <q req_id="unreferenced_id"/> + </p> + <n nmtoken="1bad nmtoken"/> + <n nmtoken="default_nmtoken"/> + <n/> + <nn nmtokens="1bad nmtokens"/> + <nn nmtokens="default_nmtoken"/> + <nn/> + <bad_id bad_idref="1bad ID"/> + <bad_id/> + <bad_ent bad_ent="1bad ENTITY"/> + <bad_ent/> + <empty>text in empty</empty> +</root> diff --git a/etc/profiling.txt b/etc/profiling.txt new file mode 100644 index 00000000..434b0bfd --- /dev/null +++ b/etc/profiling.txt @@ -0,0 +1,397 @@ +Notes on Profiling Proof General in XEmacs [da] +------------------------------------------------ + +M-x clear-profiling-info +Eval: (profile (proof-toolbar-next) (proof-shell-wait)) +M-x profile-results + +NB: Must ignore calls to accept-process-output and sit-for, these + are from proof-shell-wait (only). + + +Testing by processing first line of src/HOL/Real/ROOT.ML (i.e. loading +RealDef) + +Best case scenarios: + + * Running Isabelle in ordinary shell buffer in Emacs, PIII: + ~8% Emacs (PIII), ~90% SML if shell hidden + ~15% X, ~25% xemacs, ~60% SML if shell displayed! + + * Running Isabelle in xterm: + ~3% xterm, ~2% X, 95% SML if xterm hidden + ~4% xterm, ~16% X, 90% SML if xterm revealed + + +Before optimization: + + * CPU time split about 70%/30% (Cel 366) or 65%/35% (PIII 500) SML/xemacs + + + + + + + + +Sample Runs. Tue Oct 5 +----------------------- + +[On Cel 366 64M] + + +Function Name Ticks %/Total Call Count +=================================== ===== ======= ========== +(in redisplay) 1183 44.947 +re-search-forward 901 34.233 8061 +sit-for 159 6.041 11919 +comint-output-filter 93 3.533 3596 +accept-process-output 43 1.634 11919 +string-match 34 1.292 7300 +font-lock-pre-idle-hook 30 1.140 25261 +insert-before-markers 28 1.064 3597 +let 14 0.532 10853 +map-extents 13 0.494 539 +(in garbage collection) 10 0.380 +byte-code 9 0.342 25376 +while 8 0.304 3648 +setq 7 0.266 8299 +comint-postoutput-scroll-to-bottom 7 0.266 3597 +next-window 6 0.228 7194 +put-nonduplicable-text-property 5 0.190 1166 +marker-position 5 0.190 14389 +goto-char 5 0.190 14097 +walk-windows 4 0.152 3597 +window-minibuffer-p 4 0.152 3597 +proof-toolbar-refresh 4 0.152 3686 +and 4 0.152 11162 +selected-window 3 0.114 14390 +window-start 3 0.114 3596 +proof-shell-filter 3 0.114 3597 +itimer-time-difference 3 0.114 546 +#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 3 0.114 7194 +#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 3 0.114 1298 +process-buffer 3 0.114 3596 +point 3 0.114 7382 +or 3 0.114 7256 +comint-watch-for-password-prompt 3 0.114 3597 +save-excursion 2 0.076 3655 +proof-shell-process-urgent-messages 2 0.076 3597 +marker-buffer 2 0.076 3596 +font-lock-fontify-keywords-region 2 0.076 45 +process-mark 2 0.076 7208 +redisplay-echo-area 2 0.076 23 +if 2 0.076 18901 +buffer-name 1 0.038 3650 +erase-buffer 1 0.038 26 +pos-visible-in-window-p 1 0.038 1 +window-buffer 1 0.038 7195 +self-insert-command 1 0.038 14 +< 1 0.038 4300 +itimer-timer-driver 1 0.038 182 +font-lock-fontify-glumped-region 1 0.038 31 +get-buffer-process 1 0.038 3633 +char-to-string 1 0.038 3597 +save-current-buffer 1 0.038 17 +insert-string 1 0.038 23 +-------------------------------------------------------------------- +Total 2632 100.00 + + +One tick = 1 ms + + +[On PIII 256M] top shows roughly 65% SML / 35% xemacs. + +Function Name Ticks %/Total Call Count +====================================== ===== ======= ========== +(in redisplay) 3529 55.166 +re-search-forward 1520 23.761 31627 +sit-for 356 5.565 33870 +comint-output-filter 265 4.143 12980 +accept-process-output 125 1.954 33870 +font-lock-pre-idle-hook 67 1.047 73094 +insert-before-markers 51 0.797 12981 +(in garbage collection) 46 0.719 +string-match 44 0.688 27686 +byte-code 27 0.422 74822 +let 23 0.360 39724 +#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 21 0.328 25962 +selected-window 20 0.313 51951 +comint-postoutput-scroll-to-bottom 19 0.297 12981 +setq 15 0.234 39971 +if 15 0.234 72709 +walk-windows 13 0.203 12981 +proof-toolbar-refresh 13 0.203 14429 +marker-position 12 0.188 51925 +proof-shell-filter 12 0.188 12981 +goto-char 12 0.188 53685 +run-hook-with-args 12 0.188 13219 +next-window 11 0.172 25962 +and 9 0.141 40761 +save-excursion 8 0.125 13756 +buffer-name 7 0.109 13783 +window-buffer 7 0.109 26077 +log-message 7 0.109 237 +process-mark 7 0.109 26208 +point 7 0.109 27554 +while 7 0.109 13727 +#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 6 0.094 11268 +char-to-string 6 0.094 12981 +force-mode-line-update 6 0.094 12980 +< 5 0.078 19216 +itimer-run-expired-timers 4 0.063 415 +aref 4 0.063 11953 +get-buffer-process 4 0.063 13290 +proof-shell-process-urgent-messages 4 0.063 12981 +redisplay-echo-area 4 0.063 238 +insert-string 4 0.063 238 +font-lock-fontify-keywords-region 4 0.063 740 +window-minibuffer-p 3 0.047 12981 +window-start 3 0.047 12980 +marker-buffer 3 0.047 12980 +process-buffer 3 0.047 12980 +featurep 3 0.047 2120 +comint-watch-for-password-prompt 3 0.047 12981 +set-buffer 2 0.031 259 +or 2 0.031 26285 +font-lock-after-change-function-1 2 0.031 494 +font-lock-default-fontify-region 2 0.031 740 +event-over-toolbar-p 1 0.016 107 +get-buffer 1 0.016 433 +extent-object 1 0.016 988 +itimerp 1 0.016 9136 +itimer-is-idle 1 0.016 3735 +set-extent-property 1 0.016 1024 +make-string 1 0.016 247 +next-single-property-change 1 0.016 246 +expand-file-name 1 0.016 96 +incf 1 0.016 11268 +center-to-window-line 1 0.016 9 +proof-done-advancing 1 0.016 2 +itimer-time-difference 1 0.016 1660 +itimer-timer-driver 1 0.016 415 +1+ 1 0.016 11268 +length 1 0.016 249 +append-message 1 0.016 238 +concat 1 0.016 246 +proof-shell-strip-special-annotations 1 0.016 246 +proof-shell-process-urgent-message 1 0.016 246 +buffer-substring 1 0.016 493 +save-current-buffer 1 0.016 248 +newline 1 0.016 246 +insert 1 0.016 249 +current-time 1 0.016 831 +match-beginning 1 0.016 247 +font-lock-append-text-property 1 0.016 246 +progn 1 0.016 1034 +proof-response-buffer-display 1 0.016 246 +font-lock-fontify-syntactically-region 1 0.016 740 +font-lock-fontify-glumped-region 1 0.016 494 +#<compiled-function (buffer &rest body) "...(8)" [save-current-buffer set-buffer buffer body] 3 540150> 1 0.016 248 +font-lock-after-change-function 1 0.016 494 +----------------------------------------------------------------------- +Total 6397 100.00 + + +One tick = 1 ms + + +*** After some optimization attempt in proof-shell-process-urgent-messages, + to remove re-search-forward hog: + +[Cel 366] + +Function Name Ticks %/Total Call Count +=================================== ===== ======= ========== +accept-process-output 3279 62.374 1047436 +(in redisplay) 919 17.481 +sit-for 547 10.405 1047435 +re-search-forward 134 2.549 8950 +while 110 2.092 3648 +comint-output-filter 65 1.236 3347 +(in garbage collection) 24 0.457 +font-lock-pre-idle-hook 18 0.342 14166 +insert-before-markers 15 0.285 3348 +string-match 10 0.190 7376 +let 9 0.171 7010 +#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 9 0.171 6696 +setq 6 0.114 12598 +byte-code 5 0.095 14879 +#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 5 0.095 4762 +and 5 0.095 10936 +comint-postoutput-scroll-to-bottom 5 0.095 3348 +log-message 4 0.076 98 +save-excursion 3 0.057 3655 +itimerp 3 0.057 14128 +selected-window 3 0.057 13403 +next-window 3 0.057 6696 +point 3 0.057 10722 +proof-toolbar-refresh 3 0.057 3942 +if 3 0.057 23233 +font-lock-default-unfontify-region 3 0.057 295 +walk-windows 2 0.038 3348 +event-window 2 0.038 658 +buffer-name 2 0.038 3670 +erase-buffer 2 0.038 105 +put-nonduplicable-text-property 2 0.038 590 +window-start 2 0.038 3347 +null 2 0.038 3352 +marker-position 2 0.038 13393 +marker-buffer 2 0.038 3347 +itimer-time-difference 2 0.038 2223 +- 2 0.038 3350 +font-lock-fontify-keywords-region 2 0.038 295 +goto-char 2 0.038 14092 +buffer-substring 2 0.038 196 +redisplay-echo-area 2 0.038 104 +run-hook-with-args 2 0.038 3447 +comint-watch-for-password-prompt 2 0.038 3348 +event-over-vertical-divider-p 1 0.019 254 +event-glyph-extent 1 0.019 329 +get-buffer 1 0.019 255 +pointer-image-instance-p 1 0.019 985 +barf-if-buffer-read-only 1 0.019 98 +extent-at 1 0.019 87 +itimer-value 1 0.019 6175 +pos-visible-in-window-p 1 0.019 4 +expand-file-name 1 0.019 192 +file-truename 1 0.019 104 +center-to-window-line 1 0.019 4 +proof-shell-process-urgent-messages 1 0.019 3348 +proof-shell-filter 1 0.019 3348 +set-marker 1 0.019 3429 +itimer-run-expired-timers 1 0.019 247 +< 1 0.019 5950 +min 1 0.019 3428 +1- 1 0.019 3428 +display-message 1 0.019 99 +font-lock-fontify-glumped-region 1 0.019 197 +get-buffer-process 1 0.019 6791 +process-mark 1 0.019 10124 +default-mouse-motion-handler 1 0.019 329 +char-to-string 1 0.019 3348 +save-current-buffer 1 0.019 99 +newline 1 0.019 98 +or 1 0.019 3490 +#<compiled-function (buffer &rest body) "...(8)" [save-current-buffer set-buffer buffer body] 3 540150> 1 0.019 99 +font-lock-unfontify-region 1 0.019 295 +specifier-instance 1 0.019 329 +-------------------------------------------------------------------- +Total 5257 100.00 + + +One tick = 1 ms + + +[PIII] split now about 70%/30% + +Function Name Ticks %/Total Call Count +====================================== ===== ======= ========== +(in redisplay) 3638 72.082 +sit-for 358 7.093 34176 +comint-output-filter 247 4.894 12963 +accept-process-output 132 2.615 34176 +font-lock-pre-idle-hook 70 1.387 74389 +insert-before-markers 67 1.328 12964 +string-match 50 0.991 27655 +(in garbage collection) 43 0.852 +#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 29 0.575 25928 +re-search-forward 25 0.495 18630 +comint-postoutput-scroll-to-bottom 24 0.476 12964 +byte-code 22 0.436 76129 +selected-window 20 0.396 51883 +walk-windows 19 0.376 12964 +let 18 0.357 13746 +next-window 16 0.317 25928 +proof-toolbar-refresh 13 0.258 14445 +while 13 0.258 13710 +proof-shell-filter 11 0.218 12964 +process-mark 11 0.218 39137 +save-excursion 10 0.198 13741 +setq 10 0.198 27010 +and 9 0.178 27701 +goto-char 8 0.159 27695 +run-hook-with-args 8 0.159 13211 +if 7 0.139 33491 +font-lock-fontify-keywords-region 6 0.119 740 +#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 6 0.119 11268 +get-buffer-process 6 0.119 26242 +char-to-string 6 0.119 12964 +redisplay-echo-area 6 0.119 253 +specifier-instance 6 0.119 656 +itimerp 5 0.099 5713 +1- 5 0.099 13209 +point 5 0.099 27523 +buffer-name 4 0.079 13766 +current-buffer 4 0.079 13210 +window-start 4 0.079 12963 +< 4 0.079 6236 +itimer-timer-driver 4 0.079 380 +default-mouse-motion-handler 4 0.079 656 +featurep 4 0.079 2693 +force-mode-line-update 4 0.079 12963 +comint-watch-for-password-prompt 4 0.079 12964 +proof-shell-process-urgent-messages 3 0.059 12964 +font-lock-fontify-syntactically-region 3 0.059 740 +incf 3 0.059 11268 +marker-position 3 0.059 12968 +set-marker 3 0.059 13210 +itimer-time-difference 3 0.059 1140 +process-buffer 3 0.059 12963 +event-window 2 0.040 1312 +window-minibuffer-p 2 0.040 12964 +window-buffer 2 0.040 26524 +- 2 0.040 12967 +move-to-left-margin 2 0.040 246 +remove-message 2 0.040 253 +event-buffer 2 0.040 656 +font-lock-default-unfontify-region 2 0.040 740 +font-lock-after-change-function 2 0.040 494 +buffer-substring 2 0.040 493 +insert-string 2 0.040 253 +event-over-modeline-p 1 0.020 537 +event-glyph-extent 1 0.020 656 +set-syntax-table 1 0.020 740 +pointer-image-instance-p 1 0.020 1913 +extent-start-position 1 0.020 494 +make-extent 1 0.020 527 +detach-extent 1 0.020 495 +extent-at 1 0.020 363 +itimer-value 1 0.020 2660 +itimer-is-idle 1 0.020 2280 +set-extent-property 1 0.020 1024 +highlight-extent 1 0.020 656 +pos-visible-in-window-p 1 0.020 9 +glyph-property-instance 1 0.020 656 +get-text-property 1 0.020 492 +put-nonduplicable-text-property 1 0.020 1480 +next-single-property-change 1 0.020 246 +quote 1 0.020 13798 +marker-buffer 1 0.020 12963 +itimer-run-expired-timers 1 0.020 380 +aset 1 0.020 5280 +log-message 1 0.020 246 +min 1 0.020 13209 +current-left-margin 1 0.020 246 +display-message 1 0.020 246 +fw-frame 1 0.020 656 +font-lock-fontify-region 1 0.020 740 +font-lock-append-text-property 1 0.020 246 +substring 1 0.020 247 +proof-response-buffer-display 1 0.020 246 +delq 1 0.020 246 +syntactically-sectionize 1 0.020 740 +format 1 0.020 238 +proof-file-truename 1 0.020 88 +newline 1 0.020 246 +store-match-data 1 0.020 742 +proof-zap-commas-region 1 0.020 494 +specifierp 1 0.020 656 +log-message-filter 1 0.020 246 +----------------------------------------------------------------------- +Total 5047 100.00 + + +One tick = 1 ms + diff --git a/etc/proofgeneral-domain.txt b/etc/proofgeneral-domain.txt new file mode 100644 index 00000000..7b5b3c48 --- /dev/null +++ b/etc/proofgeneral-domain.txt @@ -0,0 +1,29 @@ +Notes about proofgeneral.org +---------------------------- + +Hosted by freeparking.co.uk. + +Sign up 20th Sep 2000, 2 years for £29.95 + +mail.proofgeneral.org is freeparking's mail handler +www.proofgeneral.org is zermelo.dcs.ed.ac.uk + + DNS zone: + + proofgeneral.org A 129.215.96.75 + +Email aliases: +-------------- + +support proofgen@dcs.ed.ac.uk +feedback proofgen@dcs.ed.ac.uk +bugs proofgen@dcs.ed.ac.uk +users proofgeneral@dcs.ed.ac.uk +devel proofgeneral-devel@dcs.ed.ac.uk +majordomo majordomo@dcs.ed.ac.uk +da da@dcs.ed.ac.uk + + + + + diff --git a/etc/release-log.txt b/etc/release-log.txt new file mode 100644 index 00000000..8c9c3986 --- /dev/null +++ b/etc/release-log.txt @@ -0,0 +1,68 @@ +9.9.01 3.3 Release 3-3 based on branch 6.0 + (repeated 10.9.01 to fix doc build) + +-------------------- + +02.10.00 3.2 Release 3-2 based on branch 5.0 + +-------------------- + +25.05.00 3.1.6 Release 3-1-6, from Release-3-1-branch + Button enablers are not used by default on XEmacs/Solaris. + When button enablers disabled, don't use itimer or after-change hook. + +9.05.00 3.1.5 Release 3-1-5, from Release-3-1-branch + Improved proof-find-theorems-command for Isabelle + (allow multiple constants separated by commas). + +28.04.00 3.1.4 Release 3-1-4, from Release-3-1-branch + Applied patch sent by Mike Squire, fix accident in previous fix. + (Isabelle theory retraction file paths) + +04.04.00 3.1.3 Release 3-1-3 + Fixed two problems with Isabelle theory loader interface + (first introduced accidently in 3.1, second a bug/issue in Isabelle) + Markus's continuing Isar syntax patches. + Updated some copyright notices. + +24.03.00 3.1.2 Release 3-1-2 + Small improvement to HOL support. + +24.03.00 3.1.1 Release 3-1-1 + Added more fixes for Isabelle and Windows. + Fixes for Windows, using proper colours, etc. + Markus's Isar syntax patches. + +23.03.00 3.1 Release 3-1 + First version of 3.1 release + +-------------------- + + +30.11.99 3.0.3 Release-3-0-3 + Full version now in version stamp. + +29.11.99 3.0.2 Release-3-0-2 + Added some more key-bindings and menu entries to + Isabelle's theory file mode. + +26.11.99 3.0 Release 3-0 + First attempt at 3.0 release + + 3.0.1 Release-3-0-1 + Fixed problem with proof-shell-proof-completed-regexp + in Isabelle. + + +-------------------- + + +25.8.99 2.1.3 Release-2-1-3 + Fixed RPM package to include isar/ + +24.8.99 2.1.2 Release-2-1-2 + Official release Proof General 2.1 + +23.8.99 2.1.1 Release-2-1-1 + First release of Proof General version 2.1. + Missing Isar and with broken version stamp (2.1pre990820) diff --git a/etc/screenshot-notes.txt b/etc/screenshot-notes.txt new file mode 100644 index 00000000..3a0daff6 --- /dev/null +++ b/etc/screenshot-notes.txt @@ -0,0 +1,36 @@ +Screenshot notes. +================= + +All in 80x40 sized XEmacs. + +* Isabelle: Dagstuhl HOLCF example. Show theory file on screen too. + +* Isar: Example Group.thy is modified version with extra X-Symbol line: + +syntax (xsymbols) + "op *" :: "['a::times, 'a] => 'a" (infixl "\\<bullet>" 70); + +And uses of * replaced with \\<bullet>. + +* Coq: Example from Sorting library. Multiple frame mode, X-Symbols, +also with Netscape. + +Most shots scaled to 0.2 or thereabouts to give nice sized thumbnail. + + + + + + +----------------------------------------------------------------- + +Regenerating screen shot in html/IsaPGscreen.jpg: + + 30x80 sized XEmacs. Visit isa/example.ML. + Click on "next" button four times. + Drag middle modeline to display whole proof script. + Move point to end of locked region. + Grab with gimp, Xtns -> Screen Shot. + Save with default quality settings. + +-----------------------------------------------------------------
\ No newline at end of file diff --git a/etc/test-schedule.txt b/etc/test-schedule.txt new file mode 100644 index 00000000..700cf5ca --- /dev/null +++ b/etc/test-schedule.txt @@ -0,0 +1,19 @@ +Some test schedules for Proof General +===================================== + +$Id$ + +(in progress) + +-------------------- + +Desirable tests: + +* Settings mechanism; PROOFGENERAL_ASSISTANTS vs .emacs and + customize-set-variable, interaction with Isabelle startup + scripts. + + + + + diff --git a/etc/testing-log.txt b/etc/testing-log.txt new file mode 100644 index 00000000..324284d4 --- /dev/null +++ b/etc/testing-log.txt @@ -0,0 +1,142 @@ +Fri Mar 24 15:40:10 GMT 2000 da + + Tested Proof General on win32 (NT4sp6) with Isabelle, Coq and + XEmacs 21.1.9. + + Problems: Isabelle bombs on paths containing chars like \ : $ + XEmacs barfs on reading some files in PG, why?? + e.g. coq/coq.el + + Can fix this by reloading coq stuff again. + + A few probs remain, e.g. toolbar enablers for undo are + flaky. + + +Wed Mar 22 13:45:34 GMT 2000 da + + Tested file name quoting problem with Coq, Isabelle, LEGO. + + \ quoting triggers bug in Isabelle (complaint about pathname) + " quoting not allowed in LEGO, \ quoting not needed. + Coq works well with either. + + + +-------- + +Wed Nov 17 13:43:11 GMT 1999 + + Tested compiled version. Seems to work well for XEmacs! + Also for FSF Emacs! So long as using their own elc's. + +Tue Nov 16 15:28:51 GMT 1999 + + Tested automatic multiple file handling: see etc/demoisa + + Tested FSF Emacs, after fixing several things. + + Tested proof by pointing in LEGO. Fixes for bugs, + empty pbp response, and added a useful click + (C-button 3) for undoing and deleting the last + pbp command. Can now prove example.l by PBP. + Proof-by-pointing lives! + +Thu Nov 11 19:05:39 GMT 1999 + + Tested response buffer display: see isa/message-test.ML + Made output more regular by removing spurious space/newline + after every prompt, and padding response buffer with + newlines when messages aren't newline terminated. + + Testing window management for multiple frames. Could find no + evidence of old bug message in code about with + special-display-regexps, script buffer gets made into + dedicated buffer. Removed the comment. + +Mon Aug 23 19:00:26 BST 1999 da + + Summary of tests today: + + Proof General 2.0: sanity check. + Okay with XEmacs 20.4, lego 1.3.1 and Isabelle 98p1. + Strange overlay disappearing problem with FSF Emacs 20.2, + so must be X Server or architecture anomaly that causes + different display order. + + Today's Proof General. + + 1. With Isabelle 98p1, no go. + 2. Same show-stopper as above with Emacs 20.2 and 20.3. + Argh! I'm really fed up of FSF Emacs, it goes wrong + even when "nothing" has changed. + 3. With current Isabelle (or, at least, 99pre180899). + 4. Using x-symbol. No success, and a big mess (rebinds M-x !!?) + +Thu Jan 21 14:27:36 GMT 1999 da + + Quick test for pipe communication with emacs 20.3. + Used C-c C-n and C-c C-u on example.ML file in + Isabelle successfully. + + (Tested 990115 prerelease with piped communication + patch in XEmacs already, for LEGO and Isabelle). + +Wed Dec 16 15:45:53 GMT 1998 da + + Quick test of Coq mode. + + xemacs -q -l ProofGeneral/generic/proof-site.el + + (setq proof-rsh-command "ssh hope") + + Assertion and retraction commands work as far as I can + tell. Using toolbar on file coq/example.v + + +Wed Dec 16 12:25:00 GMT 1998 tms + + Clarification of entry "Mon Dec 14 15:02:52 GMT 1998 da" + + The problem with LEGOVERSION "alpha" can also be reproduced with + lego 1.3.1 (and XEmacs 20.4 or FSF Emacs 20.2) and the file + lego/example2.l which accesses a module in a non-writable directory. + You need to set chmod u-w readonly yourself; CVS doesn't like + non-writable directories) + It is a LEGO specific problem. LEGO forgets about annotations + sometimes. This has been reported to lego@dcs.ed.ac.uk . + + +Wed Dec 16 12:25:00 GMT 1998 tms + + On scar, tested Emacs 20.2.1 with lego 1.3.1 via "ssh craro", + LEGOVERSION "std" + + emacs-20.2 -eval '(progn (load + "/home/tms/emacs/ProofGeneral/generic/proof-site.el")(setq + proof-rsh-command "ssh craro"))' lego/example.l + + Pressing C-c C-n crashes Emacs: Fatal error (11).Segmentation fault + + This must be a problem with my .emacs file. Including -q in the + options, everyting seems to work just fine. Still, this is somewhat + concerning. + + +Mon Dec 14 15:02:52 GMT 1998 da + + Tested Emacs 20.2.1 with lego 1.3 via "ssh hope", + with lego 1.3.1 via "ssh craro", LEGOVERSION "std" + + Both successfully process example.l + + With lego 1.3.1 via "ssh craro", LEGOVERSION "alpha", + processing gets stuck, never reports "imports done". + Is this a bug or problem with LEGO installation? + + Bugs: + Killing off process shell via proof-shell-exit. + Killing proof script buffer gives error. + + + |