Roger,

> On 30 Apr 2016, at 10:43, Roger Bishop Jones <r...@rbjones.com> 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 <r...@lemma-one.com 
>> <mailto:r...@lemma-one.com>> 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.

Regards,

Rob.

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to