Re: [polyml] polyc and libraries
Phil, I've now added -lpolymain to polyml.pc.in so that should handle your specific problem. Can you check it? I'd be happy if you could produce an improved version of this. It's not something I use or have any familiarity with. Regards, David On 19/12/2017 21:47, Phil Clayton wrote: David, I think I would expect `pkg-config --libs polyml` to provide the linker flags required to create an executable, i.e. I wouldn't expect to have to specify -lpolymain additionally. I can't think of any other use cases of pkg-config because Poly/ML can't be used to produce a library. Even if it could, I don't believe adding -lpolymain would cause overlinking because only an archive version of libpolymain is available (and should always be available) and this shouldn't be included by the linker if there is no reference to the symbol "main". For Poly/ML built with --disable-shared, Libs still has all the linker flags, as I would expect, except for -lpolymain. If -lpolymain is added, it appears that it would need to be added _before_ -lpolyml (where it used to be), at least for my Linux distribution. On a separate note, for Poly/ML built with --enable-shared, I believe that the flags recently removed to avoid overlinking should still be produced if `pkg-config --static ...` is used, so should appear in Libs.private. However, it looks like this is only useful in the unusual case where all dependencies are to be statically linked. Most distributions don't supply archives for all libraries so that isn't usually possible. For Poly/ML built with --enable-shared, static linking of the Poly/ML library but not its dependencies is possible, e.g. gcc file.o \ -Wl,-Bstatic \ -L/tmp/polyml/lib -lpolymain -lpolyml \ -Wl,-Bdynamic \ -lpthread -lffi -lgmp -lm -ldl -lstdc++ -lgcc_s -lgcc but `pkg-config --static ...` can't produce such commands. Such a command could be produced with some shell trickery to get static-only dependencies, so perhaps it is worth supporting --static. Finally, I note that libffi has its own PC file, so when Poly/ML is built with --with-system-libffi, instead of adding -lffi to Libs/Libs.private, libffi could be added to Requires/Requires.private, respectively. Phil On 18/12/17 15:47, David Matthews wrote: Phil, I'm not exactly clear how pkg-config is supposed to be used. It's certainly possible to add -lpolymain explicitly to the libraries in polyml.pc. David On 17/12/2017 21:57, Phil Clayton wrote: David, On Fedora 25, polyc still appears to work for shared poly with this change. However, there is an issue for pkg-config because the libs section in polyml.pc no longer includes the flag -lpolymain causing a link error: /usr/lib/gcc/x86_64-redhat-linux/6.4.1/../../../../lib64/crt1.o: In function `_start': (.text+0x20): undefined reference to `main' collect2: error: ld returned 1 exit status Regards, Phil On 12/12/17 13:14, David Matthews wrote: The polyc script has been developed mainly to simplify the linking of an exported ML function and in particular to try to capture the libraries that need to be included. I've been having another look at this because of an issue that was reported a while back. Up till now the linking step has included all the libraries that were needed in order to link libpolyml itself. That was extracted by the configure script. It turns out that this is right if libpolyml is compiled as a static library but has a problem if libpolyml is a dynamic library. Object files exported by PolyML.export make reference to external symbols from libpolyml but do not directly reference anything else. If libpolyml is a dynamic library it exports these symbols but all the other dependencies are satisfied by loading the appropriate libraries dynamically. The issue was reported in the Fedora distribution but may also affect other distributions that package up Poly/ML and have separate packages for libraries (e.g. libgmp and libffi) and development packages. They were building libpolyml as a shared library but because polyc included the dependencies of libpolyml itself polyc was including -lgmp -lffi in the link step. This meant that it needed the development versions of these libraries even though they were not actually used. I've now modified the configure script so that polyc only includes the dependent libraries if libpolyml has been built with shared libraries disabled and at the same time changed the default so that it builds a shared library unless --disable-shared is given. Hopefully this hasn't broken anything but I'd appreciate any reports of problems. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
David, I think I would expect `pkg-config --libs polyml` to provide the linker flags required to create an executable, i.e. I wouldn't expect to have to specify -lpolymain additionally. I can't think of any other use cases of pkg-config because Poly/ML can't be used to produce a library. Even if it could, I don't believe adding -lpolymain would cause overlinking because only an archive version of libpolymain is available (and should always be available) and this shouldn't be included by the linker if there is no reference to the symbol "main". For Poly/ML built with --disable-shared, Libs still has all the linker flags, as I would expect, except for -lpolymain. If -lpolymain is added, it appears that it would need to be added _before_ -lpolyml (where it used to be), at least for my Linux distribution. On a separate note, for Poly/ML built with --enable-shared, I believe that the flags recently removed to avoid overlinking should still be produced if `pkg-config --static ...` is used, so should appear in Libs.private. However, it looks like this is only useful in the unusual case where all dependencies are to be statically linked. Most distributions don't supply archives for all libraries so that isn't usually possible. For Poly/ML built with --enable-shared, static linking of the Poly/ML library but not its dependencies is possible, e.g. gcc file.o \ -Wl,-Bstatic \ -L/tmp/polyml/lib -lpolymain -lpolyml \ -Wl,-Bdynamic \ -lpthread -lffi -lgmp -lm -ldl -lstdc++ -lgcc_s -lgcc but `pkg-config --static ...` can't produce such commands. Such a command could be produced with some shell trickery to get static-only dependencies, so perhaps it is worth supporting --static. Finally, I note that libffi has its own PC file, so when Poly/ML is built with --with-system-libffi, instead of adding -lffi to Libs/Libs.private, libffi could be added to Requires/Requires.private, respectively. Phil On 18/12/17 15:47, David Matthews wrote: Phil, I'm not exactly clear how pkg-config is supposed to be used. It's certainly possible to add -lpolymain explicitly to the libraries in polyml.pc. David On 17/12/2017 21:57, Phil Clayton wrote: David, On Fedora 25, polyc still appears to work for shared poly with this change. However, there is an issue for pkg-config because the libs section in polyml.pc no longer includes the flag -lpolymain causing a link error: /usr/lib/gcc/x86_64-redhat-linux/6.4.1/../../../../lib64/crt1.o: In function `_start': (.text+0x20): undefined reference to `main' collect2: error: ld returned 1 exit status Regards, Phil On 12/12/17 13:14, David Matthews wrote: The polyc script has been developed mainly to simplify the linking of an exported ML function and in particular to try to capture the libraries that need to be included. I've been having another look at this because of an issue that was reported a while back. Up till now the linking step has included all the libraries that were needed in order to link libpolyml itself. That was extracted by the configure script. It turns out that this is right if libpolyml is compiled as a static library but has a problem if libpolyml is a dynamic library. Object files exported by PolyML.export make reference to external symbols from libpolyml but do not directly reference anything else. If libpolyml is a dynamic library it exports these symbols but all the other dependencies are satisfied by loading the appropriate libraries dynamically. The issue was reported in the Fedora distribution but may also affect other distributions that package up Poly/ML and have separate packages for libraries (e.g. libgmp and libffi) and development packages. They were building libpolyml as a shared library but because polyc included the dependencies of libpolyml itself polyc was including -lgmp -lffi in the link step. This meant that it needed the development versions of these libraries even though they were not actually used. I've now modified the configure script so that polyc only includes the dependent libraries if libpolyml has been built with shared libraries disabled and at the same time changed the default so that it builds a shared library unless --disable-shared is given. Hopefully this hasn't broken anything but I'd appreciate any reports of problems. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
Phil, I'm not exactly clear how pkg-config is supposed to be used. It's certainly possible to add -lpolymain explicitly to the libraries in polyml.pc. David On 17/12/2017 21:57, Phil Clayton wrote: David, On Fedora 25, polyc still appears to work for shared poly with this change. However, there is an issue for pkg-config because the libs section in polyml.pc no longer includes the flag -lpolymain causing a link error: /usr/lib/gcc/x86_64-redhat-linux/6.4.1/../../../../lib64/crt1.o: In function `_start': (.text+0x20): undefined reference to `main' collect2: error: ld returned 1 exit status Regards, Phil On 12/12/17 13:14, David Matthews wrote: The polyc script has been developed mainly to simplify the linking of an exported ML function and in particular to try to capture the libraries that need to be included. I've been having another look at this because of an issue that was reported a while back. Up till now the linking step has included all the libraries that were needed in order to link libpolyml itself. That was extracted by the configure script. It turns out that this is right if libpolyml is compiled as a static library but has a problem if libpolyml is a dynamic library. Object files exported by PolyML.export make reference to external symbols from libpolyml but do not directly reference anything else. If libpolyml is a dynamic library it exports these symbols but all the other dependencies are satisfied by loading the appropriate libraries dynamically. The issue was reported in the Fedora distribution but may also affect other distributions that package up Poly/ML and have separate packages for libraries (e.g. libgmp and libffi) and development packages. They were building libpolyml as a shared library but because polyc included the dependencies of libpolyml itself polyc was including -lgmp -lffi in the link step. This meant that it needed the development versions of these libraries even though they were not actually used. I've now modified the configure script so that polyc only includes the dependent libraries if libpolyml has been built with shared libraries disabled and at the same time changed the default so that it builds a shared library unless --disable-shared is given. Hopefully this hasn't broken anything but I'd appreciate any reports of problems. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
On 15/12/2017 18:41, Makarius wrote: On 15/12/17 17:46, David Matthews wrote: On 15/12/2017 16:15, Makarius wrote: * The polyc script cannot handle directory names with spaces, e.g. the main "prefix". I guess it would need some extra quotation. Do you want to propose a fix? See the included change: my very first commit produced with git (with VSCode and gitk). Thanks. I've merged and pushed it. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
David, On Fedora 25, polyc still appears to work for shared poly with this change. However, there is an issue for pkg-config because the libs section in polyml.pc no longer includes the flag -lpolymain causing a link error: /usr/lib/gcc/x86_64-redhat-linux/6.4.1/../../../../lib64/crt1.o: In function `_start': (.text+0x20): undefined reference to `main' collect2: error: ld returned 1 exit status Regards, Phil On 12/12/17 13:14, David Matthews wrote: The polyc script has been developed mainly to simplify the linking of an exported ML function and in particular to try to capture the libraries that need to be included. I've been having another look at this because of an issue that was reported a while back. Up till now the linking step has included all the libraries that were needed in order to link libpolyml itself. That was extracted by the configure script. It turns out that this is right if libpolyml is compiled as a static library but has a problem if libpolyml is a dynamic library. Object files exported by PolyML.export make reference to external symbols from libpolyml but do not directly reference anything else. If libpolyml is a dynamic library it exports these symbols but all the other dependencies are satisfied by loading the appropriate libraries dynamically. The issue was reported in the Fedora distribution but may also affect other distributions that package up Poly/ML and have separate packages for libraries (e.g. libgmp and libffi) and development packages. They were building libpolyml as a shared library but because polyc included the dependencies of libpolyml itself polyc was including -lgmp -lffi in the link step. This meant that it needed the development versions of these libraries even though they were not actually used. I've now modified the configure script so that polyc only includes the dependent libraries if libpolyml has been built with shared libraries disabled and at the same time changed the default so that it builds a shared library unless --disable-shared is given. Hopefully this hasn't broken anything but I'd appreciate any reports of problems. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
On 15/12/2017 18:41, Makarius wrote: On 15/12/17 17:46, David Matthews wrote: On 15/12/2017 16:15, Makarius wrote: * The polyc script cannot handle directory names with spaces, e.g. the main "prefix". I guess it would need some extra quotation. Do you want to propose a fix? See the included change: my very first commit produced with git (with VSCode and gitk). Thanks. I'll have a look at that. * Instead of insisting in hardwired directory locations it should be possible to refer to the relative location of the polyc itself. In GNU bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to me how to do it in /bin/sh. The paths are set from the installation directories in configure i.e. where the binaries and libraries are to be installed. It's possible to set the library and binary directories independently so there's no necessary relationship between them. The above change might already be sufficient for that: isabelle build_polyml merely needs to change /bin/sh into bash and make the prefix relative. This will allow users of Isabelle to use the bundled Poly/ML polyc, even though it is not directly relevant for Isabelle -- see also https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-February/msg00144.html I don't think you can give configure anything but absolute paths but when I'm testing I usually set --libdir, --bindir and --mandir to the same directory so everything ends up in the same place. The only case where I've had a problem is with shared libraries in Msys/Mingw where libtool insists on putting the DLL in "libdir/../bin". I see further references to the install dir in: pkgconfig/polyml.pc libpolymain.la libpolyml.la Are these relevant for polyc? No. polyml.pc is only used if you have pkg_config. The other two are only used by libtool as far as I'm aware. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
On 15/12/2017 16:15, Makarius wrote: On 12/12/17 14:14, David Matthews wrote: The polyc script has been developed mainly to simplify the linking of an exported ML function and in particular to try to capture the libraries that need to be included. I've been having another look at this because of an issue that was reported a while back. Here are some further observations and open problems from the past: * The polyc script cannot handle directory names with spaces, e.g. the main "prefix". I guess it would need some extra quotation. Do you want to propose a fix? * Instead of insisting in hardwired directory locations it should be possible to refer to the relative location of the polyc itself. In GNU bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to me how to do it in /bin/sh. The paths are set from the installation directories in configure i.e. where the binaries and libraries are to be installed. It's possible to set the library and binary directories independently so there's no necessary relationship between them. * Use of libgmp on Mac OS X is generally unclear to me. Is there a robust way to build poly with gmp on an old OS version (e.g. Mac OS X 10.10) and use it on a newer one? Is there any chance to do this with x86 instead of x86_64? There have been problems with linking libgmp and Poly/ML on Mac OS X in the past. Is there someone who uses Mac OS who could answer this? David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
There seems to be a problem with building it as a shared library in FreeBSD. It seems to work fine with ./configure --disable-shared David On 15/12/2017 12:58, Kostirya wrote: It is broken. I think this is because of the inconsistency of the options: -nostdlib and -lstdc++. libtool: link: c++ -fPIC -DPIC -shared -nostdlib /usr/lib/crti.o /usr/lib/crtbeginS.o .libs/arb.o .libs/basicio.o .libs/bitmap.o .libs/check_objects.o .libs/diagnostics.o .libs/errors.o .libs/exporter.o .libs/foreign.o .libs/gc.o .libs/gc_check_weak_ref.o .libs/gc_copy_phase.o .libs/gc_mark_phase.o .libs/gc_share_phase.o .libs/gc_update_phase.o .libs/gctaskfarm.o .libs/heapsizing.o .libs/locking.o .libs/memmgr.o .libs/mpoly.o .libs/network.o .libs/objsize.o .libs/osmem.o .libs/pexport.o .libs/poly_specific.o .libs/polyffi.o .libs/polystring.o .libs/process_env.o .libs/processes.o .libs/profiling.o .libs/quick_gc.o .libs/realconv.o .libs/reals.o .libs/rts_module.o .libs/rtsentry.o .libs/run_time.o .libs/save_vec.o .libs/savestate.o .libs/scanaddrs.o .libs/sharedata.o .libs/sighandler.o .libs/statistics.o .libs/timing.o .libs/xwindows.o .libs/x86_dep.o .libs/x86assembly_gas32.o .libs/elfexport.o .libs/unix_specific.o -Wl,--whole-archive libffi/.libs/libffi_convenience.a -Wl,--no-whole-archive -L/usr/local/lib -lpthread -lgmp -lstdc++ -L/usr/lib -lc++ -lm -lc -lgcc -lgcc_s /usr/lib/crtendS.o /usr/lib/crtn.o -O3 -Wl,-soname -Wl,libpolyml.so.9 -o .libs/libpolyml.so.9.0.0 /usr/bin/ld: cannot find -lstdc++ c++: error: linker command failed with exit code 1 (use -v to see invocation) *** Error code 1 Stop. make[1]: stopped in /scr/polyml_git/libpolyml *** Error code 1 I delete AC_CHECK_LIB(stdc++, main) line from configure.ac and do successfully built polyml on FreeBSD and DragonFlyBSD. But stdc++ is need for linux... ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] polyc and libraries
On 12/12/17 14:14, David Matthews wrote: > The polyc script has been developed mainly to simplify the linking of an > exported ML function and in particular to try to capture the libraries > that need to be included. I've been having another look at this because > of an issue that was reported a while back. Here are some further observations and open problems from the past: * The polyc script cannot handle directory names with spaces, e.g. the main "prefix". * Instead of insisting in hardwired directory locations it should be possible to refer to the relative location of the polyc itself. In GNU bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to me how to do it in /bin/sh. * Use of libgmp on Mac OS X is generally unclear to me. Is there a robust way to build poly with gmp on an old OS version (e.g. Mac OS X 10.10) and use it on a newer one? Is there any chance to do this with x86 instead of x86_64? Makarius ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
