Via:  uk.ac.ucl.cs.nss; 7 Dec 88 2:20 GMT  (UK.AC.Cam.Cl.scaup)
Message-Id: <8812061934.AA02315@cheetah.ucdavis.edu>
Qotw: If a group of N people implements a COBOL compiler, it will have
      N-1 passes; someone in the group has to be the manager.
Pointers: (916) 752-7324/3168
To: info-hol@edu.ucdavis.clover
Subject: HOL in Common LISP
Date: Tue, 06 Dec 88 11:34:03 -0800
From: Phil Windley <windley@edu.ucdavis.cheetah>
Sender: windley <windley%edu.ucdavis.cheetah@edu.ucdavis.clover>
Status: RO

Hi All,

We at Davis feel a need for a Common LISP version of HOL.  We have a
lot of resources that run CL, but not Franz.  This situation is only going
to get worse since Franz, INC. isn't making any new ports of Franz.
Putting HOL in CL would allow the same collection of VAXs and Suns to run
HOL as well as new machines such as Sun 4's, IBM RT's IBM 3090's, etc.

We don't want to merely make a conversion and then be left out of the
mainstream if we can help it.  Thus, we would like to see the supported
version of HOL from Cambridge move in this direction.  Mike Gordon has
expressed some interest in this.

What version of CL should be used?  I would vote for Kyoto since it is
available for little cost and there is a supported version available (IBUKI
CL) for those who prefer supported software.

I thought I would open this up in the HOL community for discussion since it
would ultimately affect all of us.  I believe that HOL should be ported to
CL, what do you and your organization think?  Please send replies to me, I
will collect them and post them to the mailing list.

--phil--

Phil Windley                          |  windley@iris.ucdavis.edu
Division of Computer Science          |  ucbvax!ucdavis!iris!windley
College of Engineering                |  (916) 752-7324 (or 3168)
University of California, Davis       |  Davis, CA 95616