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 14:14:15 CST
From: jug@itd.dsto.gov.au (Jim Grundy)
Message-Id: <9409270444.AA23647@itd0.dsto.gov.au>
To: wwong@pistis.comp01.hkbc.hk
Subject: Re: hol-486-586
In-Reply-To: Mail from 'info-hol-request@lal.cs.byu.edu' dated: Tue, 27 Sep 1994 09:22:14 +0800
Cc: info-hol@lal.cs.byu.edu

Hi All

Wai Wong write:

> 2) Did you port AKCL? Which C compiler did you used? If you
> use Linux which include a version of gcc, the GNU C compiler, I think
> it would be less difficult to port GCL, the GNU Common LISP.

This question was directed to Karim, but here is my 2c worth
(2c Australian cents is about 1.5 US cents or 0.9 pence at the current rates).

I use Linux with the gcc C compiler.  Earlier versions of AKCL
(1.615 if I remember, but I probably don't) needed porting because they did
nasting hacking with file structures (they assumed they knew the internal
structure of a C file pointer, which is supposed to be an opaque type).
There was a port by some Italian guy whose name escapes me at the moment for an
old version of the gnu libc library.  With later linuxes came a later libc and
this port stopped working.  In my quest to get HOL working I foind a few people
running this port on old Linux installations.  For some time I could find no
working port to recent Linux releases.

Then a later version of AKCL came out which cleaned up its act with respect
to file pointers. The current version builds just fine with recent Linux
distributions.

As far as AKCL vs GNU-CL goes, I was under the impression that the guys at
GNU had just persuaded the people at Kyoto to let go of their licence and 
place their code under a GNU public licence.  They then merged the
KCL source with the AKCL patches and released it as GNU-CL, so you should find
no real difference between the two. The two are really one.
At least that is the impression I got from reading the READMEs at the Austin
ftp site.

Hope this helps.

> 3) Have you check out SML/NJ to see whether it can be built on
> Linux? If the answer is yes, HOL90 may be ported to that platform.

As I said before, there is an SML/NJ port to linux, but it is not currently
supported by the folks at AT&T (pity). (There are supported ports to the 
freeware BSD variants for PCs though). The linux port seems to be fine except
the pwd function doesn't work.   Using this port it is straight forward to
build HOL90.  Check out the comp.lang.ml faq for how to get the port.
I used HOL90 under Linux to develop the latest vertion of the window library
which should come out with HOL90.7.

There are also CAML and Moscow ML ports for Linux, it would be nice to see
a re-implementation of HOL90 in one of these light-weight MLs.

Hope this helps.

Jim