Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Message-Id: <m0osxYx-0000kLC@nfs.research.att.com>
Date: Fri, 29 Oct 93 13:24 EDT
From: elsa@research.att.com (Elsa Gunter)
To: info-hol@cs.uidaho.edu, d_ellis@ricks.enet.dec.com
Subject: hol90.6 at ATT

Dear HOL community:
  A while ago (a few months) a version of hol90.6 was put up on
research.att.com which had a bug in it that cause the system build to
crash in the very final steps of building.  I had actually attempted
to build the system and had it crash on me, but I negligently forgot
to remove the file hol90.6.tar.Z from the ftp site.  Thanks to Konrad,
the bug has been fixed and a new version of hol90.6 now exists.  I
have checked it by building it in various modes on various machines
here at ATT, and it checks out as being quite robust.  However, I
suffer a problem at ATT at present.  The network here has been
seriously disconnected and it is impossible for me to gain internal
access to the ftp site to remove the bad version and replace it with
the corrected one.  To help those who picked up the bad version, I
have ftped a copy the correct version of hol90.6.tar.Z into 

	   research.att.com:dist/ml/incoming/hol90.6.tar.Z

from where you should be able to annonymously ftp it.

CAUTION: DO NOT ftp the version of hol90.6 from dist/ml/hol90


The fix to hol90.6 is quite small, and I enclose it here for those who
would prefer to do a little hacking than to do an ftp.

Fix: in the file hol90.6/src/3/sys_lib.sml, line 29, replace

    else Library.find_library "HOL";

by

    else let val h_lib = Library.find_library "HOL"
         in Library.move_library(h_lib, !Globals.HOLdir);
            h_lib
         end;

If you have any trouble with any of the above, please feel free to
contact me.
				---Elsa

				elsa@research.att.com