Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!cis.ohio-state.edu!ucbvax!ucdavis!gfink From: gfink@bonzai.eecs.ucdavis.edu (George Fink) Newsgroups: comp.lang.lisp Subject: AKCL on DecStation 5000 Message-ID: Date: 27 May 91 22:34:24 GMT Sender: usenet@ucdavis.ucdavis.edu Distribution: comp Organization: University of California at Davis Lines: 29 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