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; Wed, 30 Mar 1994 16:58:37 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26126; Wed, 30 Mar 1994 08:43:52 -0700 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 AA26122; Wed, 30 Mar 1994 08:43:51 -0700 Received: from oberon.inmos.co.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA17252; Wed, 30 Mar 1994 07:43:01 -0800 Received: from frogland.inmos.co.uk by oberon.inmos.co.uk; Wed, 30 Mar 1994 16:42:54 +0100 From: David Shepherd Message-Id: <2053.9403301541@frogland.inmos.co.uk> Subject: Re: Compiling numeral Library in 2.02 To: info-hol@cs.uidaho.edu (info-hol mailing list) Date: Wed, 30 Mar 1994 16:41:33 +0100 (BST) In-Reply-To: <9403301443.AA06298@easynet.crl.dec.com> from "Tim Leonard, DTN 225-5809, HLO2-3/C11 30-Mar-1994 0925" at Mar 30, 94 09:44:00 am X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 2004 Tim Leonard, DTN 225-5809, HLO2-3/C11 30-Mar-1994 0925 has said: > Jim Grundy's compiler breaks on the numeral library with the message: > > > Calling Lisp compiler > > "numeral_rules_ml.c", line 48172: compiler error: out of hash tables > > The numeral library creates theorem tables to speed up numeral arithmetic. > By default, the library creates tables for decimal and hexadecimal arithmetic. > The tables are of size (radix EXP 3), so the default builds tables holding > several thousand theorems. You can change the list of "fast" radices by > changing this line at the beginning of numeral_rules.ml: > > letref radices = [10;16];; > > If all you're doing is decimal, then remove the 16. If you want, you can > remove both --- the library lets you perform arithmetic on radices that aren't > in the list, though such arithmetic is much slower --- but because I don't > remember ever testing the library with an empty list of supported radices, > use [2] as a minimal list. Can't recall what machine you were doing this on but .... from the dim and distant past I can remember having problems with AKCL compilation of HOL because some files (esp drules) produce a large amount of totally "unstructured" C as they have arrived in C from ML via Lisp! The result was that the then SunOS assembler tried to perform optimisations over this code - but because it had no structure I think it was trying to optimise the whole code as a single flat entity. This manifested itself in the assembly stage of the compilation taking over 24hrs to complete! You may be running into the same problem here again ... try to see if turning any optimisation in the C compilation stage of the run makes any difference. -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "I am not a nut --- I am a human being."