On 19/09/2013 07:44, Phil Clayton wrote:
18/09/13 12:51, David Matthews wrote:
The complication is that exactly which libraries have to be included depend on how libpolyml was built. The configure script detects the libraries that are needed to build "poly" and builds a linker command line from that. In particular, -lgmp is included only if GMP is present. This all makes it difficult for a build script such as that used by HOL4 to have a standard linker command line.
The idea of "polyc" is to capture the linker command line that was used to build "poly" on the particular platform and make it available for other applications. ...
One well-established aid for constructing suitable command-line options is pkg-config. This may be more useful for use in Makefiles due to greater flexibility than polyc. For pkg-config, a library installs a PC file. (There are quite a few examples in /usr/lib64/pkgconfig/ on my system.) This tells pkg-config which command line options are required for building with that library.
Thanks for the suggestion. It certainly seems like a good idea to install pkg-config files if possible. It does look as though they would have to be generated by a script in the same way as polyc is built by buildpolyc since the libraries would depend on what configure has found.
I don't know how useful it will be in general, though. I've done a quick look and pkg-config doesn't seem to be installed on several set-ups I looked at including Mac OS X and Solaris. The other problem is that it is going to require the PC files to be written into /usr/lib/pkgconfig or some other non-user-writable directory. One of the problems I was trying to work round was the fact that many users of Poly/ML are running on systems that are managed centrally and they don't have root access. It's this that makes shared libraries a problem because libpolyml can't be installed to /usr/lib or /usr/local/lib. All this means that anyone distributing code, such as HOL4 or Metit that are intended to be built with poly, can't rely on pkg-config.
David