Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 3 Aug 1994 02:13:01 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA01878;
          Tue, 2 Aug 1994 19:04:45 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA01871;
          Tue, 2 Aug 1994 19:04:28 -0600
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 4.1/3.25) 
          id AA28700; Tue, 2 Aug 94 18:01:08 PDT
Message-Id: <9408030101.AA28700@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Re: HOL90 library loading
Date: Tue, 02 Aug 94 18:01:05 PDT
From: chou@cs.ucla.edu


Konrad Slind wrote:

> This is true! The only palliative that I can suggest is for users to
> load commonly used libraries and then dump the image with "save_hol".

You may find the following code useful.  It allows you to change the header
printed by the saved image when it is invoked.

Cheers,
- Ching Tsun


(*----------------------------------------------------------------------------
  Save GZ.  [Most codes below were stolen from HOL90/src/0/save_hol.sml]
----------------------------------------------------------------------------*)

local
  val  image_str = "The name of the image" ;
  val banner_str = "The header printed by the image, built on " ;

  val init_fname = "/hol-init.sml" ;
  val local_init_fname = "."^init_fname ;

  fun parse_HOME [ ] =
        raise HOL_ERR {origin_structure = "save_GZ",
                       origin_function = "save_GZ.parse_HOME",
                       message = "can not find HOME variable in environment"}
    | parse_HOME (s::rst) =
        case (explode s)
          of ("H"::"O"::"M"::"E"::"="::path) => implode path
           | _ => parse_HOME rst ;

  local val (I,O) = execute ("/bin/date",[ ]) ;
        val date = input_line I ;
        val _ = close_in I ;
        val _ = close_out O ;
  in
    fun print_banner () =
      output (std_out,
      "\n\n*******************************************************************************\n"
      ^"        "^banner_str^date^
      "*******************************************************************************\n\n" )
  end ;

  fun save_hol (image) = 

  ( exportML (image) ;
    print_banner () ;
    if not (!Globals.use_init_file)
    then ()
    else if (Lib.file_exists_for_reading local_init_fname)
         then use local_init_fname
         else let val home_init_fname = parse_HOME (System.environ ())
                                        ^init_fname
              in if (Lib.file_exists_for_reading home_init_fname)
                 then use home_init_fname
                 else ()
              end ) ;
in
  val _ = save_hol (image_str) ;
end ;