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
prefix=/opt/polyml/polyml-r1848d
exec_prefix=${prefix}
bindir=${exec_prefix}/bin
libdir=${exec_prefix}/lib
includedir=${prefix}/include
Name: Poly/ML
Description: Poly/ML Standard ML Compiler
URL: http://www.polyml.org/
Version: 5.5.1
Requires:
Libs: -L${libdir} -lpolymain -lpolyml
Libs.private: -lpthread -lgmp -lm -ldl -lstdc++ -lgcc_s -lgcc
Cflags: -I${includedir}
prefix=/opt/polyml/polyml-r1848
exec_prefix=${prefix}
bindir=${exec_prefix}/bin
libdir=${exec_prefix}/lib
includedir=${prefix}/include
Name: Poly/ML
Description: Poly/ML Standard ML Compiler
URL: http://www.polyml.org/
Version: 5.5.1
Requires:
Libs: -L${libdir} -lpolymain -lpolyml -lpthread -lgmp -lm -ldl -lstdc++ -lgcc_s
-lgcc
Libs.private:
Cflags: -I${includedir}
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
