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 18:17:27 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA25611; Wed, 30 Mar 1994 07:49:50 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from crl.dec.com by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA25607; Wed, 30 Mar 1994 07:49:48 -0700 Received: by crl.dec.com; id AA22943; Wed, 30 Mar 94 09:44:00 -0500 Received: by easynet.crl.dec.com; id AA06298; Wed, 30 Mar 94 09:43:59 -0500 Message-Id: <9403301443.AA06298@easynet.crl.dec.com> Received: from ricks.enet; by crl.enet; Wed, 30 Mar 94 09:44:00 EST Date: Wed, 30 Mar 94 09:44:00 EST From: "Tim Leonard, DTN 225-5809, HLO2-3/C11 30-Mar-1994 0925" To: info-hol@leopard.cs.byu.edu Apparently-To: info-hol@leopard.cs.byu.edu Subject: Re: Compiling numeral Library in 2.02 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. Tim