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; Tue, 10 May 1994 11:27:12 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA07194; Tue, 10 May 1994 04:12:40 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA07190; Tue, 10 May 1994 04:12:33 -0600 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA08404; Tue, 10 May 1994 03:13:31 -0700 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 10 May 1994 10:07:48 +0100 To: Jockum von Wright IB Cc: info-hol@cs.uidaho.edu Subject: Re: Size increase from HOL2.01 to HOL2.02. WHY? In-Reply-To: Your message of "Mon, 09 May 94 20:38:36 +0300." <199405091738.UAA15411@ra.abo.fi> Date: Tue, 10 May 94 10:07:08 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:247610:940510090825"@cl.cam.ac.uk> I believe the size increase is due (mainly) to the loading of the file lisp/akcl.l prior to saving the executable. This file contains modifications to the sizes of AKCL resources which significantly improve the performance of HOL88 when built with AKCL. An alternative is to load this file from a hol-init file. The following line should be removed from the Makefile: 'lisp `(load "lisp/akcl.l")`;;'\ You should then find that the executable is back down to about 8 or 9 Mbytes, but will have to pay the price of the time to load the lisp file every time you execute HOL. I guess that this is only worthwhile if you are concerned about disk space, though the loading time may actually be reduced due to the smaller size of the executable. Please note that I haven't actually tried any of these suggestions. Richard.