On 19/04/15 17:16, Rob Arthan wrote:
On 18 Apr 2015, at 18:19, Phil Clayton <phil.clay...@lineone.net
I have build 3.1w5 and am seeing Z characters in the terminal which is
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
(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:
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
(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
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):
polyc -o xyz pp-ml.o
[...@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.
Proofpower mailing list