Roger,
> On 29 Apr 2016, at 23:16, Roger Bishop Jones <r...@rbjones.com> wrote:
>
> Rob,
>
>> On 29 Apr 2016, at 20:31, Rob Arthan <r...@lemma-one.com> wrote:
>>
>>
>> The linker can’t find the gmp library. What version of Poly/ML are you
>> using? Did you build
>> it yourself or download it ready-made from somewhere?
>>
>
> I did:
> port install polymer
>
> poly -v gives
>
> Poly/ML 5.5.2 Release RTS version: X86_64-5.5.1
>
>
OK. You may need to build your own, but let's see if we can get it working
with the MacPorts version.
>> If you go into src/dev, what happens if you run the following command
>> interactively?
>>
>
> src/dev where? Can’r find one.
In the directory OpenProofPower-3.1w7 you got when you unpacked the tarball.
>
> But if I run it in my home directory I get:
>
> Rogers-MacBook:~ rbj$ polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o
> Only one source file name allowed
> Usage: polyc [OPTION]... [SOURCEFILE]
>
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
If that works, then if you get rid of those options from the polyc command
lines in src/dev/dev.mkf and src/hol/hol.mkf, you should get a bit further.
Regards,
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
