Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Fri, 23 Oct 1992 11:10:54 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23653; Fri, 23 Oct 92 02:57:46 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA23598; Fri, 23 Oct 92 02:57:29 -0700 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Fri, 23 Oct 92 10:56:24 BST From: David Shepherd Message-Id: <8050.9210230956@frogland.inmos.co.uk> Subject: Re: prim_rec loading error? To: gavan@za.ac.uct.mth.elc (Gavan Tredoux) Date: Fri, 23 Oct 1992 10:56:28 +0100 (BST) Cc: info-hol@edu.uidaho.cs.ted In-Reply-To: <9210230002.AA05419@elc.mth.uct.ac.za> from "Gavan Tredoux" at Oct 23, 92 02:02:31 am X-Mailer: ELM [version 2.4 PL3] Content-Type: text Content-Length: 1252 Gavan Tredoux has said: > As I understand it, prim_rec is built-in and so all > theorems should be autoloaded. However LESS_LEMMA2, > which print_theory reveals as part of prim_rec, > doesn't load, it has to be explicitly loaded. from the code in ml/load_thms.ml its clear that it is not getting set up for autoloading. i think that this could be allieviated if load_thms.ml used something like the include_theorems mechanism in Library/group/start_groups.ml which extracts all the theorem names and marks them all for autoloading. a problem with include_theorems etc is that to mark the theorems for autoloading involves loading in the entire theory to discover the names which sort of nullifies the reason behind it! this is a problem with the current theory file format, as noticed by soemone else recently, that theories are always "all or nothing" ... i.e. as soon as you need one element of a theory you get the overhead of the entire file. -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk or des@inmos.com tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq 1992: celebrate the quincentenary of columbus getting lost