Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: info-hol@edu.uidaho.cs.ted
Subject: hol90 version 5 release
Message-Id: <93Mar13.175842met.8116@sunbroy14.informatik.tu-muenchen.de>
Date: Sat, 13 Mar 1993 17:58:31 +0100


hol90 version 5 is available for anonymous ftp from Munich and Bell Labs.

This release is not a big change from version 4. The reasons for it are:
to synchronize with the latest release of SML/NJ, to make some important
libraries available, and to fix a few bugs in the implementation of
libraries. Installation is a bit simpler, so make sure to read the
installation instructions!


System overview.

hol90 is a re-implementation in SML/NJ of the Cambridge HOL system,
version 2.01. The proof support of hol90 (term manipulation, axioms,
inference rules, tactics, conversions, theories, libraries, etc.) is
intended to be an identical replacement for that of hol88, version 2.01.

There are of course some differences in the two systems. These are
discussed in detail in the release notes that come with the system. The
differences between the two systems generally lie in the "systems
support" aspect: how paths are administered, how autoloading works, the
nature of theory files, how quotation, antiquotation, and prettyprinting
work, etc.

hol90 runs proofs 2 to 4 times faster than hol88, but requires a
workstation with a lot of memory: 16Meg. does not give a large SML/NJ
program much breathing room. I recommend at least 24 Megabytes. The
hol90.5 image is approximately 8.2 Meg on disk and constructs a large
heap at runtime.


How to get it.

To build hol90, one must have the SML/NJ compiler, version 0.92 or
greater, which is available from research.att.com and also princeton.edu.
The installation guide in the hol90 sources gives full details. First
though, one must get the hol90 sources. These are available by anonymous
ftp from 

    Site                                File
    ----                                ----
    ftp.informatik.tu-muenchen.de      lehrstuhl/nipkow/hol90/hol90.5.tar.Z
or
    research.att.com                   dist/ml/hol90/hol90.5.tar.Z


An example session would be

    % ftp ftp.informatik.tu-muenchen.de
    Connected to dsrbg2.informatik.tu-muenchen.de.
    220 dsrbg2 FTP server (Version 6.10 Wed Mar 4 03:23:45 MET 1992) ready.
    Name (ftp:slind): anonymous
    331 Guest login ok, send e-mail address as password.
    Password:

        .
        .
    < a banner appears >
        .
        .

    230 Guest login ok, access restrictions apply.
    ftp> cd lehrstuhl/nipkow/hol90
    250 CWD command successful.
    ftp> binary
    200 Type set to I.
    ftp> get hol90.5.tar.Z
            .
            .
            .
    ftp> quit
    %

Once you have hol90.5.tar.Z, it can be unpacked by

    zcat hol90.5.tar.Z | tar xf -

This gives a directory hol90.5, with subdirectories "contrib", "doc",
"src", "help", "library", "tools", and "theories". The installation
guide is in the file "install.doc" in hol90.5/doc. 


* Miscellaneous

Since this is a new release, users will have to rebuild all of their
theory files.

hol90 will no longer be available from the Calgary ftp site.


* Credits

Many thanks to Matthew Morley, Richard Boulton, KimDam Peterson,
Flemming Anderson, Paul Loewenstein, and David Shepherd. They did most
of the work in porting the libraries.