Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Tue, 27 Sep 94 09:28:00 CST
From: jug@itd.dsto.gov.au (Jim Grundy)
Message-Id: <9409262358.AA19202@itd0.dsto.gov.au>
To: es774@eng.warwick.ac.uk
Subject: Re: hol-486-586
In-Reply-To: Mail from 'info-hol-request@lal.cs.byu.edu' dated: Mon, 26 Sep 94 15:20:23 BST
Cc: info-hol@lal.cs.byu.edu


I'd just like to add to this thread and encourage people to try HOL on PCs.
I run a PC (Similar configuration to Karim) with the Linux operating system
(a freeware Posix compliant Unix clone - which I am very happy with by the way).
It took some time to get it working, but this was completely due to difficulty
getting earlier version of AKCL running.  AKCL used to do some nasty little
nonportable hacks in its IO code.  The latest versions of AKCL (or is it
GNU Common Lisp now) don't.   

To get HOL running on a Linux PC now, all you have to do it ftp down the
latest AKCL and make it, then ftp down the latest HOL and make it - just
as easy as any other platform. No porting required.

HOL90 is a little harder, but only a tiny bit.  You ftp down Linux sml/nj 
binary (this is a nonsupported port), see the comp.lang.ml faq for where
to get it.  Then ftp down the latest HOL90 and make it using explicit 
path names rather than letting it figure out the current directory for itsself
(This is because the linux-sml pwd command is broken, but thats the only bit
that is). The HOL90 readme will explain what I mean about using explicit
pathnames when makeing it.  I have built HOL90.6 and the HOL90.7 pre-release
like this.

Be warned, most fast PCs  will run HOL88 quite well, but few peole 
(including me with 20M of RAM) have a PC with enough memory to run HOL90
effectively.

Jim