Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 9 Sep 1993 16:07:52 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA25079; Thu, 9 Sep 93 07:58:16 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from laforge.cs.byu.edu by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA25071; Thu, 9 Sep 93 07:58:13 -0700 Received: by laforge (5.65/DEC-Ultrix/4.3) id AA01455; Thu, 9 Sep 1993 08:57:29 -0600 Message-Id: <9309091457.AA01455@laforge> To: Karlis Cerans Cc: info-hol@cs.uidaho.edu Subject: Re: HOL on DEC machines In-Reply-To: Your message of Thu, 09 Sep 93 16:50:56 +0200. <9309091450.AA22394@animal.cs.chalmers.se> Date: Thu, 09 Sep 93 08:57:29 -0600 From: Phil Windley X-Mts: smtp On Thu, 09 Sep 93 16:50:56 +0200, karlis@cs.chalmers.se wrote: +------------ | is anybody using any kind of HOL system on a DEC machine? What are the | principal difficulties in installing HOL on DEC (lack of a suitable ML | compiler, all compilers being very expensive -?). I'm sure Tim Leaonard is ;-). I am as well. I found that building HOL88 on DECStations worked best with Lucid Common Lisp. We did (with JVT's help) get AKCL to run, but there were still times when it crahsed unexplainably (this was several years ago, so all may work now). HOL88 compiled with Lucid CL on a DECStation makes a wonderful platform for running HOL. Highly recommended. --phil-- Phillip J. Windley, Asst. Professor | windley@cs.byu.edu Laboratory for Applied Logic | Dept. of Computer Science, TMCB 3370 | Brigham Young University | Phone: 801.378.3722 Provo UT 84602-6576 | Fax: 801.378.7775