I'm trying to install HOL and BoyerMoore theorem provers on top of AKCL on
a DecStation 5000. I've modified the decstation 3100 port and akcl
seems to work ok, but my compilations on top of akcl are bombing for
similar reasons.
My questions are these:
1. Is there an official DecStation5000 port of AKCL yet? Or even of KCL?
2. Is there a way to specify a different compiler in AKCL? It's
using 'cc' right now, and that definitely bombs. I hand-translated
the cc call into a gcc call and it went through, but later akcl bombed
on a stack error when it loaded in the gcc-created object file.
HOL and BoyerMoore use 'compile-file.
3. Has anyone ported HOL or BoyerMoore to the Decstations yet?
4. Does anyone have more experience with large common-lisp programs
so I could correspond with them over email about my difficulties?
Thanks for any help y'all can give.
Please respond by email.
--George
--
George Fink | ·····@iris.eecs.ucdavis.edu
University of California, Davis | ucbvax!ucdavis!iris!gfink