Date: Tue, 15 Oct 91 06:31:19 MDT
From: slind@ca.ucalgary.cpsc (Konrad Slind)
Message-Id: <9110151231.AA22399@fsa.cpsc.ucalgary.ca>
To: info-hol@edu.uidaho.cs.ted

hol90 now runs on vax, m68k, sun4 and big-and-little-endian mips
architectures. The hol90 directory no longer carries an SML/NJ
executable; you have to make your own, but this is not very hard.
One must ftp several files now:

    1. 73/mo.<arch>.tar.Z, where <arch> is the architecture you want
       to run on (and are compiling on!). The architecture may be
       found by invoking bin/arch in the shell.
    2. 73/src.tar.Z
    3. hol90.tar.Z

(73/lib.tar.Z and 73/doc.tar.Z are probably also useful.)

An example session would be

    gh% 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
    250 CWD command successful.
    ftp> binary
    200 Type set to I.
    ftp> get hol90.tar.Z
            .
            .
            .
    ftp> cd 73
    250 CWD command successful.
    ftp> get mo.<arch>.tar.Z
            .
            .
            .
    ftp> get mo.src.tar.Z
            .
            .
            .
    ftp> quit
    gh%

Once you have unpacked these directories someplace, make an sml:

    cd src
    makeml

This will leave an sml interactive system in src/sml.

Once you have an sml, it is possible to make hol90. First you have to
set the theory path. This is done by editing the variable "theory_path"
in the file hol90/globals.sml. The prefix of the path must be changed;
the prefix is "/home/vlsi/hol90". Replace it with the absolute path to
where you put the hol90 directory.

The shell script make_hol will make the system. It takes about 35
minutes on a 48 Meg. SPARC2. In general, you want to build hol90 on the
machine with the most memory.

Thanks to John Van Tassel for help with this.

If you have problems getting or building hol90, please let me know.


Konrad.