> On 30 Apr 2016, at 10:43, Roger Bishop Jones <> wrote:
> Rob,
> Thanks for you continuing support.

Not a problem. Thank you for persisting with this bit of the
installation, because I have a bit of difficulty testing it on
Mac OS in a clean environment. I will look into improving
the way I test it.

>> On 30 Apr 2016, at 10:16, Rob Arthan < 
>> <>> wrote:
> ...
>> Try it in in src/dev. I think it will fail. If so, try it without the 
>> obsolete options:
>>      polyc -o pp-ml pp-ml.o
> Here are the results:
> bash-3.2$ polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o
> Only one source file name allowed
> Usage: polyc [OPTION]... [SOURCEFILE]
> bash-3.2$ polyc -o pp-ml pp-ml.o
> ld: warning: could not create compact unwind for _ffi_call_unix64: does not 
> use RBP or RSP based frame
> So I need to build my own?

Hopefully not. That warning should be harmless.

I’ve just realised that it is only src/hol/hol.mkf which has this legacy way of
linking a poly executable. src/dev/dev.mkf creates slrp-ml the modern way
and will already have done that.

For the next step, I realise that you don’t need to edit thesrc/hol/hol.mkf:
to get it to call polyc correctly, run configure like this:

PPPOLYLINKFLAGS=“ “ ./configure

together with any other environment variable settings you need. I think there
is a good chance that the rest of the ML compilations will work then.



Proofpower mailing list

Reply via email to