Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: shaw@cs.ucdavis.edu
Message-Id: <9408012311.AA21102@ice.cs.ucdavis.edu>
To: info-hol@cs.uidaho.edu
Subject: HOL90 library loading
Date: Mon, 01 Aug 94 16:11:31 -0700


Hi, I'm looking at HOL90 (90.6) for the first time. I've just
seen some surprising behaviour and want to know if this is
normal, or if some kind of reconfiguring of our system is 
indicated. 

My execution of 

load_library_in_place set_lib ;;

yeilded much more than I was expecting from my experience with
Classic HOL. I did this just after starting HOL, and entering
draft mode with new_theory.

-------------------------------------------------------------------
Loading the library "set".

Loading the library "num".

The library "HOL" is already loaded.

The parent libraries of library "num" have been loaded.
[opening /pkg/hol-build/hol90.6/library/num/src/num_lib.sig]
signature Num_lib_sig =
  sig
    val ADD_CONV : conv
    val num_EQ_CONV : conv
    val EXISTS_LEAST_CONV : conv
    val EXISTS_GREATEST_CONV : conv
  end
[opening /pkg/hol-build/hol90.6/library/num/src/num_lib.sml]
.../num/src/num_lib.sml:86.8-86.73 Warning: binding not exhaustive
          (c,n :: m :: nil) = ...

[Major collection... 68% used (5135864/7485576), 7040 msec]

[Increasing heap to 16230k]

[Major collection... 60% used (5206064/8571620), 6830 msec]

[Increasing heap to 16350k]

[Major collection... 75% used (6406896/8464104), 8630 msec]

[Increasing heap to 19198k]

[Major collection... 63% used (6283908/9856228), 8300 msec]
structure Num_lib : Num_lib_sig

The code of library "num" has been loaded.

The help path for library "num" has been adjusted.

The library "num" is loaded.

The parent libraries of library "set" have been loaded.

The theories belonging to library "set" are in the theory graph.
[opening /pkg/hol-build/hol90.6/library/set/src/gspec.sig]
signature Gspec_sig = sig val SET_SPEC_CONV : conv end
[opening /pkg/hol-build/hol90.6/library/set/src/gspec.sml]
.../set/src/gspec.sml:231.8-231.52 Warning: binding not exhaustive
          {Args=uty :: _ :: nil,...} = ...
.../set/src/gspec.sml:228.8-228.58 Warning: binding not exhaustive
          (_,v :: set :: nil) = ...
.../set/src/gspec.sml:38.11-38.52 Warning: binding not exhaustive
          {Args=ty1 :: ty2 :: nil,...} = ...

[Major collection... 55% used (5568736/10073532), 7250 msec]
structure Gspec : Gspec_sig
[opening /pkg/hol-build/hol90.6/library/set/src/set_ind.sig]
signature Set_ind_sig = sig val SET_INDUCT_TAC : tactic end
[opening /pkg/hol-build/hol90.6/library/set/src/set_ind.sml]
.../set/src/set_ind.sml:63.8-63.49 Warning: binding not exhaustive
          {Args=ty :: nil,...} = ...
structure Set_ind : Set_ind_sig
[opening /pkg/hol-build/hol90.6/library/set/src/fset_conv.sig]
signature Fset_conv_sig =
  sig
    val FINITE_CONV : conv
    val IN_CONV : conv -> conv
    val DELETE_CONV : conv -> conv
    val UNION_CONV : conv -> conv
    val INSERT_CONV : conv -> conv
    val IMAGE_CONV : conv -> conv -> conv
  end
[opening /pkg/hol-build/hol90.6/library/set/src/fset_conv.sml]
.../set/src/fset_conv.sml:368.8-368.51 Warning: binding not exhaustive
          {Args=_ :: ty :: nil,...} = ...
.../set/src/fset_conv.sml:367.8-367.59 Warning: binding not exhaustive
          (_,f :: s :: nil) = ...
.../set/src/fset_conv.sml:356.8-356.59 Warning: binding not exhaustive
          (_,x :: t :: nil) = ...
.../set/src/fset_conv.sml:322.8-322.51 Warning: binding not exhaustive
          (_,x :: s :: nil) = ...
.../set/src/fset_conv.sml:269.8-269.61 Warning: binding not exhaustive
          (_,S1 :: S2 :: nil) = ...
.../set/src/fset_conv.sml:247.8-247.48 Warning: binding not exhaustive
          (_,S :: T :: nil) = ...
.../set/src/fset_conv.sml:228.8-228.62 Warning: binding not exhaustive
          h :: t :: nil = ...
.../set/src/fset_conv.sml:193.8-193.60 Warning: binding not exhaustive
          (_,S :: x :: nil) = ...
.../set/src/fset_conv.sml:176.8-176.60 Warning: binding not exhaustive
          (_,y :: S' :: nil) = ...
.../set/src/fset_conv.sml:142.8-142.56 Warning: binding not exhaustive
          (_,x :: S :: nil) = ...
.../set/src/fset_conv.sml:106.8-106.60 Warning: binding not exhaustive
          (_,y :: S' :: nil) = ...
.../set/src/fset_conv.sml:64.8-64.57 Warning: binding not exhaustive
          {Args=ty :: nil,...} = ...
.../set/src/fset_conv.sml:50.8-50.59 Warning: binding not exhaustive
          (_,h :: t :: nil) = ...

[Major collection... 61% used (6034924/9874336), 8030 msec]

[Major collection... 61% used (6087424/9962588), 7850 msec]

[Major collection... 60% used (6082908/10043392), 8140 msec]

[Major collection... 71% used (7039844/9887232), 9200 msec]

[Increasing heap to 21070k]
structure Fset_conv : Fset_conv_sig

The code of library "set" has been loaded.

The help path for library "set" has been adjusted.

The library "set" is loaded.
val it = () : unit

---------------------------------------------------------------------------

Why all the warnings and GC's ?

Thanx!

Rob