On 13/01/2014 22:31, Michael Norrish wrote:

I'll look at the relevant lib directories; thanks.

The reason is that the HOL build process wants to create executables (for mlyacc, mllex and others), and doing so without --enable-shared will fail mysteriously. If I can cut this off at the pass, I can provide better error messages.

There was a problem that I discovered with making --disable-shared the default that I hadn't anticipated. It seems that when linking with the static library it is necessary to include some extra libraries (e.g. gmp) that are used within libpolyml. These don't seem to be needed when linking with the dynamic library so presumably they have already been linked into the dynamic library.

I confess I haven't properly looked at polyc; would this give us a uniform approach?

That is the intention. "polyc" is written as part of the process of building "poly" and should include all the libraries that are needed.

Regards, David