Return-Path: Delivery-Date: Received: from bescot.cl.cam.ac.uk (user exim (mailer)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 12 Dec 1995 00:20:12 +0000 Received: from leopard.cs.byu.edu [128.187.2.182] by bescot.cl.cam.ac.uk with esmtp (Exim 0.24 #1) id E0tPIRX-0002vL-00; Tue, 12 Dec 1995 00:19:56 +0000 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA024885213; Mon, 11 Dec 1995 16:40:13 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from dialup.math.ncsu.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA024855210; Mon, 11 Dec 1995 16:40:10 -0700 Received: by dialup.math.ncsu.edu (8.6.11/UC06jan95) id SAA14539; Mon, 11 Dec 1995 18:23:31 -0500 Date: Mon, 11 Dec 1995 18:23:31 -0500 From: hishikaw@unity.ncsu.edu Message-Id: <199512112323.SAA14539@dialup.math.ncsu.edu> To: info-hol@leopard.cs.byu.edu Subject: Is anybody know how to install HOL via Lucid Lisp ? Hello. I am a new member of this HOL user community. From the first mail, it will be clear that I am not a "real" HOL user. I haven't installed HOL, yet. My problem is "Lucid Lisp" (I think). For building "hol-lcf" ecutable file, "ml/ml-curry.ml" file must be compiled. But, under my investigation, this first part haven't been done properly. I mean that all I got is "ml/ml-curry_ml.l" file instead of "ml/ml-curry_ml.o". Moreover, after excuting "compile(`ml/ml-curry`,true)", I have got a message that after calling Lisp compiler, evaluation failed. and I am out of "make hol". I have tried almost everything i knew. (Even I did compile ml/ml-curry.) It has been almost 1 month since I tried to install HOL. After knowing LCF, I really want to use HOL to know its power. Please, help me. Thank you for your time.