On 18 Apr 2015, at 18:19, Phil Clayton < 
<>> 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
> (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.



Proofpower mailing list

Reply via email to