Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Thu, 30 Nov 1995 16:18:28 -0800
From: homeier@uniblab.aero.org (Peter Homeier)
Message-Id: <9512010018.AA14907@baggins.itd>
To: info-hol@leopard.cs.byu.edu
Subject: Need help to run HOL on a new Mac
Cc: slh@digitool.com, wfs@fireant.ma.utexas.edu, info@tenon.com, 
    homeier@cs.ucla.edu

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 recently completed my Ph.D. work on a older Macintosh, a IIfx, to which
I had ported a copy of Macintosh Common Lisp (MCL) v2.0b1.  I was able to
somewhat rework the f-cl.l file so that it all compiled and loaded, for
HOL88 versions 2.01 and 2.02.

This was fine, and I was able to create a fairly large system of about
57000 lines of source for 22 theories.  The only problem was that after
about 6 hours of continuous theorem crunching, the system would always
freeze up.  I suspect there was a memory leak somewhere in the Lisp, but
have never been able to track it down.  The effect was to limit the 
size of the examples of programs I was able to verify using my prototype
verification system.

After graduating, I decided the time was right to finally get an upgrade
for my Macintosh.  Accordingly, I purchased a bright and beautiful new
Power Macintosh 8500 from the UCLA student store, with a new monitor and
everything.  The microprocessor is a hot Power PC 604, clocked at 120 MHz.
I raised the memory to 48 Meg and got a 2 Gig HD, installed System 7.5.2,
and thought I was all set for greater and higher theorem proving than ever 
before.

My first plans were to port HOL88 to the 8500, just to recreate what I
had running before with minimal effort, and then eventually to move over
to HOL90, where the bulk of HOL users appear to be.  For the HOL88, I
purchased the newest version of MCL (v3.0p2) from the new vendor, Digitool.
But just for good measure, I found that there was an apparently very well-
done version of UNIX for the Power Macintosh being sold by Tenon, at a
reasonable price for academic users, and I got this as well.  This version
of UNIX is called "MachTen v4.0", and is native on the Power Macs. so 
very speedy.  I have played around with this for awhile and am quite 
impressed; they seem to have done a really fine job of creating a good
implementation of UNIX on the Mac that integrates well with the
rest of the Macintosh system, and has considerable power.

OK, for the port of HOL88 to the 8500, I installed MCL v3.0p2 (along with
a patch to improve the caching) and tried building the HOL system.  All
of the Lisp files seemed to compile fine, but when I started compiling and
loading the ML files, the Lisp would crash repeatedly and predicatably.
I have reported this to Steve Hain at Digitool, along with binaries of the
ML, Lisp, and object files involved, and he has said that he is looking
into it.  But so far there have been no resolution as to the cause of the 
bug.

I tried using the previous version of MLC, v2.0b1, that I had running on
my Mac IIfx, but it did not behave properly on the new Power Macintosh
Hardware.  The cursor appeared as a scrambled bit pattern, and other
things were weird too.  However HOL88 did compile and load, and I could
get my Ph.D. code running.  The only problem was that it was THREE TIMES
SLOWER on the 8500 (with a 120 MHz 604 microprocessor) than on the IIfx
(with a 40 MHz 68030 microprocessor)!!!

All right, I said, let's just try something else.  I went and found the
sources for both AKCL and for GCL v2.2, and transferred them to the 8500.
I brought up the MachTen UNIX, and untarred AKCL (with its KCL), and 
attempted to make it.  Unfortunately, I found out that the AKCL build
depends distinctly on the specific machine architecture and operating
system being used, and the Macintosh was *not* included in the list.
I looked for some vanilla kind of BSD UNIX version, but none of the
choices I tried would proceed.

Well, I understood that AKCL was an older version, and that people now
were more using GCL.  So I took out GCL, and tried building it in a 
similar fashion.  However, I ran into the same problem, finding that
it was never configured to build on a Macintosh under MachTen.  I wrote
to the author of GCL, and he replied that he was interested, and might
have some thoughts on how to configure GCL, but that nothing had been
done so far.  I also called up the makers of MachTen, Tenon, and they 
shared that they were just talking about possibly working on a port of 
GCL to their UNIX.  So there are good prospects for sometime in the 
future.  But I am currently stuck without any working Common Lisp at all.

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.

After weeks of fruitless work, at this point I am really in need of help.  
Does anyone have any advice on how I might proceed, so I can continue with 
my research?  My shiny new hardware is for the moment not able to do the 
main thing I bought it for.

Here are some web pointers:
Digitool:         http://www.digitool.com/
GCL author:       wfs@fireant.ma.utexas.edu
Tenon:            http://www.tenon.com/
Other Mac Unixes: http://w3.one.net/~beef/Unix.html
SML:              http://www.cs.princeton.edu/~appel/smlnj/
HOL90:            ftp://research.att.com/dist/ml/hol90

Sliding down the bleeding edge of new technology, sincerely,

Peter
--------------------------------------------------------------------------
"In your majesty ride forth victoriously in behalf of truth, humility, and
 righteousness; let your right hand display awesome deeds."  -- Psalm 45:4
homeier@aero.org  __  _ http://www.cs.ucla.edu/csd-grads-gs2/homeier/html/
Peter V. Homeier <;_><_    These are my personal opinions: did you listen?