Received: from scaup.cl.cam.ac.uk by Steve.CL.Cam.AC.UK
          with SMTP/TCP/IP over Ethernet id a020300; 7 Dec 88 11:13 GMT
Via:  uk.ac.ucl.cs.nss; 7 Dec 88 11:11 GMT  (UK.AC.Cam.Cl.scaup)
Received: from clover.ucdavis.edu by NSS.Cs.Ucl.AC.UK   via Satnet with SMTP
           id aa03933; 7 Dec 88 10:55 GMT
Received: from hplb.hp.com by clover.ucdavis.edu (5.59/UCD.EECS.1.1)
        id AA28598; Wed, 7 Dec 88 02:53:50 PST
Message-Id: <8812071053.AA28598@clover.ucdavis.edu>
Received: from acamille.lb.hp.co.uk by hplb; Wed, 7 Dec 88 10:53:02 gmt
Received: by acamille; Wed, 7 Dec 88 10:52:47 gmt
From: ac <ac%acamille@csnet.hplb.hpl.hp.com>
Subject: HOL in Common Lisp
To: info-hol <info-hol@edu.ucdavis.clover>
Date: Wed, 7 Dec 88 10:52:43 GMT
X-Mailer: Elm [version 2.0 beta]
Sender: ac <ac%acamille%csnet.hplb.hpl.hp.com@edu.ucdavis.clover>
Status: RO


At Hewlett Packard we also require a Common Lisp implementation
of HOL in order to run it on HP machines. I agree that Kyoto
Common Lisp is probably the best bet for portability---if I'm not
mistaken it runs on SUNs, Vaxes, HP 9000s, etc, etc. Plus it is
free to academic institutions and all that. There is also a
version of Common Lisp called AKCL which is a version of Kyoto
Common Lisp developed at Univ. of texas at Austin. This is a more
optimised Common Lisp and it is supposed to be completely
straightforward to compile KCL code using the AKCL compiler.
Perhaps the best thing would be to produce a KCL implementation
of HOL, and institutions with other faster implementations of Common
Lisp can tweak their own HOL systems to run on these.

Vote:-  KCL

Albert Camilleri