Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Message-Id: <9201031948.AA20811@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: dmartin@edu.ucla.cs, chou@edu.ucla.cs
Subject: HELP! Trouble in running HOL on NeXT using AKCL-1-599
Date: Fri, 03 Jan 92 11:48:49 PST
From: chou@edu.ucla.cs

I built HOL successfully on a NeXT but found that I couldn't run it
from anywhere other than my home directory.  Furthermore, if I do
run hol in my home directory, I can't do anything that involves
accessing files.  An example session:

========================================================================
[chou.10] cd
[chou.11] hol

          _  _    __    _      __    __
   |___   |__|   |  |   |     |__|  |__|
   |      |  |   |__|   |__   |__|  |__|

          Version 2.0, built on 3/1/92


HOL installed (`/usr/local/src/hol/hol`)
() : void


File hol-init loaded
() : void

#1.[2;3;4;5];;
[1; 2; 3; 4; 5] : int list

#let l = it;;
l = [1; 2; 3; 4; 5] : int list

#tl l;;
[2; 3; 4; 5] : int list

#print_theory `arithmetic`;;
The Theory arithmetic

Error: Can't expand pathname ~/arithmetic.th
Fast links are on: do (use-fast-links nil) for debugging
Error signalled by FUNCALL.
Backtrace:  > funcall > lambda > fun%5085%235 > funcall
evaluation failed     parents -- arithmetic theory missing

#new_theory `Peano`;;

Error: Can't expand pathname ~/Peano.th
Fast links are on: do (use-fast-links nil) for debugging
Error signalled by FUN%4287%487.
Backtrace:  > funcall > lambda > FUN%4287%487
evaluation failed     lisp error

#ADD;;
Definition ADD autoloaded from theory `arithmetic`.

Error: Can't expand pathname ~/arithmetic.th
Fast links are on: do (use-fast-links nil) for debugging
Error signalled by FUNCALL.
Backtrace:  > funcall > lambda > cons > fun%5085%254 > funcall
evaluation failed     definition


unbound or non-assignable variable ADD
1 error in typing
typecheck failed

#quit();;
Bye.
========================================================================

If I run hol from a directory other than my home directory (including
the hol directory itself!), I get:

========================================================================
[chou.15] hol

          _  _    __    _      __    __
   |___   |__|   |  |   |     |__|  |__|
   |      |  |   |__|   |__   |__|  |__|

          Version 2.0, built on 3/1/92

Error: Can't expand pathname ~/hol-init.ml
Fast links are on: do (use-fast-links nil) for debugging
Error signalled by TML.

Error: 4 is an illegal ihs index.
Fast links are on: do (use-fast-links nil) for debugging
Error signalled by SYSTEM:UNIVERSAL-ERROR-HANDLER.

Error: 0 is an illegal frs index.
Fast links are on: do (use-fast-links nil) for debugging
Error signalled by SYSTEM:UNIVERSAL-ERROR-HANDLER.

        ..... Many, many more copies of the last error message .....

Unrecoverable error: bind stack overflow.
IOT trap
========================================================================

Can some HOL expert out there help me?  I'd greatly appreciate any help.

My system configuration:
* NeXTstation running Release 2.1 on 68040.
* AKCL-1-599 modified by Noritake Yonezawa <yonezawa@cs.uiuc.edu> to run
  on a NeXT.  Its source distribution contains the following information:

        This AKCL port runs on NeXT OS 2.0 or later.

        Current version uses GCC-1.40 and modified GAS-1.38.1 instead of
        NeXT's (g)cc and (g)as to compile C-files generated by the AKCL
        compiler. It doesn't work well with NeXT's (g)as.

        The restrictions of this port are as follows:

        * The process size of running AKCL is fixed.
        * SYSTEM::FASLINK is not supported.

* HOL was built successfully using the above AKCL from scratch, i.e.,
  "make clobber ; make hol".
* I do have a hol-init.ml in my home directory, which constains the
  single line:
        install `/usr/local/src/hol/hol` ;;
* /usr/local/src/hol is the hol directory, which contains the hol
  executable hol.

- Ching Tsun <chou@cs.ucla.edu>

PS. A more general question: how do people run HOL on a NeXT?
    I'd appreciate any information.