Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Sat, 12 Dec 1992 13:44:48 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04297;
          Sat, 12 Dec 92 05:36:15 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA04292;
          Sat, 12 Dec 92 05:36:05 -0800
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by nene.cl.cam.ac.uk 
          with SMTP (PP-6.3) to cl; Sat, 12 Dec 1992 13:35:20 +0000
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: hol-lcf and basic-hol
In-Reply-To: Your message of Sat, 12 Dec 92 01:19:11 -0800. <9212120919.AA09323@maui.cs.ucla.edu>
Date: Sat, 12 Dec 92 13:35:13 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"nene.cl.ca.257:12.12.92.13.35.21"@cl.cam.ac.uk>


Ching Tsun (chou@edu.ucla.cs) writes:
> In the new HOL 2.01, after "make hol" is done, are hol-lcf and
> basic-hol still needed?  I seem to recall that in version 2.00
> "make hol" automatically zeros hol-lcf and basic-hol after
> it's done.  Version 2.01 doesn't do that.

You can delete hol-lcf and basic-hol after hol has been built.

As pointed out, previous versions of the Makefile zeroed these 
files to save space.  This, however, tended to mess up the 
dependencies---e.g. when a rebuild bombed, you would often have 
to start from scratch again. Since people tend to have more
disk space in the past, it was thought better to have the right
dependencies...

Tom