[polyml] Building portable Poly/ML on Linux

[Makarius]

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

[Matthew Fernandez]

Hi Makarius,

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

Post by Makarius
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
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
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
(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
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

[Makarius]

Post by Matthew Fernandez
./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

[Matthew Fernandez]

Post by Makarius

Post by Matthew Fernandez
./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.

Post by Makarius
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.

Post by Makarius
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

[Ian Zimmerman]

Post by Matthew Fernandez
Given the number of dependencies Isabelle ships with already, I agree
including libgmp as well is probably the right way to go. times the
pain of shipping larger binaries seems far less than the pain of
debugging runtime linker issues.

Size has not been the main motivation for shared libraries for a long time.

[Makarius]

Post by Makarius

Post by Matthew Fernandez
./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 have made some further experiments with --enable-shared, in order to
reuse the special tricks for libgmp are also for libpolyml.

The results are platform-dependent:

* x86-linux, x86_64-linux: works

* x86-windows, x86_64-windows, x86-darwin: build fails (crash of polyimport)

* x86_64-darwin: build works, but running it on a different machine
failed (cannot load libpolyml)


In conclusion, I am mostly back to the original setup, but now have
--enabled-shared for Linux to make explicit that this is active here --
it works thanks to LDFLAGS=-Wl,-rpath,_DUMMY_ and chrpath -r '$ORIGIN' poly.

For the full record see
http://isabelle.in.tum.de/repos/isabelle/file/d515b6140381/src/Pure/Admin/build_polyml.scala


Makarius