Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 19 Nov 1993 23:00:21 +0000 Received: by leopard.cs.byu.edu (1.37.109.7/16.2) id AA11503; Fri, 19 Nov 93 15:00:28 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from panther.cs.byu.edu by leopard.cs.byu.edu with SMTP (1.37.109.7/16.2) id AA11498; Fri, 19 Nov 93 15:00:26 -0700 Received: from localhost by panther.cs.byu.edu with SMTP (1.37.109.7/16.2) id AA18066; Fri, 19 Nov 93 12:19:53 -0700 To: info-hol@leopard.cs.byu.edu, kcl@cli.com Subject: Re: AKCL space problems In-Reply-To: Your message of Thu, 18 Nov 1993 15:14:18 -0500. <9311182014.AA18366@amber.ccs.neu.edu> Date: Fri, 19 Nov 1993 12:19:52 -0700 From: Phil Windley Message-ID: <"swan.cl.cam.:112460:931119230104"@cl.cam.ac.uk> I posted several days ago about space problems running HOL compiled in AKCL. Many people sent suggestions---thanks to everyone who replied. Bill Schelter and Gene Cooperman win the prize for making the suggestion that worked. My problem, it turns out, is that AKCL had been compiled with the default MAXSIZE. The file h/hp800.h has the MAXSIZE definition commented out. After uncommenting it, making it big (64K), and recompiling AKCL and HOL, I was able to complete my proof. Thanks again. --phil-- Phillip J. Windley, Asst. Professor | windley@cs.byu.edu Laboratory for Applied Logic | Dept. of Computer Science, TMCB 3370 | Brigham Young University | Phone: 801.378.3722 Provo UT 84602-6576 | Fax: 801.378.7775