Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 5 Oct 1993 09:17:44 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA20835;
          Mon, 4 Oct 93 19:27:36 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from panther.cs.uidaho.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA20831; Mon, 4 Oct 93 19:27:35 -0700
Received: by panther.cs.uidaho.edu id AA06988 (5.65c/IDA-1.4.4 
          for info-hol@cs.uidaho.edu); Mon, 4 Oct 1993 19:26:34 -0700
Date: Mon, 4 Oct 1993 19:26:34 -0700
From: Chris Toshok <toshok@cs.uidaho.edu>
Message-Id: <199310050226.AA06988@panther.cs.uidaho.edu>
To: info-hol@cs.uidaho.edu
Subject: Problem with load_library


Hello again,

  I am having a problem with load_library in hol90.6.  I type the
following:

  load_library {lib = Sys_lib.string_lib, theory = "string"};

and hol90 spits back at me "uncaught exception HOL_ERR".  The message field
in the exception contains the string:

 File.get_file_by_name: unable to get the file 
    "/.net1/dworshak1/snake/sysop/toshok/Lib/hol90.6/library/string/theories/ascii/string.holsig"

  The file actually exists, and this is the path to it.  I have actuall
specified the path to this file in the Globals.theory_path variable. The
directory where the file is is NFS mounted (if that really matters).  I
thought that perhaps the library needed rebuilding, so I make_lib'ed, but
the problem remains.

  Help.

Chris Toshok
Laboratory for Applied Logic
University of Idaho
Moscow, Id
toshok@cs.uidaho.edu
