On Wed, Sep 18, 2013 at 12:51 PM, David Matthews < David.Matthews at 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