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 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
> (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. 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
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
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.
Proofpower mailing list