Roger, > On 30 Apr 2016, at 10:43, Roger Bishop Jones <[email protected]> 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 <[email protected] >> <mailto:[email protected]>> 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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
