Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-5.6)
          id <28183-0@swan.cl.cam.ac.uk>; Wed, 27 Nov 1991 15:50:04 +0000
Received: by ted.cs.uidaho.edu (15.11/1.34) id AA17484;
          Wed, 27 Nov 91 07:41:23 pst
Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from [128.232.0.56] by ted.cs.uidaho.edu (15.11/1.34) id AA17480;
          Wed, 27 Nov 91 07:41:11 pst
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk
          with SMTP (PP-5.6) to cl id <27943-0@swan.cl.cam.ac.uk>;
          Wed, 27 Nov 1991 15:41:32 +0000
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl
Subject: local and multi-segment libraries.
Date: Wed, 27 Nov 91 15:41:28 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.949:27.10.91.15.41.36"@cl.cam.ac.uk>

I have recently installed two new facilities for library loading in HOL.

The first is a search path mechanism, similar to the help search path,
that allows users to access local libraries using load_library.  In
particular, there are two new functions:

   * library_search_path : void -> string list
   * set_library_search_path : string list -> void

These are analgous to the similarly named functions for the help search
path.  The function load_library uses the library search path returned
by library_search_path and set by set_library_search_path to look for
library load files.

The second (rather experimental) facility allows loading of segments of
a library. Evaluating:

   load_library `lib:part`;;

loads the load file <path>/lib/part.ml instead of <path>/lib/lib.ml.  This
allows multiple load files in a single library.  The convention will be
that:

   load_library `lib`;;

will load an entire library, as at present (hence the change is compatable).
And evaluating:

   load_library `lib:part`;;

will load a selected segment of the library lib.  It will be up to library
authors to ensure that something sensible happens when parts of a library
are loaded.  Two multi-section libraries are currently under development
here, and these will be intended to serve as paradigms.

All this is installed in HOL version 2.01. This is not expected to be
released for some time yet, but if there is sufficient interest I could
prepare a patch kit for incorporating this change into version 2.0. Please
let me know it you're interested.

Tom