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. 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.
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
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.
Regards,
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
