Re: [polyml] Building portable Poly/ML on Linux
On 10/02/18 21:47, Makarius wrote: > 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. 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 ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] Building portable Poly/ML on Linux
On 2018-02-10 14:19, Matthew Fernandez wrote: > 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. -- Please don't Cc: me privately on mailing lists and Usenet, if you also post the followup to the list or newsgroup. To reply privately _only_ on Usenet, fetch the TXT record for the domain. ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Re: [polyml] Building portable Poly/ML on Linux
> On Feb 10, 2018, at 12:47, Makarius wrote: > > 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. 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. > > 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. > > 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
Re: [polyml] Building portable Poly/ML on Linux
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
Re: [polyml] Building portable Poly/ML on Linux
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 > On Feb 9, 2018, at 12:55, Makarius wrote: > > 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 => (0x7fffdc799000) > libpolyml.so.9 => > /home/makarius/lib/polyml/polyml-git/target/bin/../lib/libpolyml.so.9 > (0x7f4b02d98000) > libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x7f4b029ce000) >... > > > 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 ___ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
[polyml] Building portable Poly/ML on Linux
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 => (0x7fffdc799000) libpolyml.so.9 => /home/makarius/lib/polyml/polyml-git/target/bin/../lib/libpolyml.so.9 (0x7f4b02d98000) libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x7f4b029ce000) ... 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
