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, 2 Aug 1994 10:05:05 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA11676; Tue, 2 Aug 1994 02:53:22 -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 AA11672; Tue, 2 Aug 1994 02:53:19 -0600 Received: from swan.cl.cam.ac.uk (swan.cl.cam.ac.uk [128.232.0.56]) by dworshak.cs.uidaho.edu (8.6.9/1.0) with ESMTP id BAA21095 for ; Tue, 2 Aug 1994 01:50:10 -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, 2 Aug 1994 09:49:40 +0100 To: shaw@cs.ucdavis.edu Cc: info-hol@cs.uidaho.edu Subject: Re: HOL90 library loading In-Reply-To: Your message of "Mon, 01 Aug 94 16:11:31 PDT." <9408012311.AA21102@ice.cs.ucdavis.edu> Date: Tue, 02 Aug 94 09:49:34 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:159900:940802084948"@cl.cam.ac.uk> Rob Shaw (shaw@cs.ucdavis.edu) writes: > Hi, I'm looking at HOL90 (90.6) for the first time. I've just > seen some surprising behaviour and want to know if this is > normal, or if some kind of reconfiguring of our system is > indicated. > ... > Why all the warnings and GC's ? HOL88 (Classic HOL) does its garbage collection silently, though it can often be detected by the execution taking longer than expected or stalls in the flow of output during loading. Setting `timer true;;' will show how much GC is taking place. There is probably more GC taking place during loading of the library in hol90 for two reasons. First, SML/NJ likes to use memory. Second, the code being loaded has not been compiled in hol90 whereas it usually is in HOL88. Thus hol90 is compiling during loading. When pattern matching is not exhaustive in SML an exception (`Match' I think) is raised if the value being matched is not covered. The SML/NJ compiler warns that this may happen. Such non-exhaustive patterns are also possible in the ML used by HOL88, and may also give rise to an exception (failure), but HOL88 does not issue a warning. If you really don't like the GC messages, they can be hidden. They are sent to std_err rather than std_out, so redirect std_err, e.g.: $hol90 2>/dev/null This does not eliminate the warnings. (I have a vague recollection that when I've tried this redirection before it had some undesirable effect -- so proceed with caution.) Richard.