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 release
Message-Id: <93Jan19.085536met.8121@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 19 Jan 1993 08:55:34 +0100

First, a metaphor.


How to describe the experience of trying to finish a new release? The
image I've settled on is that of something nasty stuck to one's shoe,
that won't, no matter how vigourously one shakes and scrapes, come off.
Only after one has been thoroughly disgraced and has in exhaustion
accepted the possibility, nay the certainty, of a lifelong attachment,
does it drop off, the event provoking few emotions save a mild anxiety
about what to do next.


And now an announcement: hol90 version 4 is available for anonymous ftp
from Calgary.


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
general differences in the two systems lie in the "systems" 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.4 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 att.research.com and also princeton.
The installation guide in the sources gives full details. First though,
one must get the hol90 sources. These are available by anonymous ftp at
Calgary in the file

    pub/hol90/hol90.4.tar.Z

An example session would be

    % ftp fsa.cpsc.ucalgary.ca
    Connected to fsa.cpsc.ucalgary.ca.
    220 fsa.cpsc.ucalgary.ca FTP server ready.
    Name (fsa.cpsc.ucalgary.ca:slind): anonymous
    331 Guest login ok, send ident as password.
    Password:
    230 Guest login ok, access restrictions apply.
    ftp> cd pub/hol90
    250 CWD command successful.
    ftp> binary
    200 Type set to I.
    ftp> get hol90.4.tar.Z
            .
            .
            .
    ftp> quit
    %

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

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

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


* Credits

I would like to acknowledge the help of Elsa Gunter. She has not only
employed me but she has put in a great deal of work on the grottier
aspects of the implementation to smooth off the rough edges,
particularly in the area of libraries. And she has kept me honest in the
implementation more often than I wanted.