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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
