Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Mon, 4 Dec 1995 13:37:43 GMT
Message-Id: <9512041337.AA09742@adder.cl.cam.ac.uk>
From: John Carroll <John.Carroll@cl.cam.ac.uk>
To: info-hol@leopard.cs.byu.edu
Subject: Re: Need help to run HOL on a new Mac

>I have to appeal to the HOL community for help.  I have been trying to
>get HOL to work on my new Macintosh, and every different path I have
>tried has been blocked.
>...
>

I think you've tried all the right things with respect to getting HOL88
to run on your new 8500. I hope Digitool find their bug soon

>So I said, all right, perhaps it is simply time to bite the bullet and
>move to HOL90.  It means having to rework my HOL88 code, but I knew I 
>had to do this eventually.  So I found a copy of the SML application 
>for the Mac by Elsa Gunter from the net.  I took it home and ran it on
>the 8500, and it crashed, saying that it required a 68030 or better
>microprocessor with a floating point unit.  (So I guess it would
>probably work fine on my IIfx!)
>
>Well, the 8500 emulates the 68030, and has a powerful floating point
>unit in it, so I realized that the SML application had simply not been
>updated for the newest machines that Apple had put out.  No fault here;
>Elsa has better things on her mind nowadays than keeping up with
>mods to old software.  But again I am blocked; without SML, I cannot
>even begin to build HOL90 on the 8500.

Applications which test for the presence of a hardware FPU can usually
be run after installing softwarefpu:

<ftp://sunsite.doc.ic.ac.uk//computing/systems/mac/Collections/umich/system.extensions/cdev/softwarefpu3.03.sit.hqx.gz>

This is shareware. The Mac will then _appear_ to have a hardware FPU,
and hopefully SML will start up

John