Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 4 Jan 1995 16:27:48 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA09662;
          Wed, 4 Jan 1995 09:19:03 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA09658;
          Wed, 4 Jan 1995 09:18:58 -0700
Received: from swan.cl.cam.ac.uk (swan.cl.cam.ac.uk [128.232.0.56]) 
          by dworshak.cs.uidaho.edu (8.6.9/1.0) with ESMTP id IAA29912 
          for <info-hol@cs.uidaho.edu>; Wed, 4 Jan 1995 08:16:52 -0800
Received: from albatross.cl.cam.ac.uk (user drs1004 (rfc931)) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl;
          Wed, 4 Jan 1995 16:16:25 +0000
To: info-hol@cs.uidaho.edu
Subject: Patches to TkHolWorkbench 0.1b available
Date: Wed, 04 Jan 1995 16:16:21 +0000
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:115350:950104161639"@cl.cam.ac.uk>


Dear fellow HOL users,

I have prepared patches 1 to 3 for TkHolWorkbench 0.1b.
For Cambridge people, the patches have already been 
applied to the installation under
/usr/groups/hol/interfaces/TkHolWorkbench.

If you have downloaded a copy of TkHolWorkbench you
should consider applying these patches to your installation.
This should be quite easy and quick to do - just follow
the instructions below.

Since TkHolWorkbench is under development, potential users
should note that patches will be released fairly frequently,
at the rate of about once every 2 weeks.
Until the product is more mature, it may not
be worth your while to apply every patch, but instead
to update your version at later times.  Patch files 
will always be available to upgrade your version to the most
recent one availale from any previous release (thanks
to the wonders of CVS).

Instead of applying the patches, you may at any time simply
download the latest copy of the release file
ftp://ftp.cl.cam.ac.uk/hvg/contrib/TkHolWorkbench/TkHolWorkbench.0.1
.tar.gz and reinstall from scratch.

Please let me know if you have trouble applying the patches,
or indeed if you successfully apply them.


Cheers,
Don


Changes and Fixes in the patches
--------------------------------

If you have used "tktheoryviewer", please note its name has changed
to "tkholhelper".


Version 0.1bp3: (4/1/95)
	- Added new "setup" installation procedure.

	- Moved runpackages from ./runpackages/ into ./bin/

	- Removed "install.sh" which is replaced by the "setup"
	program.

	- Fixed bug in TkTRS under hol90.  The current theory
	wasn't being displayed in the list of searchable theories.

Version 0.1bp2: (30/12/95)
	- Fixed bug which caused error when the empty string was
	executed from TkHolShell.

	- Fixed colouring bugs in TkHolShell.

	- Disabled "help" function in TkHolShell.

	- Made "quit()" in HOL88 from TkHolShell quit the application.

	- Added safety checks to catch failure of a bad HOL executable,
	and also to catch untimely death of the HOL slave.

	- Fixed bugs which meant that -hol <hol90 exectutable saved by
	save_hol> didn't work without a -theory flag to indicate the
	top theory.  Any hol90 executable is now OK.

	- Name change of "tktheoryviewer" -> "tkholhelper"

	- Fixed non-appearence of main window in tktheoryviewer (now
	tkholhelper).

	- Fixed bugs in notification routines which meant that things
	failed everytime a theorem was saved in the TkGoalProof 
	window in tkholwb.

Version 0.1bp1: (13/12/94)
	- Fixed small mistakes in TkGoalProof window, including the
	"Entire Tactic" which wasn't appearing.

	- Added automatic button defaulting to TkGoalProof window.

	- Fixed a small bug in error reporting.

Version 0.1bp0:
	- Initial version



Applying the patches
--------------------

1. Getting the right patch file.

The patch files are available via FTP from:

	ftp://ftp.cl.cam.ac.uk/hvg/contrib/TkHolWorkbench

Before you can get the right patch file, you must
find out the current patch level of your version.  In
future versions you will simply be able to look in the file
"TkHolWorkbench/patchlevel.tcl".  In this release, that file
isn't present.  Instead, use the following guide:
	- if you downloaded TkHoLWorkbench before 14:00 Dec 13th
1994 then you are at patch level 0
	- if after then your are at patch level 1.

Then choose the relevant file from:

 232 -rw-r--r--  1 drs1004    222337 Jan  4 15:55 TkHolWorkbench.patch.0.1bp0-0.1bp3
 224 -rw-r--r--  1 drs1004    213058 Jan  4 15:55 TkHolWorkbench.patch.0.1bp1-0.1bp3


Once you have the file, copy it to your TkHolWorkbench installation
directory.

2. Applying the patch

Move to the TkHolWorkbench installation directory and type
	patch -f -p < [patch-file]

"patch" will complain about a few small problems associated
with the expansion of RCS tags in files - look through the 
reject files if you want to check that nothing important has gone
wrong.

"patch" may also complain about some files which have disappeared,
claiming that the patch is a "reverse patch".  Don't
worry about this - its shouldn't really effect things.


3. Run the new "setup" program

Read the notes in "INSTALL" and run "./setup".