Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-21 20:31:41 -0700 (Thu, 21 Aug 2003)
Revision: 4866
Log message:

      This is a hacked commit, to temporarily fix the weak memo problem
      by using arrays instead of weak arrays.  This completely fixes the
      problem as far as I can tell, but of course it may greatly increase
      the amount of memory used by MetaPRL.
      
      Here is my suspicion.  There are two indexes into the weak memo,
      a weak_descriptor (and int), and a descriptor (the int and the value).
      Assumed invariant: a weak_descriptor is live iff the descriptor is live.
      The implementation guarantees that the weak_descriptor is live if the
      descriptor is.  We get into trouble the other way around.  If the
      descriptor goes dead, the value referred to by the weak_descriptor
      will change without notice.
      
      This seems to match the current problem.  I'll do some more investigating.
      

Changes	Path
+6 -5	metaprl/mllib/hash_with_gc.ml
+24 -5	metaprl/mllib/weak_memo.ml
+0 -2	metaprl/theories/itt/itt_int_base.mli