gfink@bonzai.eecs.ucdavis.edu (George Fink) (05/28/91)
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 | gfink@iris.eecs.ucdavis.edu University of California, Davis | ucbvax!ucdavis!iris!gfink