Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <9674.9310211528@frogland.inmos.co.uk>
Subject: Re: A New on-line HOL Documentation Service!!!!
To: windley@laforge.cs.byu.edu (Phil Windley), 
    info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Thu, 21 Oct 1993 16:28:13 +0100 (BST)
In-Reply-To: <9310012142.AA21595@laforge> from "Phil Windley" at Oct 1, 93 03:42:37 pm
Content-Type: text
Content-Length: 2604

Phil Windley has said:
> The Laboratory for Applied Logic at Brigham Young University is pleased to
> announce the opening of an on-line network hypertexted based documentation
> service for the HOL theorem proving system.  Using this service, you will
> be able to access HOL documentation in hypertext format.
> 
> To browse this documentation, you will first need to obtain the XMosaic
> tool.  This tool is freely distributed by NCSA.  To get the tool, use
> anonymous FTP to connect to ftp.ncsa.uiuc.edu.  In the directory
> /Mosaic/xmosaic-binaries you will find already compiled copies of the
> latest version of XMosaic for a variety of architectures.  The source code
> is available in /Mosaic/xmosaic-source.
> 
> While, you're there, download the papers in /Mosaic/mosaic-papers and read
> them.  They will provide you with additional information about XMosaic.
> 
> The on-line documentation service is available at URL
> 
>     http://lal.cs.byu.edu/lal/hol-documentation.html.
> 
> Select OPEN from the XMosaic menu and enter this line.  You will then be
> connected to the HOL documentation server.
> 
> In the near future we will be distributing the code necessary for you to
> run this server locally if the network access is too slow.  Please stay
> tuned for further details.

I eventually got round to getting the sources to xmosaic and finding out
how to connect to a mosaic server via our gateway machine and have just
started playing with this.

I strongly recommend anyone who has the necessary connections/permissions
to have a look at this. It's quite something to find that searching for 
a theorem by firing of request to Utah is quicker than flicking through
the manual on the desk beside me.

Suggestions for future enhancements:

1) What would be really useful would be a mechanism to read the print_theory
   output for each theory/library - even better if it was done with a search
   ability as in the current HOL Theorem Entries page

2) Some more involved hyperlinking of theories ... e.g. link to
   page of theorems about "<" - possibly with sublinks of theorems
   about "<" and "+" etc etc.

The disadvantage is that apart from the HOL documentation, Mosaic seems
to have all the hallmarks of being something that could distract you
from work for a long time :-)

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                Latest football score: Real Madrid:1, Surreal Madrid:lemon