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
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
