Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 23 Sep 1993 18:25:45 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA25947; Thu, 23 Sep 93 10:04:24 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA25940; Thu, 23 Sep 93 10:04:10 -0700 Received: from coot.cl.cam.ac.uk (user pc (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 23 Sep 1993 18:04:05 +0100 To: shaw@cs.ucdavis.edu Cc: info-hol@cs.uidaho.edu, benson@cs.ucdavis.edu, Paul.Curzon@cl.cam.ac.uk Subject: Re: loading more_lists fails. In-Reply-To: Your message of "Thu, 23 Sep 93 08:59:00 PDT." <9309231559.AA21173@mahogany.cs.ucdavis.edu> Date: Thu, 23 Sep 93 18:04:00 +0100 From: Paul Curzon Message-Id: <"swan.cl.cam.:057330:930923170410"@cl.cam.ac.uk> This is a known problem. I enclose the message sent previously to info-hol on the fix. I appologise for any inconvenience caused. Paul Curzon. -------------- > Something's wrong with library `more_lists`: it can't be loaded in > draft mode, as the following sessions show: Sorry about this bug. The problem is in the file more_lists.ml which contains the lines: >> if (draft_mode() or (current_theory() = `more_lists`)) then >> let path st = library_pathname() ^ `/more_lists/` ^ st in >> (load_auxiliary(); >> load(path `list_imec_tactics`, get_flag_value `print_lib`));; The call to load_auxiliary is needed when not in draft mode, as otherwise some of the tactics defined in the library will not work. When in draft mode the function load_auxiliary isn't defined (as it isn't needed). This bug can be fixed by changing the above to: if (draft_mode() or (current_theory() = `more_lists`)) then let path st = library_pathname() ^ `/more_lists/` ^ st in (if not (draft_mode()) then loadf `call_load_auxiliary`; load(path `list_imec_tactics`, get_flag_value `print_lib`));; and creating a file call_load_auxiliary.ml in the directory Library/more_lists which contains the call to load_auxiliary: load_auxiliary();; The call to load_auxiliary needs to be in a different file as otherwise it will not parse in the case when it has not been defined. The problem can also be avoided by loading the library before calling new_theory.