Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Sat, 9 Jan 1993 20:39:26 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14839; Sat, 9 Jan 93 11:59:36 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA14834; Sat, 9 Jan 93 11:59:29 -0800 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA08981; Sat, 9 Jan 93 11:58:59 -0800 Message-Id: <9301091958.AA08981@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list) Subject: Thrashing Date: Sat, 09 Jan 93 11:58:54 PST From: chou@edu.ucla.cs Sometimes during a long proof my HOL session begins to thrash. (I know because my hard disk is noisy and I can hear lots of disk activity.) What can I do in this situation? Of course, adding more physical memory helps, but only if I have the extra $$$ on hand. I do not want to quit the HOL session and re-start because I need to load in quite a few libraries and theories, which takes a long time. Does garbage collection help? If so, can I force HOL to do an extensive garbage collection? How about re-adjusting the memory resources AKCL allocates to various types of data? How do I know which type of data needs more space than others? Does the total of size of the HOL process affect the thrashing behavior? I don't think I want to reduce the process size, since I once ran out of space when the process size was half of the current size. My HOL was built using AKCL-1-615 on a NeXT. The process size is fixed in this AKCL. Many thanks in advance! - Ching Tsun