What semantics, if any, does PolyML.pointerEq have? In particular, is
it supposed to be guaranteed that if pointerEq (x,y) is true, then it
will remain true after GC?
My reason for asking is that I've been having trouble with assertion
failures in HOL when reducing large terms. The assertions check that
the left hand side of the conclusions of two theorem objects are equal
according to pointerEq, because this allows a fast comparison that
"should" always be true if the theorem is manipulated carefully.
I'm fairly certain the assertion failures are related to GC: they are
non-deterministic on code that ought to be deterministic, and vary in
frequency across different machines. (I haven't seen it at all on a 4GB
32-bit machine, rarely on 4GB 64-bit, often on the 8GB I normally use
and infrequently on a compute server with much more.) There's no sign
of any data corruption, however.
Brian
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
