hol90 Installation Guide

1. Get the hol90 sources
2. Get SML/NJ
3. Make hol90
4. Install the hol90 manual

    slind@informatik.tu-muenchen.de

User Manual Table of Contents

Get the hol90 sources

Once you have the hol90 source, it it can be unpacked by

    zcat hol90.7.tar.Z | tar xf -

• contrib - libraries contributed by users
• doc - system documentation
• examples - examples of using hol90
• help - the system online help files
• src - the hol90 sources
• library - the standard libraries
• theories - the system theories
• tools - some useful tools

Beginning of Installation Guide.
User Manual Table of Contents.

Get SML/NJ

Beginning of Installation Guide.
User Manual Table of Contents.

Make hol90

In the simplest case, making the system image for an architecture is done by invoking the unix command

    make_hol sml

There are extra options to make_hol that cover special circumstances, so if you find that the default option to make_hol doesn't give you the flexibility you need to build hol90 at your site, the following documentation gives more detail.

make_hol

    make_hol sml [-n | -b | -o] [-d path]

• Re-use the existing (ascii) theory files. These will be the theory files that were shipped with the release, unless the system has since been remade locally by invoking make_hol with the -n option.
• Set the hol90 root directory to be the parent directory of the current working directory (which is found by pwd). If make_hol isn't invoked in .../hol90/src or if one wants the hol90 root directory to be expandable in different ways on different machines in a networked computing environment, the -d option must be used.

-o

Reuse the existing ascii theory files.

-n

This option tells the system to rebuild all its theories. Be warned that a consequence of this option is that the system libraries will have to be rebuilt (with src/make_lib) and all user theories at the site will have to be rebuilt, along with any images that depend on hol90 libraries.

-b

The -b option tells the system to build binary theories. This is not advised, and some editing of the src/sys01.sml file is necessary to get this approach to work.

-d path

This option to make_hol is used to establish the root directory for hol90. If your current directory at the time of calling make_hol is not .../hol90/src, then you will need to supply the full directory path to the hol90 directory. This option is also useful in the case when building a version of the system that will be used in a networked environment, where the root directory may be expanded differently for different machines in the network. Note: there must be a space separating -d and path.

    make_hol sml -o -d `pwd`/..

Notes

• In the normal course of events, the system needn't be built with the -n option.
• The default and the -n and -o options entail that theory files will be in ascii. This is preferable, since ascii files are portable between architectures and are much smaller than binary theory files.

Libraries

    make_lib hol90

Contrib

    make_contrib hol90

• Some contrib libraries, hol_ML in particular, can take several hours to build, even on a large machine, so you might want to leave them out of an initial build sequence. In fact, all theories belonging to contrib libraries have already been made, so the only installation work that really needs to be done is to re-declare the contrib library of interest, and put the declaration in the right place. For example, the hol_ML library gets built with the following shell script:

      #!/bin/sh
      
      # Make script for holML library
      
      # Build the theories
      
      
      $* < theories/src/more_list/mk_more_list.sml
      $* < theories/src/more_string/mk_more_string.sml
      $* < theories/src/finmap/mk_finmap.sml
      $* < theories/src/Core/Common/mk_common_holML_core.sml
      $* < theories/src/Core/Plain_Core/mk_holML_Plain_Core.sml
      $* < theories/src/Core/Determinacy/mk_core_determinacy.sml
      $* < theories/src/Modules/Common/mk_common_ModML.sml
      $* < theories/src/Modules/ModML/mk_ModML.sml
      $* < theories/src/Modules/HOFML/mk_HOFML.sml
      
      # Install the library description file
      
      $* < theories/src/mk_holML_lib.sml
      mv holML.hol_lib ../desc
  

  Only the last two lines would need to be executed to install this library. i.e.,

      $* < theories/src/mk_holML_lib.sml
      mv holML.hol_lib ../desc
  

• If one moves the hol90 root directory after building the system, contrib libraries will be findable (via find_library) but not loadable. See Moving hol90 after it has been built for more information.

Install the hol90 manual

Beginning of Installation Guide.
User Manual Table of Contents.

Moving hol90 after it has been built

• You move only the executables, or link to them. Nothing needs to be done: executables can be moved with impunity.
• You move the hol90 directory. For instance, you might have built the system in your home directory, and now want to move the sources to /usr/local/lib and hol90.arch to /usr/local/bin. In such a case, you have to reset some internal paths in the hol90.arch images. Fortunately, this has been automated. In the following, let path be the full path to the directory you have moved the sources to. (For example, if you perform mv hol90 /usr/local/lib then path is /usr/local/lib/hol90.) On each architecture arch invoke the following

     tools/resituate_hol90 from-image  to-image  path
  

  where from-image is hol90.arch, to-image is the file name to put the saved image at, and path is the path to the hol90 root directory. For example, on a sun4 one could do, in directory hol90,

     tools/resituate_hol90 src/hol90.sparc src/hol90.sparc `pwd`
     

  Note that this particular invocation will overwrite the file of an executing process (namely src/hol90.sparc). Some operating systems may not allow this (how will you know? Don't worry - the OS will let you know!); in that case one needs to use a "temporary" to-image. Invoking something like

     tools/resituate_hol90 src/hol90.sparc src/hol90.tmp `pwd`
     mv src/hol90.tmp src/hol90.sparc
     

  ought to work. After the images have been resituated, one can make symbolic links in /usr/local/bin to the executables.

  contrib libraries will no longer load, although they are findable with find_library. Probably the simplest solution to this is to not execute make_contrib until the system is in its final resting place. Otherwise, one can

  • redo the make_contrib, or
  • perform a find_library then move_library everytime one wants a contrib library, or
  • edit the path field in each .hol_lib file in contrib/desc.

Finally, once this new version of hol90 has been installed, we repeat that all hol90 users must rebuild any of their theories that have been built on an earlier release of hol90.