> On 30 Apr 2016, at 10:43, Roger Bishop Jones <r...@rbjones.com> wrote:
> 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.
Proofpower mailing list