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