Peter, Are you subscribed to the Poly/ML mailing list? Rob Arthan has also been asking about this and it makes sense that everyone is aware of the various issues. I'm copying this to the list as well.

Rob also found that ./configure --build=x86_64-darwin LDFLAGS='-segprot POLY rwx rwx' worked. I'm surprised that "make cvs" didn't appear to do anything but actually you don't need it in this case. Did you do a "make distclean" before the configure?

It would appear that the Mac OS X linker will require the LDFLAGS="-segprot POLY rwx rwx' option whenever an executable file is built using an exported Poly object file. I don't know how to do this with HOL; perhaps someone on the list will be able to help. I'll add it to the link step of Poly/ML but that won't help with Isabelle.

Regards, David

Peter Vincent Homeier wrote:

Dear David,

I tried the same thing on the developer (svn) version. I downloaded a clean new copy, and tried

./configure --build=x86_64-darwin LDFLAGS='-segprot POLY rwx rwx' make make cvs make sudo make install

and this all seemed to work. (Note that the "make cvs" seemed to have no effect.) However, when I then tried to build HOL4 (a theorem prover that built before with Poly/ML) I found that although I could build HOL4's lexer, when I tried to run this lexer to build the parser I got

Bus error

I could go back and try for the 32-bit versions as you suggested earlier, although I really would like to build the 64-bit version, given that much of the point of Snow Leopard is to be natively 64-bit as much as possible.

What would you suggest?

Cheers, Peter