Rob,

On 19/04/15 17:16, Rob Arthan wrote:
Phil,

On 18 Apr 2015, at 18:19, Phil Clayton <phil.clay...@lineone.net
<mailto:phil.clay...@lineone.net>> wrote:

Rob,

I have build 3.1w5 and am seeing Z characters in the terminal which is
great!

Glad you like it!

I find that I need to set LD_LIBRARY_PATH for the Poly/ML libraries
when running.  I suspect that this is because the polyc command in
HOLSTARTCMD in hol.mkf does does not include
 LD_RUN_PATH=$(LD_RUN_PATH)
(Similarly for SLRPSTARTCMD in dev.mkf)
Is there any reason for that?

The idea of polyc was to prevent you having to do that
kind of thing.

polyc ducks the issue of the run path though. I raised this with David when polyc first appeared - see the thread starting here:
http://lists.inf.ed.ac.uk/pipermail/polyml/2013-April/001216.html

David was concerned that some linkers may not support rpaths and did not know of any way to check with autotools. Also, there was some concern about Linux distributions with objects to rpaths - for example see discussion starting "Libtool's use of `-rpath'..." at
https://www.sourceware.org/autobook/autobook/autobook_88.html
(where the authors of Libtool say "using rpath is a good thing".)


I don’t know how it achieves it because it doesn't set
LD_RUN_PATH (or Mac OS equivalent), but I don’t
have this problem on any system I have tried.
I have just installed it on Kubuntu 12.10 having made sure that
LD_RUN_PATH and LD_LIBRARY_PATH are not set and
it works.

Did you specify a prefix when you installed Poly/ML? The problem occurs only when Poly/ML is installed to a non-system location, i.e. where the libraries are in a location not known to ld.


Unfortunately, because the makefiles defend themselves against polyc
not being there. it is a a bit difficult to tell exactly what happened
during the build. Can you unset LD_RUN_PATH and then
try this starting from  the build directory (assuming you have done
a build and haven’t cleaned up after it):

cd src/hol
polyc -o xyz pp-ml.o
xyz hol.polydb

[...@rizzo OpenProofPower-3.1w5]$ unset LD_RUN_PATH
[...@rizzo OpenProofPower-3.1w5]$ cd src/hol/
[...@rizzo hol]$ polyc -o xyz pp-ml.o
[...@rizzo hol]$ ./xyz hol.polydb
./xyz: error while loading shared libraries: libpolyml.so.6: cannot open shared object file: No such file or directory


That should start an HOL session. If it doesn’t then I think there
is a bug in polyc on your system and we should manufacture a
cut-down example and report it.

As noted, this behaviour of polyc is expected. In fact, this is why --disable-shared became the default when building Poly/ML. The upshot of the previous discussion was that users should either
 A. use the non-shared version
 B. add their installation to the ld config, /etc/ld.so.conf
or, as discussed
 C. set LD_LIBRARY_PATH if installed to a non-system location
(Are there any others?)

Whilst LD_RUN_PATH=... does work with polyc, I've now realized that that doesn't work for Mac OS X. Possibly Mac OS X needs additional arguments, e.g. -Wl,-rpath,$(POLYML_LIBDIR), but polyc has no mechanism to pass additional arguments, if I remember correctly.

It's not a major issue for me - I can just build ProofPower with a static Poly/ML. I just mentioned it to make ProofPower more portable.

Regards,
Phil


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to