Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: sas@dk.aau.daimi
Message-Id: <9201051458.AA02078@deimos.daimi.aau.dk>
Subject: Re: HELP! Trouble in running HOL on NeXT using AKCL-1-599
To: chou@edu.ucla.cs
Date: Sun, 5 Jan 92 15:58:31 MET
Cc: info-hol@edu.uidaho.cs.ted, dmartin@edu.ucla.cs
In-Reply-To: <9201031948.AA20811@maui.cs.ucla.edu>; from "chou@cs.ucla.edu" at Jan 3, 92 11:48 am

Ching can probably solve his problem in an easier way that changing to
another version of AKCL (if this is not available). I think the problem
arises because the search path is defined to include `~/`. This is done
in the Makefile by the line

          'set_search_path[``; `~/`; `${Theory}/`];;'\

Simply deleting the second element of the list will solve the problem
(who uses the search in their home directory anyway?). If loading the
file `hol-init.ml' is really necessary, it can probably be done manually,
or the file can be placed in the directory which is the current one
when HOL is activated.

Regards,

Sten Agerholm (sas@daimi.aau.dk)
Aarhus University