> On Feb 10, 2018, at 12:47, Makarius <makar...@sketis.net> wrote: > > On 10/02/18 21:16, Matthew Fernandez wrote: >> >> If I understand your aim correctly, you are trying to alter the path the >> runtime linker will use to find libpolyml.so. Is it not simpler to >> statically link to libpolyml instead? There’s probably a more elegant way to >> achieve this, but a blunt approach is: >> >> ./configure --disable-shared --prefix=/tmp/foo >> make >> make install >> ldd /tmp/foo/bin/poly | grep libpolyml # shows nothing > > OK, this appears to work, although I am unsure about the defaults: in > some of my build environments I get the effect of --disable-shared > without naming that option, but there is also --enable-shared to be > explicit about it.
I am not sure about the defaults either. Autotools seems to have various ways of tweaking this and I’m not an expert in this arena. I suspect --disable-shared only works coincidentally because the poly link step sees only the .a when it runs. > > What I did not explain in this mail thread: there are two main library > dependencies -- libpolyml and libgmp. The latter is often available on > Linux, but there is no guarantee -- it needs to be bundled with Poly/ML. Given the number of dependencies Isabelle ships with already, I agree including libgmp as well is probably the right way to go. In present times the pain of shipping larger binaries seems far less than the pain of debugging runtime linker issues. For what it’s worth, more modern tooling like CMake already defaults to static linking. > > The starting point for the current reorganization was actually a > conflict of the bundled libgmp vs. the system-installed libgmp, see > https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2018-February/007773.html > > > Makarius _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
