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