diff options
Diffstat (limited to 'etc')
99 files changed, 3774 insertions, 0 deletions
diff --git a/etc/Mailman/handle_opts.html b/etc/Mailman/handle_opts.html new file mode 100644 index 00000000..98ce0a02 --- /dev/null +++ b/etc/Mailman/handle_opts.html @@ -0,0 +1,13 @@ +<!-- PG Template $Id$. Based on Informatics/MM Revision: 1.4 --> +<html> +<head> +<title><MM-List-Name> <MM-Operation> Results</title> +<link rel="SHORTCUT ICON" href="http://www.proofgeneral.org/favicon.ico"> +<link href="http://www.proofgeneral.org/proofgen.css" rel="stylesheet" type="text/css"> +</head> +<body> +<h1><MM-List-Name> <MM-Operation> Results</h1> +<MM-Results> +<MM-Mailman-Footer> +</body> +</html> diff --git a/etc/Mailman/intro-proofgeneral.html b/etc/Mailman/intro-proofgeneral.html new file mode 100644 index 00000000..d66cc397 --- /dev/null +++ b/etc/Mailman/intro-proofgeneral.html @@ -0,0 +1,3 @@ +<a href="http://www.proofgeneral.org">Proof General</a> is a generic interface for proof assistants, currently based on Emacs. This mailing list is for the announcement of new versions of Proof General and discussions about using Proof General. Posting is only available to list members. + +If you have a problem with using or configuring Proof General, please contact <a href="mailto:support@proofgeneral.org">support@proofgeneral.org</a> instead of posting to this list. People who are interested in the development of Proof General should join the <a href="http://lists.informatics.ed.ac.uk/mailman/listinfo/proofgeneral-devel">Proof General developers list</a>. diff --git a/etc/Mailman/intro-proofgeneraldevel.html b/etc/Mailman/intro-proofgeneraldevel.html new file mode 100644 index 00000000..ef926a63 --- /dev/null +++ b/etc/Mailman/intro-proofgeneraldevel.html @@ -0,0 +1,4 @@ +<a href="http://www.proofgeneral.org">Proof General</a> is a generic interface for proof assistants, currently based on Emacs. This mailing list is for developers of Proof General to discuss issues in the development of new versions of Proof General, such as new features and adaptation to new proof assistants. +Posting is only available to list members. + +For announcements about Proof General and discussion of using it, subscribe to the <a href="http://lists.informatics.ed.ac.uk/mailman/listinfo/proofgeneral">ProofGeneral users list</a>. Announcements sent there will <b>not</b> be duplicated here. diff --git a/etc/Mailman/listinfo.html b/etc/Mailman/listinfo.html new file mode 100644 index 00000000..f0295cd6 --- /dev/null +++ b/etc/Mailman/listinfo.html @@ -0,0 +1,142 @@ +<!-- Template for PG lists, based on Informatics/Mailman template Revision: 1.21 --> +<!-- $Id$ --> +<html> +<head> + <link rel="SHORTCUT ICON" href="http://www.proofgeneral.org/favicon.ico"> + <title><MM-List-Name> Mailing List Info Page</title> + <meta name="author" content="David Aspinall <da@dcs.ed.ac.uk>"> + <meta name="keywords" content="Isabelle, LEGO, Coq, Emacs, XEmacs, + Interface, Theorem Prover, GUI, David Aspinall"> + <meta name="description" content="Proof General is an Emacs based + generic interface for theorem provers"> + <link href="http://www.proofgeneral.org/proofgen.css" rel="stylesheet" type="text/css"> +</head> +<body + bgcolor="#2D1D03" + background="http://www.proofgeneral.org/images/canvaswallpaper.jpg" + text="#FFFFFF" + link="#FFD820" + vlink="#FFD820" + alink="#FFF030" + > +<table width="80%"> +<tr> +<td width="15%"> +<a href=""> +<img src="http://www.proofgeneral.org/images/PG-small.jpg" align=top width=37 height=50 border=0 alt="Proof General Home"> +</a> +</td> +<td width="85%"> +<h1><MM-List-Name> List Info Page</h1> +</td> +</table> + <MM-Subscribe-Form-Start> + <TABLE COLS="1" BORDER="0" CELLSPACING="4" CELLPADDING="5"> + <TR> + <TD class="head1" COLSPAN="2" WIDTH="100%"> + <MM-List-Name> -- <MM-List-Description> + </TD> + </TR> + <tr> + <TD class="head2" COLSPAN="2" WIDTH="100%"> + About the <MM-List-Name> list + </TD> + </TR> + <tr> + <td colspan="2"> + <P><MM-List-Info></P> + <p> To see the collection of prior postings to the list, + visit the <MM-Archive><MM-List-Name> + Archives</MM-Archive>. + <MM-Restricted-List-Message> + </p> + </TD> + </TR> + <tr> + <TD class="head2" COLSPAN="2" WIDTH="100%"> + Using the <MM-List-Name> list + </TD> + </TR> + <tr> + <td colspan="2"> + To post a message to all the list members, send email to + <A HREF="mailto:<MM-Posting-Addr>"><MM-Posting-Addr></A>. + + <p>You can subscribe to the list, or change your existing + subscription, in the sections below. + </td> + </tr> + <tr> + <TD class="head2" COLSPAN="2" WIDTH="100%"> + Subscribing to the <MM-List-Name> list + </TD> + </TR> + <tr> + <td colspan="2"> + <P> + Subscribe to the <MM-List-Name> list by filling out the following + form. + <MM-List-Subscription-Msg> + <ul> + <TABLE BORDER="0" CELLSPACING="2" CELLPADDING="2" + WIDTH="90%" HEIGHT= "112"> + <TR> + <TD class="head3" WIDTH="55%">Your email address:</TD> + <TD WIDTH="33%"><MM-Subscribe-Box> + </TD> + <TD WIDTH="12%"> </TD></TR> + <TR> + <TD COLSPAN="3"><FONT SIZE=-1>You must enter a + privacy password. This provides only mild security, + but should prevent others from messing with your + subscription. <b>Do not use a valuable password</b> as + it will occasionally be emailed back to you in cleartext. + <MM-Reminder> + </TD> + </TR> + <TR> + <TD class="head3">Pick a password:</TD> + <TD><MM-New-Password-Box></TD> + <TD> </TD></TR> + <TR> + <TD class="head3">Reenter password to confirm:</TD> + <TD><MM-Confirm-Password></TD> + <TD> </TD></TR> + <tr> + <td>Would you like to receive list mail batched in a daily + digest? + </td> + <td><MM-Undigest-Radio-Button> No + <MM-Digest-Radio-Button> Yes + </TD> + </tr> + <tr> + <td colspan="3"> + <center><MM-Subscribe-Button></P></center> + </TABLE> + <MM-Form-End> + </ul> + </td> + </tr> + <tr> + <a name="subscribers"> + <TD class="head2" COLSPAN="2" WIDTH="100%"> + <MM-List-Name> subscribers + </TD> + </TR> + <tr> + <TD COLSPAN="2" WIDTH="100%"> + <MM-Roster-Form-Start> + <MM-Roster-Option> + <MM-Form-End> + <p> + <MM-Subscribe-Form-Start> + <MM-Editing-Options> + <MM-Form-End> + </td> + </tr> + </table> +<MM-Mailman-Footer> +</BODY> +</HTML> + diff --git a/etc/Mailman/note.txt b/etc/Mailman/note.txt new file mode 100644 index 00000000..dc26ca6b --- /dev/null +++ b/etc/Mailman/note.txt @@ -0,0 +1,36 @@ +intro-proofgeneral<-devel>.html +is header set in general options +http://lists.informatics.ed.ac.uk/mailman/admin/proofgeneral/general +http://lists.informatics.ed.ac.uk/mailman/admin/proofgeneral-devel/general + +----------------------------------------------------------------- + +The remaining templates have to be installed in mailman by visiting +these pages: + +http://lists.informatics.ed.ac.uk/mailman/edithtml/proofgeneral/<template> + +http://lists.informatics.ed.ac.uk/mailman/edithtml/proofgeneral-devel/<template> + +The same templates are used to give PG styling to each list. + + +See Mailman docs at http://www.imsa.edu/~ckolar/mailman/ + +(For mail admin settings, see here: + http://www.imsa.edu/~ckolar/mailman/mailman-administration-v2.html) + +================================================================= + +FIXME: + +Header of options/result seems broken in Mailman/inf: + +following junk appears at start of page defined: + +<html> +<head> +</head> +<body +<BODY bgcolor="#ffffff"> + diff --git a/etc/Mailman/options.html b/etc/Mailman/options.html new file mode 100644 index 00000000..6f3ab613 --- /dev/null +++ b/etc/Mailman/options.html @@ -0,0 +1,186 @@ +<!-- Template for PG lists, based on Informatics/Mailman template Revision: 1.21 --> +<!-- $Id$ --> +<html> +<head> + <link rel="SHORTCUT ICON" href="http://www.proofgeneral.org/favicon.ico"> + <title><MM-List-Name> Mailing List Options Page</title> + <meta name="author" content="David Aspinall <da@dcs.ed.ac.uk>"> + <meta name="keywords" content="Isabelle, LEGO, Coq, Emacs, XEmacs, + Interface, Theorem Prover, GUI, David Aspinall"> + <meta name="description" content="Proof General is an Emacs based + generic interface for theorem provers"> + <link href="http://www.proofgeneral.org/proofgen.css" rel="stylesheet" type="text/css"> +</head> +<body + bgcolor="#2D1D03" + background="http://www.proofgeneral.org/images/canvaswallpaper.jpg" + text="#FFFFFF" + link="#FFD820" + vlink="#FFD820" + alink="#FFF030" + > +<table width="80%"> +<tr> +<td width="15%"> +<a href=""> +<img src="http://www.proofgeneral.org/images/PG-small.jpg" align=top width=37 height=50 border=0 alt="Proof General Home"> +</a> +</td> +<td width="85%"> +<h1><MM-List-Name> Mailing List Options Page</h1> +</td> +</table> + +<MM-Form-Start> + +<p> + +<b><MM-Presentable-User></b>'s subscription status, +password, and options for the <MM-List-Name> mailing list. +<MM-Case-Preserved-User> + +<MM-Disabled-Notice> + +<p> + +<!-- Added style sheet --> +<a name=unsub> + <TABLE WIDTH="100%" BORDER="0" CELLSPACING=5" CELLPADDING="5"> + <TR> + <TD class="head2" WIDTH="50%"> + Unsubscribing from <MM-List-Name> + </TD> + <TD class="head2" WIDTH="50%"> + Your other <MM-Host> subscriptions + </TD> + </TR> + +<tr> +<td> +To unsubscribe, enter your password and hit the button. (If you've +lost your password, see just below to have it emailed to you.) + +<p> +Password: <MM-Unsub-Pw-Box> +<MM-Unsubscribe-Button> +</p> +</a> +</td> + +<td> +Enter your password to visit a list of links to option pages for +all your subscriptions. + +<p> +Password: <MM-Other-Subscriptions-Pw-Box> +<MM-Other-Subscriptions-Submit><p> +</p> +</td></tr> +</table> + +<TABLE WIDTH="100%" BORDER="0" CELLSPACING="0" CELLPADDING="5"> +<!-- Added style sheet --> + <TR> + <TD class="head2" COLSPAN="2" WIDTH="100%"> + Your <MM-List-Name> Password + </TD> + </TR> +<tr valign="TOP"> +<td WIDTH="50%"> +<a name=reminder> +<center> +<h3>Forgotten Your Password?</h3> +</center> +Click this button to have your password emailed to your list delivery +address. <p> +<MM-Umbrella-Notice> +<center> +<MM-Email-My-Pw> +</center> +</td> +<td WIDTH="50%"> +<a name=changepw> +<center> +<h3>Change Your Password</h3> + <TABLE BORDER="0" CELLSPACING="2" CELLPADDING="2" WIDTH="90%" COLS=2> + <TR> + <TD class="head3" WIDTH="30%" >Old password:</TD> + <TD WIDTH="70%"><MM-Old-Pw-Box></TD> + </TR> + <TR> + <TD class="head3">New password:</TD> + <TD><MM-New-Pass-Box></TD> + </TR> + <TR> + <TD class="head3">Again to confirm:</TD> + <TD><MM-Confirm-Pass-Box></TD> + </TR> +</table> + <MM-Change-Pass-Button> + </TABLE> + +<p> + +<a name=options> + <TABLE WIDTH="100%" BORDER="0" CELLSPACING="0" CELLPADDING="5"> +<!-- Added style sheet --> + <TR> + <TD class="head2" COLSPAN="2" WIDTH="100%"> + Your <MM-List-Name> Subscription Options + </TD> + </TR> +</table> + +<p> +<i><strong>Current values are checked.</strong></i><p> +<p> +<TABLE BORDER="0" CELLSPACING="2" CELLPADDING="3" WIDTH="80%"> +<tr><TD class="head3"> +<a name="disable"> +<strong> Disable mail delivery </strong> <br> +Turn this on if you want mail to not be delivered to you for a little while.<br> +<mm-delivery-enable-button> Off +<mm-delivery-disable-button> On <p> +</a> +</td></tr> +<tr><TD class="head3"> +<strong> Set Digest Mode</strong> <br> +If you turn digest mode on, you'll get posts bundled together once a +day, instead singly when they're sent. If digest mode is changed from +on to off, you will receive one last digest.<br> +<MM-Undigest-Radio-Button> Off +<MM-Digest-Radio-Button> On<br> +</td></tr> +<tr><TD class="head3"> +<strong> Get MIME or Plain Text Digests?</strong> <br> +If you have any problems with MIME digests, select plain text. <br> +<MM-Mime-Digests-Button> MIME +<MM-Plain-Digests-Button> Plain Text <p> +</td></tr> +<tr><TD class="head3"> +<strong> Receive posts you send to the list? </strong><br> +<mm-receive-own-mail-button> Yes +<mm-dont-receive-own-mail-button> No <p> +</td></tr> +<tr><TD class="head3"> +<strong> Receive acknowledgement mail when you send mail to the list? </strong><br> +<mm-dont-ack-posts-button> No +<mm-ack-posts-button> Yes <p> +</td></tr> +<tr><TD class="head3"> +<strong> Conceal yourself from subscriber list? </strong><br> +<MM-Public-Subscription-Button> No +<MM-Hide-Subscription-Button> Yes <p> +</td></tr> +<tr><TD class="head3"> +Password: <MM-Digest-Pw-Box> <MM-Digest-Submit><p> +</td></tr></table> +</center> + +<p> +<MM-Form-End> + +<MM-Mailman-Footer> +</body> +</html> + diff --git a/etc/Mailman/subscribe.html b/etc/Mailman/subscribe.html new file mode 100644 index 00000000..ec10dd24 --- /dev/null +++ b/etc/Mailman/subscribe.html @@ -0,0 +1,13 @@ +<!-- PG Template $Id$. Based on Informatics/MM Revision: 1.4 --> +<html> +<head> +<title><MM-List-Name> Subscription results</title> +<link rel="SHORTCUT ICON" href="http://www.proofgeneral.org/favicon.ico"> +<link href="http://www.proofgeneral.org/proofgen.css" rel="stylesheet" type="text/css"> +</head> +<body> +<h1><MM-List-Name> Subscription results</h1> +<MM-Results> +<MM-Mailman-Footer> +</body> +</html> diff --git a/etc/ProofGeneral.desktop b/etc/ProofGeneral.desktop new file mode 100644 index 00000000..93594ac4 --- /dev/null +++ b/etc/ProofGeneral.desktop @@ -0,0 +1,8 @@ +# KDE Config File +[Desktop Entry] +Name=Proof General +Comment=Interface to Proof Assistants +Type=Application +Exec=proofgeneral +Icon=pgicon.png +Terminal=0 diff --git a/etc/ProofGeneral.menu b/etc/ProofGeneral.menu new file mode 100644 index 00000000..cda3fd48 --- /dev/null +++ b/etc/ProofGeneral.menu @@ -0,0 +1,7 @@ +?package(ProofGeneral):\ + needs=X11\ + section="Applications/Sciences/Computer science"\ + title="Proof General"\ + longtitle="Interface to Proof Assistants"\ + command="/usr/bin/proofgeneral"\ + icon="pgicon.png" diff --git a/etc/ProofGeneral.spec b/etc/ProofGeneral.spec new file mode 100644 index 00000000..e0954c08 --- /dev/null +++ b/etc/ProofGeneral.spec @@ -0,0 +1,122 @@ +Summary: Proof General, Emacs interface for Proof Assistants +Name: ProofGeneral +Version: 3.5pre030121 +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.5pre030121.tar.gz +BuildRoot: /tmp/ProofGeneral-root +PreReq: /sbin/install-info +Prefixes: /usr/share/emacs /usr/bin /usr/share/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 isar/isartags ${RPM_BUILD_ROOT}/usr/bin + +# Put info file in proper place, compress it. +mkdir -p ${RPM_BUILD_ROOT}/usr/share/info +mv doc/ProofGeneral.info doc/ProofGeneral.info-* ${RPM_BUILD_ROOT}/usr/share/info +mv doc/PG-adapting.info doc/PG-adapting.info-* ${RPM_BUILD_ROOT}/usr/share/info +gzip ${RPM_BUILD_ROOT}/usr/share/info/ProofGeneral.info ${RPM_BUILD_ROOT}/usr/share/info/ProofGeneral.info-* +gzip ${RPM_BUILD_ROOT}/usr/share/info/PG-adapting.info ${RPM_BUILD_ROOT}/usr/share/info/PG-adapting.info-* +# Remove duff bits +rm -f doc/dir doc/localdir + +# Put icons and menu entry into suitable place (at least for RedHat, 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/share/pixmaps +cp images/pgicon.png ${RPM_BUILD_ROOT}/usr/share/pixmaps +mkdir -p ${RPM_BUILD_ROOT}/usr/lib/menu +mkdir -p ${RPM_BUILD_ROOT}/usr/share/applnk/Applications +mkdir -p ${RPM_BUILD_ROOT}/etc/X11/applnk/Applications +mv etc/ProofGeneral.menu ${RPM_BUILD_ROOT}/usr/lib/menu/ProofGeneral # Mandrake +cp etc/ProofGeneral.desktop ${RPM_BUILD_ROOT}/usr/share/applnk/Applications # RH KDE +mv etc/ProofGeneral.desktop ${RPM_BUILD_ROOT}/etc/X11/applnk/Applications # RH Gnome + +for f in */README; do mv $f $f.`dirname $f`; done + +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/share/info/ProofGeneral.info.* /usr/share/info/dir +/sbin/install-info /usr/share/info/PG-adapting.info.* /usr/share/info/dir + +%preun +/sbin/install-info --delete /usr/share/info/ProofGeneral.info.* /usr/share/info/dir +/sbin/install-info --delete /usr/share/info/PG-adapting.info.* /usr/share/info/dir + +%files +%attr(-,root,root) %doc AUTHORS BUGS CHANGES COPYING INSTALL README.* REGISTER doc/* */README.* +%attr(-,root,root) /usr/share/info/ProofGeneral.info.* +%attr(-,root,root) /usr/share/info/ProofGeneral.info-*.* +%attr(-,root,root) /usr/share/info/PG-adapting.info.* +%attr(-,root,root) /usr/share/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/bin/isartags +%attr(-,root,root) /usr/share/icons/pgicon.png +%attr(-,root,root) /usr/share/pixmaps/pgicon.png +%attr(-,root,root) /usr/share/icons/mini/pgmini.xpm +%attr(-,root,root) /usr/lib/menu/ProofGeneral +%attr(-,root,root) /usr/share/applnk/Applications/ProofGeneral.desktop +%attr(-,root,root) /etc/X11/applnk/Applications/ProofGeneral.desktop +%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..62c7c417 --- /dev/null +++ b/etc/README @@ -0,0 +1,34 @@ +Files in the PG/etc directory (NB: some only in devel distrib) +=============================================================== + +README this file + +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. + +ProofGeneral.desktop Menu file for some Linux versions. + Install in /etc/X11/applnk/Applications/ + +announce Announcement + +lego Files for testing LEGO Proof General +isa Isabelle Proof General +isar Isar PG +demoisa Isabelle Demo PG + + +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 + +release-log.txt A record of official releases + +testing-log.txt Notes on testing +test-schedule.txt +TESTS + + 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..39a31654 --- /dev/null +++ b/etc/announce @@ -0,0 +1,48 @@ + Announcing Proof General Version 3.4 + 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 HOL98, 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 with X-Symbol +. Activation of prover output for subterm navigation, proof-by-pointing +. 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.3: + +. GPL license +. Improvements to menus, colour schemes +. Visibility control over portions of proof script +. In Isabelle: tracing buffers, dependency highlighting support +. In Coq: much improved synchronization (inc sections, nested proofs) +. Bug fixes, efficiency improvements, better generic code. +. Compatibility improvements: XEmacs 21.4, Emacs 21.2 + +For details of changes since 3.3, see +http://www.proofgeneral.org/fileshow.php?file=ProofGeneral-3.4%2FCHANGES + +For the latest user manual, see http://www.proofgeneral.org/doc + +Proof General needs a recent version of Emacs to run with. Proof +General 3.4 has been tested with XEmacs 21.1 and 21.4, and GNU Emacs +21.2. Older versions of either XEmacs may work but are not +guaranteed. + +Installing Proof General is easy. Why not give it a try? + + - David Aspinall <da@proofgeneral.org> + August 2002. + diff --git a/etc/announce-header.txt b/etc/announce-header.txt new file mode 100644 index 00000000..80e401fc --- /dev/null +++ b/etc/announce-header.txt @@ -0,0 +1,28 @@ +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] 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/naming.v b/etc/coq/naming.v new file mode 100644 index 00000000..ee078a60 --- /dev/null +++ b/etc/coq/naming.v @@ -0,0 +1,49 @@ +(* Coq theorems, etc can be named at the top .... *) + +Theorem and_comms: (A,B:Prop)(A /\ B) -> (B /\ A). + Intros A B H. + Induction H. + Apply conj. + Assumption. + Assumption. +Qed. + +(* at the bottom... *) + +Goal (A,B:Prop)(A /\ B) -> (B /\ A). + Intros A B H. + Induction H. + Apply conj. + Assumption. + Assumption. +Save and_comms2. + +(* or not at all! *) +(* 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)(A /\ B) -> (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! *) + +(* TESTING: notice output window behaviour here with different settings: + exact output displayed also depends on how many steps are issued + at once. +*) + +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/coq/nested.v b/etc/coq/nested.v new file mode 100644 index 00000000..bd447157 --- /dev/null +++ b/etc/coq/nested.v @@ -0,0 +1,99 @@ +(* Testing nested Proofs, and backtrack mechanism in general. + + BUGS: + + - Nested sections... + +======= Below here fixed + + - Retract 7a -> 6 needs to do 3 sorts of undo commands! + Abort, Undo, Back. + Algorithm is to use current search-forwards from target span + mechanism, which has to cover the whole range of undo to count + all the Backs. However, only the initial Undo's which appear + before an Abort need to be counted. (See coq-find-and-forget). + + - Undo of "Require Omega" in proof uses Undo instead of Back. + [ coq-count-undos needs fixing to use Back as well as Undo ? ] + + - once point 12 is reached, sould have one + block from 3 to 12. With the goalsave test : + OK but the reset command is wrong. + + - From point 5, retract to point 1: "Abort. Back 5." Argl + Wrong, tactics and line 3 are counted for Back!! + This comes from my modification of coq-find-and-forget + function. + + - point 7 is not well backtracked, but this can be solved easily + in coq.el. + *) + +Require Logic. (* 1 This needs "Back 1" to be retracted *) +Require List. (* 2 This needs "Back 1" to be retracted *) + + +Section Apple. + +(* 2a. *) +Fixpoint f [n:nat] : nat := Cases n of O => O | (S m)=> (f m) end. +(* 2b. Retraction to 2a from here uses "Reset". + Retraction to 2a from inside proof uses "Abort. Back." *) + + +Lemma t1: (n: nat ) {n=O} + {(EX y | n = (S y))}. +(* 3 This needs "Restart" to be retracted if inside the proof, and +"Reset t1. Back 4." if outside (after point 12). 3 because of the +Require and the two lemmas inside the proof. If only "Reset t1", like +with the current version of PG, then t2 and t3 are still in the +environment. Try this with the current version and with my patch *) + +(* da: Back command seems much better behaved than "Reset", which + always clears proof state, I think. Should PG always use Back? *) + +Intros. (* 4 This needs "Undo" to be retracted *) +Case n. (* 5 "Undo" *) +EAuto. (* 6 "Undo" *) +Definition foo:=O. (* 6.5 between 6 and 7 *) +Require Omega. (* 7 This needs "Back 1" to be retracted. *) + Lemma t2 : O=O. (* 7a. -> 6: "Abort. Back 1. Undo 1." *) + Auto. + Print f. (* a non-undoable "tactic" *) + Lemma t4 : O=O. + Auto. (* 7b. -> 6: "Abort. [Undo.] Abort. Back 1. Undo 1." *) + (* 7b. -> 2: "Abort. Abort. Abort. Back 1." + This is a useful test case because PG splits + undo calculation into phases: outwith + top-level proof and within top-level proof. *) + Save. + Save. (* 8 "Back 1" or "Reset t2". *) + Proof. (* another non-undoable... *) +Intros. (* 9 "Undo": example of retraction 9->6: Undo 2. Back 3. *) + Fixpoint g [n:nat] : nat := Cases n of O => O | (S m)=> (g m) end. (*7*) + Lemma t3 : O=O. Auto. Save. (* 10 "Back 1" or "Reset t3" *) +EAuto. (* 11 "Undo" *) +Save. (* 12 *) + +End Apple. + +Section Banana. + +Lemma Coq: O=O. Auto. Save. (* silly example to show that testing + prompt in coq-proof-mode-p to determine + if we're in proof mode is not good enough. + Hopefully nobody calls their theorems "Coq".*) + +End Banana. + +(* Nested sections? + Oh no, this is too horrible to even think about. *) + +Section Cranberry. + + Section Damson. + + Lemma CoqIsStrange: O=O. Auto. Save. + + End Damson. + +End Cranberry. diff --git a/etc/coq/parsing.v b/etc/coq/parsing.v new file mode 100644 index 00000000..be64e62e --- /dev/null +++ b/etc/coq/parsing.v @@ -0,0 +1,11 @@ +(* Here's a test of a + + (* nested comment: + Since Coq has them, PG ought to be able to deal + with them. They work fine in GNU Emacs, but + problematical in XEmacs. *) +*) + +Require Logic. + +(* Comment at the end here. *) diff --git a/etc/coq/queryreplace.v b/etc/coq/queryreplace.v new file mode 100644 index 00000000..d368d013 --- /dev/null +++ b/etc/coq/queryreplace.v @@ -0,0 +1,51 @@ +(* STATUS: Solved. This was caused by the anyway faulty + proof-zap-commas-region failing to save the match data. + See comments in proof-syntax.el about that function. +*) + +(* +From: Cuihtlauac ALVARADO <cuihtlauac.alvarado@francetelecom.com> +To: David Aspinall <da@dcs.ed.ac.uk> +Subject: broken query-replace +Date: 09 Jul 2002 11:09:03 +0200 + +BTW, there's something stange I've forgot to post. + +In FSF-emacs PG & global-font-lock-mode does not play well together. Add + +(global-font-lock-mode t) + +in your .emacs an then try to query-replace "dom" by "foo" in + +*) + +Record t : Type := make { + dom : Set; + null : dom; + inv : dom->dom; + op : dom->dom->dom; + null_l : (x:dom)x=(op null x); + null_r : (x:dom)x=(op x null); + inv_l : (x:dom)null=(op (inv x) x); + inv_r : (x:dom)null=(op x (inv x)); + assoc : (x,y,z:dom)(op x (op y z))=(op (op x y) z); + inv_null : null=(inv null); + inv_inv : (x:dom)x=(inv (inv x)); + assoc_inv_l : (x,y:dom)y=(op (inv x) (op x y)); + assoc_inv_r : (x,y:dom)y=(op x (op (inv x) y)); + inv_op : (x,y:dom)(op (inv y) (inv x))=(inv (op x y)) + }. + + +(* + +assoc, assoc_inv_l, assoc_inv_r and inv_op occurences of "dom" are +replaced by "fooom" instead of "dom", quite strange is'n it ? + +Query-replacing "dom" by "bar" leads to "barom", which make me thinks +only the first letter of the pattern is replaced... + +I've seen this strange behaviour for a while, it was present in +earlier versions of PG & emacs. + +*) diff --git a/etc/cvs-tips.txt b/etc/cvs-tips.txt new file mode 100644 index 00000000..a8b8fc7f --- /dev/null +++ b/etc/cvs-tips.txt @@ -0,0 +1,114 @@ +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 +====================== + +This only works on a clean repository (no spurious files): + + 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..a5c43756 --- /dev/null +++ b/etc/debugging-tips.txt @@ -0,0 +1,49 @@ +Tips for Debugging Proof General -- David Aspinall, 1999,2002 +=============================================================== + +Emacs debug flags +================= + +If Proof General gives an error, you can set the Emacs debug +flag to find out where in the code it occurs, showing a +stack trace: + + (setq debug-on-error t) ; debug on errors + (setq debugon-on-quit t) ; debug on CTRL-G for looping code + +You can make settings like this using M-x set-variable, writing Lisp +code as above in the *scratch* buffer, and typing C-x C-e to evaluate +the expressions, or using M-x eval-expression (ESC-:). + + +Quick hints for edebug (source-level debugger) +============================================== + +Source-level debugging is more useful than backtraces, especially if +you are writing your own additions for Proof General. + +Load the source file <foo>.el, and locate the function you +want to debug. Type + + M-x debug-defun RET + +to instrument it for debugging. + +When the code reaches the function it will enter the source-level +debugger. Keep pressing space to step through and see the result of +evaluating sub-expressions, or hit "c" to continue. + +Pressing ? gives more commands. + + + +Proof General debug messages +============================ + +Proof General includes internal debugging messages. +Make these settings to see them: + + (setq proof-tidy-response nil) ; response buffer never clears + (setq proof-show-debug-messages t) ; debug messages appear in response buffer + + 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/completed-proof.ML b/etc/isa/completed-proof.ML new file mode 100644 index 00000000..70cc8e18 --- /dev/null +++ b/etc/isa/completed-proof.ML @@ -0,0 +1,43 @@ +(* Test of completed proof behaviour: even if qed command is missing, + PG should close of the proof as a goalsave. + + Issue with Isabelle2002: Goals.disable_pr prevents + proof-shell-proof-completed being set because "No Subgoals!" is not + displayed. This means that processing file in one go here (or C-c + C-RET at val_) does not work properly. +*) + +(* default proof-completed-proof-behaviour for isa is 'closeany. + Also should test this file with 'closegoal, 'extend. + + (setq proof-completed-proof-behaviour 'closeany) + : close on any command after proof completed seen + (setq proof-completed-proof-behaviour 'closegoal) + : close when next goal is seen + (setq proof-completed-proof-behaviour 'extend) + : continually extend region after proof completed, until next goal. + + *) + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); + (* qed "and_comms"; *) + +val _ = (); +val _ = (); + +Goal "A & B --> B & A"; + by (rtac impI 1); + by (etac conjE 1); + by (rtac conjI 1); + by (assume_tac 1); + by (assume_tac 1); + qed "and_comms"; + + + + 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/parsing.ML b/etc/isa/parsing.ML new file mode 100644 index 00000000..805e69fb --- /dev/null +++ b/etc/isa/parsing.ML @@ -0,0 +1,13 @@ +(* Any (* nested comments *) are tricky in XEmacs (21.4.8), + but better syntax handling in Emacs at the moment. +*) + +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"; + +(* Comment at the end?! *)
\ No newline at end of file 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/Fibonacci.thy b/etc/isar/Fibonacci.thy new file mode 100644 index 00000000..0cbc8090 --- /dev/null +++ b/etc/isar/Fibonacci.thy @@ -0,0 +1,149 @@ +(* Fibonacci.thy taken from Isabelle distribution + Gertrud Bauer / Larry Paulson *) + +theory Fibonacci = Primes: + +subsection {* Fibonacci numbers *} + +consts fib :: "nat => nat" +recdef fib less_than + "fib 0 = 0" + "fib (Suc 0) = 1" + "fib (Suc (Suc x)) = fib x + fib (Suc x)" + +lemma [simp]: "0 < fib (Suc n)" + by (induct n rule: fib.induct) (simp+) + + +text {* Alternative induction rule. *} + +theorem fib_induct: + "\<lbrakk>P 0; P 1; \<And>n. \<lbrakk>P (n + 1); P n\<rbrakk> \<Longrightarrow> P (n + 2)\<rbrakk> \<Longrightarrow> P (n::nat)" + by (induct rule: fib.induct, simp+) + + +subsection {* Fib and gcd commute *} + +text {* A few laws taken from \cite{Concrete-Math}. *} + +lemma fib_add: + "fib (n + k + 1) = fib (k + 1) * fib (n + 1) + fib k * fib n" + (is "?P n") + -- {* see \cite[page 280]{Concrete-Math} *} +proof (induct n rule: fib_induct) + show "?P 0" by simp + show "?P 1" by simp + fix n + have "fib (n + 2 + k + 1) + = fib (n + k + 1) + fib (n + 1 + k + 1)" by simp + also assume "fib (n + k + 1) + = fib (k + 1) * fib (n + 1) + fib k * fib n" + (is " _ = ?R1") + also assume "fib (n + 1 + k + 1) + = fib (k + 1) * fib (n + 1 + 1) + fib k * fib (n + 1)" + (is " _ = ?R2") + also have "?R1 + ?R2 + = fib (k + 1) * fib (n + 2 + 1) + fib k * fib (n + 2)" + by (simp add: add_mult_distrib2) + finally show "?P (n + 2)" . +qed + +lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (n + 1)) = 1" (is "?P n") +proof (induct n rule: fib_induct) + show "?P 0" by simp + show "?P 1" by simp + fix n + have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)" + by simp + also have "gcd (fib (n + 2), ...) = gcd (fib (n + 2), fib (n + 1))" + by (simp only: gcd_add2') + also have "... = gcd (fib (n + 1), fib (n + 1 + 1))" + by (simp add: gcd_commute) + also assume "... = 1" + finally show "?P (n + 2)" . +qed + +lemma gcd_mult_add: "0 < n ==> gcd (n * k + m, n) = gcd (m, n)" +proof - + assume "0 < n" + hence "gcd (n * k + m, n) = gcd (n, m mod n)" + by (simp add: gcd_non_0 add_commute) + also have "... = gcd (m, n)" by (simp! add: gcd_non_0) + finally show ?thesis . +qed + +lemma gcd_fib_add: "gcd (fib m, fib (n + m)) = gcd (fib m, fib n)" +proof (cases m) + assume "m = 0" + thus ?thesis by simp +next + fix k assume "m = Suc k" + hence "gcd (fib m, fib (n + m)) = gcd (fib (n + k + 1), fib (k + 1))" + by (simp add: gcd_commute) + also have "fib (n + k + 1) + = fib (k + 1) * fib (n + 1) + fib k * fib n" + by (rule fib_add) + also have "gcd (..., fib (k + 1)) = gcd (fib k * fib n, fib (k + 1))" + by (simp add: gcd_mult_add) + also have "... = gcd (fib n, fib (k + 1))" + by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel) + also have "... = gcd (fib m, fib n)" + by (simp! add: gcd_commute) + finally show ?thesis . +qed + +lemma gcd_fib_diff: + "m <= n ==> gcd (fib m, fib (n - m)) = gcd (fib m, fib n)" +proof - + assume "m <= n" + have "gcd (fib m, fib (n - m)) = gcd (fib m, fib (n - m + m))" + by (simp add: gcd_fib_add) + also have "n - m + m = n" by (simp!) + finally show ?thesis . +qed + +lemma gcd_fib_mod: + "0 < m \<Longrightarrow> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" +proof - + assume m: "0 < m" + show ?thesis + proof (induct n rule: nat_less_induct) + fix n + assume hyp: "ALL ma. ma < n + --> gcd (fib m, fib (ma mod m)) = gcd (fib m, fib ma)" + show "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)" + proof - + have "n mod m = (if n < m then n else (n - m) mod m)" + by (rule mod_if) + also have "gcd (fib m, fib ...) = gcd (fib m, fib n)" + proof cases + assume "n < m" thus ?thesis by simp + next + assume not_lt: "~ n < m" hence le: "m <= n" by simp + have "n - m < n" by (simp! add: diff_less) + with hyp have "gcd (fib m, fib ((n - m) mod m)) + = gcd (fib m, fib (n - m))" by simp + also from le have "... = gcd (fib m, fib n)" + by (rule gcd_fib_diff) + finally have "gcd (fib m, fib ((n - m) mod m)) = + gcd (fib m, fib n)" . + with not_lt show ?thesis by simp + qed + finally show ?thesis . + qed + qed +qed + + +theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n") +proof (induct m n rule: gcd_induct) + fix m show "fib (gcd (m, 0)) = gcd (fib m, fib 0)" by simp + fix n :: nat assume n: "0 < n" + hence "gcd (m, n) = gcd (n, m mod n)" by (rule gcd_non_0) + also assume hyp: "fib ... = gcd (fib n, fib (m mod n))" + also from n have "... = gcd (fib n, fib m)" by (rule gcd_fib_mod) + also have "... = gcd (fib m, fib n)" by (rule gcd_commute) + finally show "fib (gcd (m, n)) = gcd (fib m, fib n)" . +qed + +end diff --git a/etc/isar/Parsing.thy b/etc/isar/Parsing.thy new file mode 100644 index 00000000..60d47e3d --- /dev/null +++ b/etc/isar/Parsing.thy @@ -0,0 +1,73 @@ +(* 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. *) + +(* At the moment, successive comments are amalgamated, and comments + following commands are wrapped into the command (so cannot be + hidden). *) + +text {* Isar theories can have arbitrary literal text, + so the text must be ignored as well; thus. *} + +(* Those pieces of literal text are treated as another kind + of comment. What gets slight risky is when they're + text {* nested one inside the other. *}. + If Emacs confuses the two kinds of sequence, then + this can go wrong. +*) + +text {* nesting (* may be the other way around *) *} + +(* The main type of comment (* may be nested *) + just like in SML. GNU Emacs [21.1] supports this now, nicely, + but XEmacs [21.4.8] doesn't, so colouration goes wrong. + If there are any command names inside this comment + (e.g. theorem), it breaks the parser in XEmacs. + [ To process this in XEmacs, delete "thxxrem" above, C-c C-n, C-x u ] +*) + +(* 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 + +(* Another thing: nesting with { and } can be tricky. *) + +theorem and_comms_again: "A & B --> B & A" +proof + assume "A & B" + thus "B & A" + proof { + assume A B + show ?thesis + .. + } 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! + + Another oddity with comments at the end: these are left as "commands". *) + diff --git a/etc/isar/Persistent.thy b/etc/isar/Persistent.thy new file mode 100644 index 00000000..f9258ce5 --- /dev/null +++ b/etc/isar/Persistent.thy @@ -0,0 +1,40 @@ +(* + +We now support persistent Isabelle sessions with Proof General, preserving +the state of loaded theories (before I used to have a few explicit +``bombs'' to prevent this). When saying ``Exit Isabelle/Isar'' the image +is committed back. It's not possible to go continue partially processed +theory buffer, but users could expect to have a fully processed theory +stored properly. The latter requires scripting to be disabled first, in +order to inform the process to store the finished theory. + +To spare users to think about this, the ``Exit Isabelle/Isar'' +operation disables scripting automatically. + +Produce a writable Isabelle session like this: + + isabelle -q HOL Foo + +Now start PG and start a process with the Foo logic image. + +Tests: + + Process this file, exit, start. + Unprocess, exit, start. [FAILS with Isabelle2002] + +*) + + +theory Persistent = Main: + +theorem and_comms: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +end 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/XSymbolTests.thy b/etc/isar/XSymbolTests.thy new file mode 100644 index 00000000..6be971e2 --- /dev/null +++ b/etc/isar/XSymbolTests.thy @@ -0,0 +1,62 @@ +(* Some checks for X-Symbol behaviour. + $Id$ +*) + +theory XSymbolTests = Main: + + +(* 28.8.02: bug in pg-remove-specials broke this; now fixed *) + +lemma "A ==> A" . -- OK + +consts A :: bool +lemma "A ==> A" . -- "xsymbols not displayed?" + + +(* Test electric token input: writing a token +like \ <alpha> (without space, \<alpha>) should immediately +replace it. *) + +constdefs + P1 :: bool ("P\<^sub>1") (* subscript *) + "P\<^sub>1 == True" + P2 :: bool ("P\<^sup>2") (* superscript *) + "P\<^sup>2 == True" + +(* Buglet here: if we enable x-sym during scripting, + goals/response flks are not updated, so xsyms + do not appear in output windows. Stoping/starting + prover fixes. +*) + +theorem "P\<^sub>1 \<and> P\<^sup>2"; (* check fonts in goals window *) +by (simp add: P1_def P2_def) (* .. and response window *) +(* BUG: \<and> not appearing in response *) + +consts + "P\<^sup>\<alpha>" :: bool (* superscript of a token char *) + "\<^bold>X" :: bool (* bold character *) + + +(* Markus reports that \<cdot> is saved in the file as +an 8-bit character. I can't repeat that with XEmacs 21.4, +unless I set the relevant X-Symbol menu option. *) + +(* + Another X-Symbol oddity: sometimes the _first_ buffer to + be visited displays _some_ characters as \2xx, e.g. + for \<circ>. But subsequent buffers to be visited work + fine. Problem is stable for turning x-symbol on/off. + Revisting the first buffer cures the problem. + I can't easily repeat the problem... +*) + +consts + iter :: "('a => 'a) => nat => ('a => 'a)" +primrec + "iter f 0 = id" + "iter f (Suc n) = f \<circ> (iter f n)" + + +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/new-parsing-test.el b/etc/isar/new-parsing-test.el new file mode 100644 index 00000000..147ad476 --- /dev/null +++ b/etc/isar/new-parsing-test.el @@ -0,0 +1,38 @@ +;; +;; Temporary test for new code in proof-done-advancing, following +;; Markus's suggestions in proof-config +;; [see doc of proof-really-save-command-p] +;; +;; Not integrated yet for fear of destruction of finely tuned +;; PG/Isar instance. +;; +;; -da June 02. +;; +;; FIXME: the handling of nesting depth counter doesn't yet work +;; smoothly in the generic code, especially across undos/forget. +;; Need to fix when nesting depth is changed, how it is changed, +;; and choice of kill_proof vs undos for Isar. +;; +;; Testing: evaluate this buffer, reload script file +;; (to re-execute isar-mode). + +(setq proof-nested-goals-p t) +(setq proof-goal-command-regexp + (concat isar-goal-command-regexp "\\|" isar-local-goal-command-regexp)) + +(defun isar-goal-command-p (str) + "Decide whether argument is a goal or not" + (proof-string-match proof-goal-command-regexp str)) + +;; Reset this to default value +(setq proof-really-save-command-p (lambda (span cmd) t)) + +;; Use the new parser, but have to hack the keywords setting +;; to fix prob with "{" +;; [do we?? that was probably buffer-syntactic context/symtab problem] +(setq proof-script-use-old-parser nil) +(setq isar-any-command-regexp + (isar-ids-to-regexp isar-keywords-major)) +; (cons "{[^\\*]" ;; FIXME: +; (isar-ids-to-regexp +; (remove "{" isar-keywords-major)))) 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/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/pbp.l b/etc/lego/pbp.l new file mode 100644 index 00000000..66a6df72 --- /dev/null +++ b/etc/lego/pbp.l @@ -0,0 +1,30 @@ +(* How to prove a sample theorem by PBP. *) + +(* All using middle-clicks. + + 1. Click on -> (Pbp 0 3 1: Intros A B) + 2. Click on left (A/\B) (Pbp 1 2 1: Intros H; Try Refine H) + 3. Click on A (Pbp 4 2 1: Intros H1; Try Refine H1) + 4. Click on B (Pbp 5 2 1: Intros H2; Try Refine H2) + 5. Click on A in A/\B (Pbp 6 2 1: Refine pair; Try Assumption) + 6. Click on final B (Pbp 10: Try Assumption) + OR: + Click on assumption B (PbpHyp H2: Try Refine H2) + QED!! +*) + +Module pbp Import lib_logic; + +Goal {A,B:Prop}(A /\ B) -> (B /\ A); +Intros A B; +Intros H; Try Refine H; +Intros H1; Try Refine H1; +Intros H2; Try Refine H2; +Refine pair; Try Assumption; +Try Assumption; +Save and_comms; + + + + + 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..0fd7abff --- /dev/null +++ b/etc/proofgeneral-domain.txt @@ -0,0 +1,28 @@ +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@informatics.ed.ac.uk +feedback proofgen@informatics.ed.ac.uk +bugs proofgen@informatics.ed.ac.uk +eeproof proofgen@informatics.ed.ac.uk +da David.Aspinall@ed.ac.uk + +users proofgeneral@informatics.ed.ac.uk + http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral +devel proofgeneral-devel@informatics.ed.ac.uk + http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel + diff --git a/etc/release-log.txt b/etc/release-log.txt new file mode 100644 index 00000000..2c6c1544 --- /dev/null +++ b/etc/release-log.txt @@ -0,0 +1,71 @@ +29.08.02 3.4 Release 3-4 based on branch 7.0 + (repeated: RPM fixes; Isabelle binary search; CHANGES; splash screen) + +-------------------- + +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. + + + diff --git a/etc/testsuite/pg-pgip-test.el b/etc/testsuite/pg-pgip-test.el new file mode 100644 index 00000000..9dbfaad7 --- /dev/null +++ b/etc/testsuite/pg-pgip-test.el @@ -0,0 +1,16 @@ +;; Tests for pg-pgip.el +;; +;; $Id$ + +(pg-clear-test-suite "pg-pgip") +(pg-set-test-suite "pg-pgip") + +(pg-test-eval (pg-pgip-interpret-value "true" 'boolean) t) +(pg-test-eval (pg-pgip-interpret-value "false" 'boolean) nil) +(pg-test-eval (pg-pgip-interpret-value "27" 'integer) 27) +(pg-test-eval (pg-pgip-interpret-value "true" (list 'choice 'boolean 'integer)) t) +(pg-test-eval (pg-pgip-interpret-value "27" (list 'choice 'boolean 'integer)) 27) + + +(provide 'pg-pgip-test) +;; End of `pg-pgip-test.el'
\ No newline at end of file diff --git a/etc/testsuite/pg-test.el b/etc/testsuite/pg-test.el new file mode 100644 index 00000000..b8d236a7 --- /dev/null +++ b/etc/testsuite/pg-test.el @@ -0,0 +1,109 @@ +;; pg-test.el -- Simple test framework for Proof General. +;; +;; $Id$ +;; + +(defconst pg-test-buffer "** PG test output **") + +(defvar pg-test-total-success-count 0) +(defvar pg-test-total-fail-count 0) + +(defvar pg-test-suite-success-count 0) +(defvar pg-test-suite-fail-count 0) + +;; A test suite is a list of tests. +(defvar pg-test-suite-table nil) + +(defvar pg-current-test-suite nil) + +(defun pg-set-test-suite (name) + (setq pg-current-test-suite name) + (unless (assoc name pg-test-suite-table) + (setq pg-test-suite-table + ;; Add an empty subtable + (cons (cons name nil) pg-test-suite-table)))) + +(defun pg-clear-test-suite (name) + (setq pg-test-suite-table + (remassoc name pg-test-suite-table))) + + +(defmacro pg-test-eval (expr result) + "Add test (equal (eval EXPR) RESULT) to current test suite." + (let* ((suite (assoc pg-current-test-suite pg-test-suite-table)) + (testnum (length suite)) + (name (concat pg-current-test-suite "." (int-to-string testnum)))) + (setcdr suite (cons (list name 'eval expr result) (cdr suite))) + ;; Result is number of this test in suite + testnum)) + +(defun pg-execute-test (test) + (let ((name (car test)) + (type (cadr test))) + (cond + ((eq type 'eval) + (let ((expr (nth 2 test)) + (goodresult (nth 3 test)) + result errorresult exn) + (condition-case exn + (setq result (eval expr)) + ;; FIXME: add negative tests here, that exns _are_ raised. + (t (setq errorresult + (format " %s failed: error signalled: %s %s\n" + name (car exn) (cdr exn))))) + (or errorresult + (unless (equal goodresult result) + (setq errorresult + (format " %s failed: exprected result %s, got %s\n" + name goodresult result)))) + (if errorresult + (incf pg-test-suite-fail-count) + (incf pg-test-suite-success-count) + (setq errorresult (format " %s succeeded.\n" name))) + ;; Return string + errorresult)) + ;; No other types at the moment + (t + (error "Eek! unrecognized test type.")) + ))) + +(defun pg-execute-test-suite (name) + (interactive (list + (completing-read "Run test suite: " + pg-test-suite-table))) + (setq pg-test-suite-success-count 0) + (setq pg-test-suite-fail-count 0) + (save-excursion + (set-buffer (get-buffer-create pg-test-buffer)) + (insert "=================================================================\n") + (insert "TEST SUITE: " name "\n") + (insert "=================================================================\n") + (apply 'insert + (mapcar 'pg-execute-test + (reverse (cdr-safe + (assoc name pg-test-suite-table))))) + (insert (format + "\nTotal successful tests: %s, failed tests: %s\n\n" + pg-test-suite-success-count pg-test-suite-fail-count))) + (setq pg-test-total-success-count + (+ pg-test-suite-success-count pg-test-total-success-count)) + (setq pg-test-total-fail-count + (+ pg-test-suite-fail-count pg-test-total-fail-count))) + +(defun pg-execute-all-tests () + (interactive) + (pop-to-buffer + (get-buffer-create pg-test-buffer)) + (erase-buffer) + (sit-for 0) + (setq pg-test-total-success-count 0) + (setq pg-test-total-fail-count 0) + (mapcar 'pg-execute-test-suite (mapcar 'car pg-test-suite-table))) + + + + + + +(provide 'pg-test) +;; End of `pg-test.el' |