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 [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
