Hi Bow-Yaw, Thanks for reporting that and sending the fix. I'll incorporate it in the next release. Markus Wenzel reported a problem in the disc garbage collector when compiling with GCC 3.0.2 which sounds exactly like this. There hasn't been any discussion of this on the Poly/ML mailing list because, so far, there hasn't been ANY discussion on the mailing list.

As far as ml-lex and ml-yacc are concerned, I don't know whether they will work with Poly/ML or not. If they're written entirely in Standard ML they should work fine but if they use some special features of SML/NJ then there may be a problem. Does anyone else know?

Regards, David.

On Saturday, March 23, 2002, at 12:42 , Bow-Yaw Wang wrote:

Hi Mr. Matthews:

I try to build Isabelle2002 with PolyML 4.1.2. But poly always crashes at "Bad pointer" when closing the database. It turns out that gcc-3.0.4 has a warning and generates different code for improve.c. After I made the following change:

739c739

< while (n--) *pt++ = (word) FixupPointer((word *)*pt);

...

while (n--) { *pt = (word) FixupPointer((word *)*pt); pt++; }

the problem goes away. Since I'm not on the mailing list, I'm not sure if this is a known issue. Just let you know in case the problem hasn't been reported.

Currently, I'm working on a project which needs a theorem prover, external function interface and yacc. PolyML + Isabelle would be the ideal environment if tools like yacc were available. I'm thinking using ml-yacc/ml-lex from SMLNJ and compiling everything in PolyML. Do you by chance know whether it may work?

Thanks,

Bow-Yaw