Dear Poly/ML enthusiasts and experts of the gcc toolchain,
we've occasionally discussed the problem of building a "portable" Poly/ML on Linux, such that the resulting directory does not have to be "installed" in a fixed location such as /usr/bin and /usr/lib.
Here is my current approach to it, using an "rpath" in the poly executable and the chrpath tool to finalize it (on Ubuntu 16.04.3 LTS):
make distclean rm -rf target ./configure --prefix="$PWD/target" LDFLAGS=-Wl,-rpath,_DUMMY_ make compiler && make compiler && make install chrpath -r '$ORIGIN/../lib' target/bin/poly
Here is a proof for the result:
ldd target/bin/poly
linux-vdso.so.1 => (0x00007fffdc799000) libpolyml.so.9 => /home/makarius/lib/polyml/polyml-git/target/bin/../lib/libpolyml.so.9 (0x00007f4b02d98000) libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f4b029ce000) ...
Note that the approach with -rpath,_DUMMY_ and separate chrpath has two main reasons:
(1) I did not manage to pass $ORIGIN through LDFLAGS, configure, Makefile etc. unharmed, despite some attempts to escape the $ and some more backslashes.
(2) The -Wl,-rpath,_DUMMY_ retains a trace from the original target directory, but chrpath -r resets all that cleanly.
I am posting this here for the record, as a solution that works so far, see also http://isabelle.in.tum.de/repos/isabelle/file/8b19a8a7f029/src/Pure/Admin/bu...
Maybe there are further recommendations for simplification, e.g. smarter LDFLAGS could make the chrpath invocation obsolete (avoiding the requirement to install that tool from a separate Linux package).
Makarius