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 nothingOK, 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/bu...
Makarius