Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Mon, 14 Dec 1992 16:37:02 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07321;
          Mon, 14 Dec 92 06:21:03 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA07316;
          Mon, 14 Dec 92 06:20:53 -0800
Received: from coot.cl.cam.ac.uk (user pc) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2) to cl; Mon, 14 Dec 1992 14:19:50 +0000
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list), 
    Paul.Curzon@uk.ac.cam.cl
Subject: Re: Can't load library `more_lists` in draft mode
In-Reply-To: Your message of Sun, 13 Dec 92 18:15:56 -0800. <9212140215.AA09056@maui.cs.ucla.edu>
Date: Mon, 14 Dec 92 14:19:38 +0000
From: Paul Curzon <Paul.Curzon@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.308:14.11.92.14.19.54"@cl.cam.ac.uk>


> 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_parent.

Sorry for any inconvenience this causes,

Paul Curzon.