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-February/007773.html Makarius _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
