Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Thu, 9 Jan 92 14:02:06 MST
From: slind@ca.ucalgary.cpsc (Konrad Slind)
Message-Id: <9201092102.AA27394@fsa.cpsc.ucalgary.ca>
To: info-hol@edu.uidaho.cs.ted
Subject: new hol90!


Another release of hol90 is now available. The principle additions are:

    A. Some libraries;
    B. Assignable path lists for help, theories, and libraries;
    C. Support for hol-init files;
    D. A help system; and
    E. An upgrade to SML/NJ 0.75

As well, there are some bug fixes.


A. Libraries.

The following libraries exist:

    set             -- T. Melham and P. Leveilley. Special syntax for
                       finite sets (e.g., {} and {1,2,3,4}) and set
                       specification, {t | P}, is supported in parser
                       and prettyprinter. This version is hardwired to
                       GSPEC.

    string          -- T. Melham and M. Gordon. HOL strings are delimited
                       by ".

    unwind          -- R. Boulton's improvements to the unwind package

    ind_def         -- T. Melham's inductive definitions package

    taut            -- R. Boulton's tautology checking routines.

    hol88           -- A collection of functions found in hol88, but not hol90.
                       Supposed to provide hol88 compatibility. This is
                       the old Compat structure.

    group           -- Elsa Gunter's first order group theory.

    integer         -- Elsa Gunter's theory of integers. Both this and the
                       "group" library are only partially done; Elsa is
                       currently working on them.

    num             -- An assortment of reasoning utilities for the type :num.
                       Signature:

                          sig
                            val ADD_CONV : conv
                            val num_EQ_CONV : conv
                            val EXISTS_LEAST_CONV : conv
                            val EXISTS_GREATEST_CONV : conv
                          end


The function "load_library" will operate as in hol88, except that any
code loaded will be source, not object, so loading will be slower. As
soon as I come to grips with SML/NJ's separate compilation facility this
will be fixed.

The function

    loaded_libraries : unit -> string list

will tell which libraries have already been loaded.

I am not going to port all the libraries; it would be nice if the
authors would give it a try and send me the translation.

A potential irritation for users: if a hol88 library had a plural name,
I made it singular, for regularity's sake. Hence "sets" is now "set" and
"ind_defs" is now "ind_def".


B. Paths.

The following assignable variables exist in the structure Globals:

    theory_path  : string list ref
    library_path : string list ref
    help_path    : string list ref

These are used to find theories, libraries, and help. The three path
lists are independent. theory_path and library_path begin with an empty
path (""), so that theories and libraries can be designated by absolute
pathnames. The path lists are used primarily to find files to read,
load, or print; however, the theory_path list is also used to determine
where to write a theory. In this case, the first member of the list is
concatenated to the theory name to give the pathname of the file to
write. No further attempts are made if the write fails.

There are some functions for manipulating paths:

    Lib.cons_path   : string -> string list ref -> unit
    Lib.append_path : string -> string list ref -> unit

In "cons_path", an attempt is made to keep the empty string first in the
path. This is so that one can get around masking effects, e.g., one
might be looking for a particular "z.th" on the theory_path, but a
"z.th" occurs "earlier" that hides the particular "z.th" being searched
for. This is helpful for developing local versions of system
theories help and libraries. Both "cons_path" and "append_path" treat the
path list as a set.


C. Hol-init files.

When hol90 is invoked, it looks for a hol-init.sml file, first in the
current directory, then in the user's home directory. A "use" is
performed on the first hol-init.sml found. This support is extended to
all binaries resulting from an invocation of "save_hol".

A new variable has been added to control the use of the hol-init file:

    Globals.use_init_file : bool ref

The value of the reference is true if we wish the system to attempt to
find and use a hol-init.sml file; otherwise it is false. Initially, it
is set to true.


D. Help.

I have ported over the hol88 help facility. An invocation of help, i.e.,

       Help.help "frees"

follows the help_path until it finds a file frees.doc. Then it makes a
system call to "sed" to process the file and print the results to
std_out. An assignable string interpreted as an operating system
function is used for printing: it is the variable

       Globals.output_help : string ref

which is initially set to "/bin/cat". If you find that "help" fails
because the system call to "sed" fails, you should try the auxiliary
help function "help1", which produces TeX-annotated, but still readable,
output.

Note: I am not including the help files in this release, since they are
      just the hol88 help files. If you don't already have the hol88
      help files, you can ftp them from Cambridge or Moscow.
      To get help to work, put something like the following in your
      hol-init file:

         let val hol88_help = "<path-to-HOL2>/HOL2/help/ENTRIES/"
         in
         Lib.append_path hol88_help Globals.help_path
         end;

It would be "a good thing" if hol90 had its own documentation of the
same quality as that for hol88, but that would be a separate project in
its own right. The proof support of hol90 (term manipulation, axioms,
inference rules, tactics, conversions, theories, libraries, etc.) is
intended to be an identical replacement for that of hol88, version 2. Up
to and including the libraries listed above, I think this is true, aside
from a few exceptions. The main differences in the two systems lie in the
"systems" aspect: how paths are administered, how autoloading works, the
nature of theory files, how quotation, antiquotation, and prettyprinting
work, etc. The only documentation for these differences is in the file
"hol90.doc" in the hol90 sources directory.

The upshot: if you want documentation on something, use "xholhelp" or the
"help" function, and the hol88 Manual; if that doesn't work, read the
file "hol90.doc"; and if that doesn't answer your question, send me
mail.


E. Modified SML/NJ.

Unfortunately, hol90 still requires a specially modified SML/NJ compiler
to build. I have ported these modifications to version 0.75 and it is
ftp-able from Calgary. I was expecting these special modifications to be
incorporated into the standard release of the New Jersey compiler, and
hence not to be special anymore, but that is not yet so.


Miscellaneous additions.

0. Control over autoloads.

The system has a new type abbreviation

   type autoload_info = {Theory : string,
                         Axioms : string list,
                         Definitions : string list,
                         Theorems : string list}

and a new function "set_autoloads" of type :autoload_info -> unit in
Add_to_sml. One establishes what bits of a theory S are to be autoloaded
by a call to "set_autoloads". Later, when the user invokes
add_theory_to_sml "S", the information given in the call to
"set_autoloads" is used to determine what theory bindings to install in
SML. If no "set_autoloads" was done for S, then all axioms, definitions,
and theorems in S are loaded.


1. Some additions to the signature of Rewrite:

       val mk_conv_net : thm list -> conv Net.net
       val REWRITES_CONV : conv Net.net -> conv
       val GEN_REWRITE_RULE : ((term -> thm) -> term -> thm) ->
                              conv Net.net ref -> thm list -> thm -> thm

   This should help those, like Jim Grundy, who want deeper access to the
   rewriting machinery.


2. The Hol_pp structure is now available to the public, because of a request
   by Sara Kalvala.

       signature Public_hol_pp_sig =
       sig
         structure Term : Public_term_sig
         val pp_type : Term.Type.hol_type -> unit
         val pp_term : Term.term -> unit
         val quoted_pp_term : Term.term -> unit
       end;


3. Addition of Globals.HOLdir : string ref, which is the full path to the
   home of hol90.


4. Added a value "arch" of type :string to Globals. This is the Unix name
   for the processor (e.g. sun4, mipsl) hol90 is running on.


5. Added function "file_exists_for_reading" to Lib. This has equivalent
   functionality to

      fun file_exists_for_reading s = (close_in(open_in s); true)
                                      handle Io _ => false;


6. Added "mk_pabs", "dest_pabs", and "is_pabs" to Term_ops. These are derived
   syntax functions for paired abstractions.


7. Added

       delete_theory_from_cache :string -> unit
       theories_in_cache :unit -> string list

   to Theory.


8. Added

       top_thm :unit -> thm    and
       save_top_thm : string -> thm

   to Goal_stack.


9. Added "GEN_BETA_CONV" and "PAIRED_ETA_CONV" to Let_conv.


10. More informative error messages are now issued for failure of
    type inference. Also, the parser function "--" now automatically reports
    parsing errors (hence the function "Goalstack.g" does, too).


11. There is now a pervasive structure Num_induct, holding INDUCT and
    INDUCT_TAC.


12. The structure Taut has been renamed Taut_thms, to avoid confusion with
    the library Taut.


13. For compatibility, new_prim_rec_definition and
    new_infix_prim_rec_definition have been added to the "hol88" library.


BUG FIXES.

1. Parsing of types has been fixed: the relative precedence of # and + was
   wrong, plus there were legal types that wouldn't parse, e.g.,

      :num + num


2. Prettyprinting of terms fixed:

       --`(@f:num -> 'a. T) 1`--

   parsed OK, but died when printing. This fixes a bug reported by
   Paul Loewenstein and Claudio Russo.


3. Fixed a goal_stack bug pointed out by Kevin Mitchell. In certain
   circumstances, it was possible for the validation function to "unwind"
   past the original goal. Now markers are put on the goal stack to prevent
   this.


4. Because of a clash between the SML exception "Size" and the HOL constant
   "Size" (found in theory "ltree") when autoloading, I have changed the HOL
   constant to be "size".


5. Fixed bug in let_CONV.


6. When a new_theory, load_theory, or extend_theory is done, the contents of
   the old theory have to be written out only if the old theory has been
   added to. This is now the case; therefore, spurious "HOL.th" files should
   no longer appear.


HOW TO GET IT.

hol90 is available for anonymous ftp from Calgary. It runs on vax, m68k,
sun4, and big- and little-endian mips architectures. To get the system,
one must ftp several files:

    1. 75/mo.<arch>.tar.Z, where <arch> is the architecture you want
       to run on (and are compiling on!). The architecture may be
       found by invoking bin/arch in the shell.
    2. 75/src.tar.Z
    3. hol90.tar.Z

Other files in this directory that are of interest: releaseNotes.ps.Z,
lib.tar.Z, doc.tar.Z, and tools.tar.Z.

An example session would be

    gh% ftp fsa.cpsc.ucalgary.ca
    Connected to fsa.cpsc.ucalgary.ca.
    220 fsa.cpsc.ucalgary.ca FTP server ready.
    Name (fsa.cpsc.ucalgary.ca:slind): anonymous
    331 Guest login ok, send ident as password.
    Password:
    230 Guest login ok, access restrictions apply.
    ftp> cd pub
    250 CWD command successful.
    ftp> binary
    200 Type set to I.
    ftp> get hol90.tar.Z
            .
            .
            .
    ftp> cd 75
    250 CWD command successful.
    ftp> get mo.<arch>.tar.Z
            .
            .
            .
    ftp> get src.tar.Z
            .
            .
            .
    ftp> quit
    gh%

Once you have unpacked these directories someplace, make an sml:

    cd src
    makeml

This will leave src/sml, an sml interactive system that is able to build
hol90. The shell script hol90/make_hol will make the system. It takes
about 45 minutes on a 48 Meg. SPARC2. In general, you want to build and
run hol90 on a machine with a lot of memory: the SPARC version of hol90
is about 7 Meg. on disk and constructs a large heap.

If you have problems getting or building hol90, please let me know.


FUTURE PLANS.

I don't plan to do much more porting of libraries, utilities, or the
like from hol88. In particular, I will not be trying to keep pace with
new additions to hol88, believing that such work is now best done in
hol90.

Of course, I will fix any bugs that I have perpetrated and answer any
questions about hol90. I am keen to hear any ideas or criticisms about
the system, so drop me a line!

Konrad.