[polyml] pkg-config for Poly/ML
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
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] Poly/ML 5.5.1
On 18/09/2013 18:21, Ramana Kumar wrote: Do you happen to know whether and how polyc could be used to build HOL4 when poly was built with --disabled-shared? I think I tried using polyc < tools/smart-configure.sml to start the HOL4 build process (i.e. using polyc instead of poly), but it didn't work. (I should try it again to be sure.) But would you expect to have to change the contents of smart-configure.sml to make this work? You can't use polyc < tools/smart-configure.sml. You will need to use "poly" here. You need to look more carefully at what smart-configure actually does. Somewhere in there it will either write out a script to link the object file or it will create a script which uses one of a number of pre-built scripts. All this is very specific to the HOL4 build process. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] Poly/ML 5.5.1
On Wed, Sep 18, 2013 at 12:51 PM, David Matthews < david.matth...@prolingua.co.uk> wrote: > On 17/09/2013 19:43, Ramana Kumar wrote: > >> I would like to report that the new default to not build a shared library >> means Poly/ML 5.5.1 does not build HOL4 unless you use the --enable-shared >> option at configure time. >> Is this as expected, or is there some other possible solution? >> > > This issue with HOL4 did come up during testing. It seems that when > libpolyml is built with --disable-shared it is necessary to give more > libraries on the linking line than when it is built with --enable-shared. > If the libraries are missing then you get the errors with missing symbols. > > 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. So, I would recommend that HOL4 and other applications check > for the presence of "polyc" and use that to do the linking if it is > available. > Do you happen to know whether and how polyc could be used to build HOL4 when poly was built with --disabled-shared? I think I tried using polyc < tools/smart-configure.sml to start the HOL4 build process (i.e. using polyc instead of poly), but it didn't work. (I should try it again to be sure.) But would you expect to have to change the contents of smart-configure.sml to make this work? > > By changing to --disable-shared as the default, I felt that this would > simplify the process of running applications, particularly "poly", at the > expense of making linking a bit more difficult. Those packaging Poly/ML > for particular distributions may want to use --enable-shared but they will > be installing libpolyml to a "standard" location where the loader can find > it. > > > Interestingly, even when --enable-shared is given at configure time, the >> polyc script prints some errors where it probably shouldn't: >> % polyc >> Usage: file [-bchikLlNnprsvz0] [--apple] [--mime-encoding] [--mime-type] >> [-e testname] [-F separator] [-f namefile] [-m magicfiles] >> file >> ... >> file -C [-m magicfiles] >> file [--help] >> /usr/lib/libpolymain.a(**polystub.o): In function `main': >> (.text.startup+0x1): undefined reference to `poly_exports' >> collect2: error: ld returned 1 exit status >> > > OK, I hadn't tested "polyc" without any arguments. That's a bug. It > ought to behave the same as > polyc --help > It is always supposed to be provided with a source or object file name. > > David > ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] Poly/ML 5.5.1
On 17/09/2013 19:43, Ramana Kumar wrote: I would like to report that the new default to not build a shared library means Poly/ML 5.5.1 does not build HOL4 unless you use the --enable-shared option at configure time. Is this as expected, or is there some other possible solution? This issue with HOL4 did come up during testing. It seems that when libpolyml is built with --disable-shared it is necessary to give more libraries on the linking line than when it is built with --enable-shared. If the libraries are missing then you get the errors with missing symbols. 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. So, I would recommend that HOL4 and other applications check for the presence of "polyc" and use that to do the linking if it is available. By changing to --disable-shared as the default, I felt that this would simplify the process of running applications, particularly "poly", at the expense of making linking a bit more difficult. Those packaging Poly/ML for particular distributions may want to use --enable-shared but they will be installing libpolyml to a "standard" location where the loader can find it. Interestingly, even when --enable-shared is given at configure time, the polyc script prints some errors where it probably shouldn't: % polyc Usage: file [-bchikLlNnprsvz0] [--apple] [--mime-encoding] [--mime-type] [-e testname] [-F separator] [-f namefile] [-m magicfiles] file ... file -C [-m magicfiles] file [--help] /usr/lib/libpolymain.a(polystub.o): In function `main': (.text.startup+0x1): undefined reference to `poly_exports' collect2: error: ld returned 1 exit status OK, I hadn't tested "polyc" without any arguments. That's a bug. It ought to behave the same as polyc --help It is always supposed to be provided with a source or object file name. David ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
