Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: info-hol@edu.uidaho.cs.ted
Subject: library proposal
Message-Id: <93Jan7.174757met.8121@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 7 Jan 1993 17:47:46 +0100


The next generation of HOL libraries?

The following is a somewhat lengthy proposal for the HOL library system.
First there are some criticisms of the current library system, then I
propose a new scheme, which is implemented in hol90. I would be
grateful for any feedback by users and implementors of the library
system. This proposal owes a lot to work done by (and discussions with)
Elsa Gunter.


Some criticisms of the current library system.

All along, Tom Melham has maintained that the current library system is
not "the right thing, but it will do", and that it should eventually be
replaced with something better. The following are some of the major problems. 


1. No formal idea of what a library is.

This says it all, I'm afraid. Having a library be represented by an
arbitrary ML file on disk, its format a matter of informal convention,
is a hindrance to writing tools that deal with libraries.


2. Paths considered harmful.

  There are many examples of why paths are bad, but they all have to do
with masking. If you use paths, you immediately place yourself in a
setting where arbitrary occurrences that you may never know about can
seriously screw you up. File permissions on library files may change,
library disk locations can change at the whim of system administrators,
people may add new libraries into their personal library, etc. Any of
these can result in a different library being loaded than you expected.
I want the hol90 system to be able to reliably provide the expected
libraries regardless of how paths change.

  Under a path regime, the answer to the question, "What does
load_library "set" do?" is meaningless. I want to tell the user that
*the* system library "set" will become available for use, but I can't. I
can say only that some file named "set.sml" in some directory named
"set" will be loaded. If you want a particular library *for certain*
(and who would want an arbitrary library?) the user has to give the
absolute path (or make a symbolic link to it from the local directory),
thus obviating the path regime.

If you develop and use a local library with the same name as a standard
library, all you are going to do is confuse the rest of the user
community when it comes time to distribute it. Suppose I develop a
library of temporal logic (calling it "temp"), and there's already a
system library named "temp". When I want somebody to use it, not at my
site, I am going to have to change its name. I may as well name it
something like "my_temporal" and save on the confusion from the very
beginning.

  Here's another thing: suppose Susan puts "~George/hol_lib" onto her
library path. Then she loads a library "A". Suppose it is found in
~George/hol_lib. Suppose further that "A" uses a library "B". So
load_library is recursively called on B. Suppose both Susan and George
have libraries named "B". The system will attempt to load Susan's, which
is almost definitely wrong.

  This points up the difference between libraries and theories (at least
in hol90, which has unique theory identifiers). Loading a library may
involve loading parent libraries. The question then becomes "what
relationship does the library path at "load" time have with the library
path at "make" time?" Right now, it seems there isn't any. With
theories, unique theory_ids enforce consistency between the two times.
My implementation provides the same sort of idea by requiring that the
known library names be a set, and that the path to each library be given
explicitly.


A new interface for libraries.

In hol90, libraries are now represented in the system, in contrast to
hol88, in which a library is what one gets by executing a file of ML
code. This change makes libraries well-defined enough to be a reasonable
system structuring mechanism. In fact, the hol90 system "out-of-the-box"
is built by loading 3 libraries on top of the implementation of the
primitive basis of the logic.

Roughly, a hol90 library is represented by a name, a path, other
libraries the library depends on, any theories that the library loads,
code the library loads, and any modifications to the help path that the
library requires. This abstraction is a modification of one proposed by
Elsa. The representation is the following in the hol90 implementation:

    datatype lib_info = 
       Lib of {name : string,
               path : path,
               parents : lib_info list,
               theories : string list,
               code : string list,
               help : string list,
               loaded_func : unit -> unit}

The `name` is the name of the library. The `path` is the path to where
the library can be found. To make life easier for those producing system
libraries, I introduced a datatype of paths: 

    datatype path = Default | Absolute of string;

The "Default" constructor signifies that the library is to be found at

     (!Globals.HOLdir)^"library/"^name

and the "Absolute" constructor signifies that no such interpretation is
to be done, i.e., the library is to be found at its argument. The
`parents` of a library are the libraries that it needs loaded before it
can be used. These could have been represented by strings, but
representing them as lib_info objects allows easy computation of library
properties. The `theories` of a library are the new HOL theories that it
provides for one to use. The `code` of a library is the SML code that
becomes available for one to use. The `help` of a library represents the
paths to its documentation files (written so as to be usable by the
system function "help"). The `loaded_func` field of a library
representation is called at the end of the loading of the library, and
is intended to provide any functionality not catered to by the first part of
the loading process.


Declaring a library.

To load a library, first it must be known. To make a library known,
there is a function "declare_library" of type :

    {name : string,
     path : path,
     parents : lib_info list,
     theories : string list,
     code : string list,
     help : string list,
     loaded_func : unit -> unit} -> lib_info

This succeeds if the library is not already known, and the parents are
all known. When a library is declared, its theory paths get added to the
system theory path. This enables one to, for instance, load a theory
that has a parent theory in an unloaded library. For example, once one
has declared the string library, one can load the theory "string" in the
string library without loading the library. The declaring of libraries
involves little computation, and is something that is appropriate for a
hol-init file.


Loading a library.

Now to load a library. The type of load_library is somewhat different
than in hol88:

    val load_library: {name :string, theory :string} -> unit

The loading of a library is intended to provide a new environment (code,
theories, help) for a user to work in. The only difficulty in
implementing this is theories, for there is a sticky question of whether
we want to load the theories provided by the library, or make them new
parents. The distinction is technical, but it can easily be the case
that loading one theory will prevent another from loading, while having
one be a parent will not prevent another theory from being a parent
(unless one is attempting to introduce loops, but that is rare mistake).
In other words, it is more robust to do a "new_parent" than a
"load_theory". The problem then becomes the fact that new_parent must be
invoked in draft mode, i.e., the user must already be in an "unclosed"
theory. Suppose the current theory is not in draft mode. Then the
simplest thing to do is to make a call to "new_theory" with a suitable
name. The name we choose is the `theory` field of the call to
load_library. (If the library to be loaded has no theories, or the
system is already in draft_mode, then `theory` can be anything; I use
"-".) Then any theories that the library uses, and indeed uses as a
result of loading parent libraries, are made new parents.

  Example. If one just starts up hol90, one is in the "HOL" theory, which
  is not in draft mode. If we want to play around with the theory of strings,
  then we would do

    load_library{name = "string", theory = "foo"}

  This places us in a new theory "foo", with the theory "string" as a parent.

With that discussion out of the way, what happens? The first thing to do
is to load the parent libraries, in left-to-right order, if there are
any. Then we check if there are any theories provided by the library. If
there are, we are either in draft mode, or we put ourselves into draft
mode by the mechanism just discussed. Now the `theories` are made new
parents of the current theory (if they are not already), in
left-to-right order. The path field is used to find the theory to load.

Now we check to see if there is any ML code provided by the library. If
not, we continue, otherwise the path is used to find the code to load,
in left-to-right order.

Now we check to see if there are any modifications to be made in the
help path. If not, there should be! Otherwise, the path is used to make
a new path name to prepend to  Globals.help_path.

Now we execute the "loaded_func". The purpose of this function is to do
any final computation necessary to load the library. Common operations
include printing messages, opening structures, and setting flags.

If failure occurs along the way, we clean up so that the theories and
paths are as they were before the invocation of load_library.


Library disk format.

A library is a directory with subdirectories "src", "help", and
"theories" (which itself must have subdirectories "src" and "ascii"
(and/or "sun4", "mipsb", ...)).


The signature.

(* ===================================================================== *)
(* FILE          : load_library.sig                                      *)
(* DESCRIPTION   : Provides functionality for HOL libraries.             *)
(*                                                                       *)
(* AUTHOR        : Konrad Slind, University of Calgary                   *)
(* DATE          : December 9, 1991                                      *)
(*                                                                       *)
(* Modified      : December 25, 1992  (kls)                              *)
(*                 Changed to have a library be represented by a data    *)
(*                 structure in memory rather than as a file on disk.    *)
(* ===================================================================== *)

  signature Load_library_sig = 
  sig
  datatype path = Default | Absolute of string
  datatype lib_info = Lib of {name : string,
                              path : path,
                              parents : lib_info list,
                              theories : string list,
                              code : string list,
                              help : string list,
                              loaded_func : unit -> unit}

  val declare_library : {name:string, 
                         path : path,
                         parents :lib_info list,
                         theories : string list,
                         code : string list, 
                         help :string list,
                         loaded_func:unit -> unit} -> lib_info
  val declared_libraries : unit -> lib_info list
  val declared_library_names : unit -> string list

  val load_library :{name:string, theory:string} -> unit
  val loaded_libraries : unit -> string list
  end;


Conclusion.

This approach to libraries has been quite successful in hol90; much of
the system may be considered to be libraries. In fact, all development
of the system after installing the primitive logic is done by loading
libraries. This whole approach is motivated by considering what state
load_library should leave one in. The answer? The same sort of state
that hol90 has on startup: in an empty theory, with parents being the
theories provided by the library. Thus libraries are now a basic
structuring tool for the system.

There is some more work that can be done on this: the information
contained in a library description should probably be extended to
contain information on how to make it.


Konrad.