David,
I have a problem building ProofPower with the latest Poly/ML. The build goes into a loop at a point where it opens a certain structure. This will be the first time Poly/ML has had to pretty-print a value of the type THM that represents theorems. This type has a circularity passing through a ref and a certain dictionary data type. I have attached a very cutdown version of the failing code. The cutdown version behaves slightly differently in that I see some never-ending output, while the ProofPower build just goes into a silent busy hang.
The dictionary type OE_DICT that causes the problem is an amalgam of two simpler dictionary data types S_DICT (simple dictionaries using an association list) and E_DICT (efficient dictionaries using a hash key and a binary tree). Somewhat oddly the problem doesn't happen if I replace OE_DICT with either S_DICT or E_DICT even though the representation type for OE_DICT is just S_DICT * E_DICT.
If it is just that the latest source in SVN is just not in a stable state, let me know and I will give up until further notice.
I also noted in passing that types declared as abstypes are now equality types. Was this a conscious attempt to implement one of the Successor ML proposals?
Regards,
Rob.