AKCL error

[bancroft@iris.ucdavis.edu (Steven Bancroft)]

Hello all,
   I am receiving a lisp error when I attempt to build the HOL
theorem-proving package using AKCL 1.465 on a Sun-3 (OS4). Now, if you
are not familiar with HOL, you still might be able to help because our
problem may not be directly HOL-related. Anyway, here's an excerpt
from the build where the problem occurs:

-----------------------
echo '(load "lisp/mk-ml")'\
     '(load "lisp/mk-hol-lcf")'\
     '(setq %system-name "HOL-LCF")'\
     '(setq %liszt "/home/hol/akcl/bin/kcl")'\
     '(setq %version "1.11a (Sun OS4)")'\
     '(set-make)'\
     '(tml)'\
     'compile(`ml/ml-curry`,true);;'\
     'quit();;'\
     | /home/hol/akcl/bin/kcl
AKCL (Austin Kyoto Common Lisp)  Version(1.465) Fri Mar  2 16:31:06 PST 1990
Contains Enhancements by W. Schelter

>Loading lisp/mk-ml.o
Loading lisp/f-cl.o

[.. stuff deleted ..]
[.. starts to compile the ml code ..]

compiling_stack = [] : bool list

load = - : ((string # bool) -> void)

compile = - : ((string # bool) -> void)

Error: The function COMPILER::QFEOF is undefined.
Error signalled by FUNCALL.
Backtrace:  > eval > tml > funcall > funcall > lambda > ml-compile > funcall
parse failed     lisp error
evaluation failed     compile -- ml/ml-curry
Bye.
*** Error code 1
make: Fatal error: Command failed for target `ml/ml-curry_ml.o'
------------------------

I have a feeling that this is an AKCL-related error, and not an
HOL-related error.  Note that we also get this same error when trying
to build HOL on a VAX 8600 (with AKCL 1.236) as well.

** BUT! ** : The interesting this is that we ARE ABLE build the HOL
package correctly (no lisp errors) on a SPARC station (with AKCL
1.243) using the same HOL source code: The 'undefined QFEOF' error
does not occur on a SPARC station for us.

As for the error, I looked at the AKCL source and found that 'qfeof'
is used in cmpnew/cmpfun.lsp and cmpnew/cmpopt.lsp. 'qfeof' isn't
mentioned in the HOL source at all, and it's not mentioned in any of
my Common Lisp reference manuals, either. 

The problem occurs when reaching the end-of-file of an ML source file
while doing an ml-compile.  The ML file is parsed completely (i.e.
reaches the end-of-file), and we believe that it is converted
completely into equivalent lisp code, too.

Has anyone else encountered this problem?  I find it very strange that
we can build HOL on one machine without this error while it bombs on
other machines using the same HOL source, and equivalent AKCL lisps.

Any help would be greatly appreciated.
                  ^^^^^^^
Thanks,

Steven Bancroft -- (bancroft@iris.ucdavis.edu)
University of California, Davis