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.
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.
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-Fe...
Makarius