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.
A while ago, I experimented with this, creating the attached PC file for polyml and adapting a Makefile to use pkg-config to construct the polyml linker command-line options. This seems to work. For example, the Makefile rule (for Poly/ML built with --enable-shared)
$(NAME)-polyml : $(NAME)-polyml.o $(CC) -o $@ -L$(POLYMLLIB) -lpolymain -lpolyml $<
was changed to
$(CC) -o $@ `pkg-config --libs polyml` $<
given the attached polyml.pc in the pkg-config path. For static linking, this would be
$(CC) -o $@ -static `pkg-config --libs --static polyml` $<
however this requires all dependencies to be static: given that pkg-config generates command-line options for all dependencies, it is not possible to switch back and forth between -static and -dynamic.
For Poly/ML built with --disable-shared (now default) the same commands also work by using a slightly different polyml.pc where certain dependencies are moved from Libs.private to Libs as they are always required for linking. This is shown in polyml.pc-disable-shared, also attached.
With pkg-config, other variables can be extracted too. For example, the Makefile lines
POLYML := $(shell which poly 2> /dev/null) POLYMLBIN := $(patsubst %/,%,$(dir $(POLYML))) POLYMLHOME := $(patsubst %/,%,$(dir $(POLYMLBIN))) POLYMLLIB := $(POLYMLHOME)/lib
were replaced by
POLYMLBIN := `pkg-config --variable=bindir polyml` POLYMLLIB := `pkg-config --variable=libdir polyml` POLYML := $(POLYMLBIN)/poly POLYMLROOT := `pkg-config --variable=prefix polyml`
Furthermore, should any future enhancements to the FFI want to allow C-side code to reference symbols from Poly/ML H files, pkg-config can produce command-line options for C include directories too. I seem to recall that I once wanted to include a MLton H file in code on the C-side of the MLton FFI.
There is a default pkg-config path which can be overridden with the environment variable PKG_CONFIG_PATH. That seems as good a way as any to indicate which version of Poly/ML should be used when building an application.
Regards, Phil