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, 25 Feb 1994 10:41:09 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14013; Fri, 25 Feb 1994 03:25:53 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.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 AA14009; Fri, 25 Feb 1994 03:25:41 -0700 Received: from elysium.cs.ucdavis.edu by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA22855; Fri, 25 Feb 1994 02:25:48 -0800 Received: from localhost.cs.ucdavis.edu by elysium.cs.ucdavis.edu (5.65/UCD.CS.2.4) id AA13488; Fri, 25 Feb 1994 02:25:09 -0800 Message-Id: <9402251025.AA13488@elysium.cs.ucdavis.edu> To: reetz Cc: info-hol@cs.uidaho.edu, schneide@ira.uka.de, eisen@fzi.de, dehof@ira.uka.de, kropf@ira.uka.de Subject: Re: HOL90.6 on a PC In-Reply-To: Your message of "Fri, 25 Feb 94 09:32:33 EST." <"i80fs2.ira.653:25.01.94.08.32.40"@ira.uka.de> Date: Fri, 25 Feb 94 02:25:09 -0800 From: benson@cs.ucdavis.edu X-Mts: smtp > day, I found my PC being lost in the software nirvana. After some > checking, it just seems to be the case that Linux does not use more > the 16MB Swapspace. I'm really not an expert on Linux, but this > limit sounds familiar for PC users. However, 20 MB memory are > clearly not enough to build HOL90. Even 32 MB (i.e. increasing > my main memory up to 16 MB, Linux will get lost into DMA-trouble > with my harddisk with more than 16 MB main memory) seems to be Linux does not have a 16 MB swap limit, nor does it have a 16 MB main memory limit. To have more than 16MB of swap you need to create more swap partitions up to 16 MB each. Use the swapon command to activate each swap partition. I am not certain what the swap space limit is, but it is much more that 16 MB. The 16 MB per partition limit may have changed in more recent versions of Linux. As far as main memory is concerned, you should not have a DMA problem. Linux uses a double buffering scheme to allow swapping above the 16 MB bus limit. I currently run Linux on a 486 with 20 MB of main memory and 16 MB of swap space. I use HOL88 2.01 built on AKCL and it works fine. I also use SML, but have not tried to build HOL 90. Greg