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:47:15 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA25143; Thu, 9 Sep 93 08:39:47 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from crl.dec.com by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA25139; Thu, 9 Sep 93 08:39:45 -0700 Received: by crl.dec.com; id AA07631; Thu, 9 Sep 93 11:39:51 -0400 Received: by easynet.crl.dec.com; id AA11105; Thu, 9 Sep 93 11:20:33 -0400 Message-Id: <9309091520.AA11105@easynet.crl.dec.com> Received: from ricks.enet; by crl.enet; Thu, 9 Sep 93 11:39:50 EDT Date: Thu, 9 Sep 93 11:39:50 EDT From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" To: info-hol@cs.uidaho.edu Apparently-To: info-hol@cs.uidaho.edu Subject: Re: HOL on DEC machines > 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 -?). Like Phil, I'm running HOL88 on a DECstation using Lucid Common Lisp. There are several kinds of machines from Digital, and you need to know which ones will be available (and several operating systems --- you need Ultrix). The main choices of architecture are: VAX (and VAXstation) --- should run HOL88 DECstation --- does run HOL88 (use Lucid Common Lisp) Alpha AXP --- I don't know of a working Lisp for Alpha yet I expect hol90 to run on VAXes and DECstations, but I don't know from experience, since I won't be using it for several months yet.