On Mon, 10 Dec 2006, Ian Zimmerman wrote:
Makarius> cc -o HOL HOL.o -lpolymain -lpolyml -lstdc++
Not an expert, but have you tried -m32 ?
I've now tried something like this:
cc -o HOL HOL.o -Xlinker -melf_i386 -L/usr/proj/polyml/polyml-5.0/x86-linux -lpolymain -lpolyml -lstdc++
/usr/lib64/gcc/x86_64-suse-linux/4.0.2/../../../../x86_64-suse-linux/bin/ld: skipping incompatible /usr/lib64/gcc/x86_64-suse-linux/4.0.2/../../../../lib64/libstdc++.so when searching for -lstdc++ /usr/lib64/gcc/x86_64-suse-linux/4.0.2/../../../../x86_64-suse-linux/bin/ld: skipping incompatible /usr/lib64/gcc/x86_64-suse-linux/4.0.2/../../../../lib64/libstdc++.a when searching for -lstdc++
This looks better, since the linker seems to expect x86 binaries now. On the other hand my system appears to lack 32 bit versions of the basic gcc libraries.
BTW, that looks like you're trying to use the new Poly/ML with Isabelle, how's that working out?
I works very well, see http://www4.in.tum.de/~wenzelm/test/Isabelle2005-polyml-5.0.tar.gz
Makarius