Is there a reason why this is used for libpolyml in the beta sources, instead of the -version-info or -version-number options as recommended by libtool manual?
I am debianizing and lintian objects hard.
On Sun, 9 Dec 2006, Ian Zimmerman wrote:
Is there a reason why this is used for libpolyml in the beta sources, instead of the -version-info or -version-number options as recommended by libtool manual?
This sounds like you are an expert on libtool etc. Maybe you happen to know how to link an x86 application on an x86_64 platform.
Let's assume the x86 version of poly has been started on a x86_64 system. Then do this from ML and exit:
PolyML.export ("HOL", PolyML.rootFunction);
No try to link as follows:
cc -o HOL HOL.o -lpolymain -lpolyml -lstdc++
/usr/lib64/gcc/x86_64-suse-linux/4.0.2/../../../../x86_64-suse-linux/bin/ld: skipping incompatible /usr/proj/polyml/polyml-5.0/x86-linux/libpolymain.a when searching for -lpolymain /usr/lib64/gcc/x86_64-suse-linux/4.0.2/../../../../x86_64-suse-linux/bin/ld: cannot find -lpolymain collect2: ld returned 1 exit status
Is there a magic option for ld to force x86 binaries on a x86_64 system.
Makarius
Makarius> Maybe you happen to know how to link an x86 application on an Makarius> x86_64 platform.
Makarius> Let's assume the x86 version of poly has been started on a Makarius> x86_64 system. Then do this from ML and exit:
Makarius> PolyML.export ("HOL", PolyML.rootFunction);
Makarius> No try to link as follows:
Makarius> cc -o HOL HOL.o -lpolymain -lpolyml -lstdc++
Not an expert, but have you tried -m32 ?
BTW, that looks like you're trying to use the new Poly/ML with Isabelle, how's that working out?
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
-
itz＠madbat.mine.nu -
makarius＠sketis.net