[ProofPower] Setting up on macosx Sierra fails...

[Rob Arthan]

Hugh,

> On 14 May 2017, at 03:21, Hugh Anderson <hugh at comp.nus.edu.sg> wrote:
> 
> 
> Hi Phil,
> 
> That does the trick! With polyml it now compiles and installs correctly on my up-to-date sierra, and the version of Poly/ML that brew installs (5.7).

The folk who maintain brew must be very quick off the mark: Poly/ML 5.7 was only
announced as released on 12th May. 

I have been working on making ProofPower compatible with Poly/ML 5.7
compiled with or without --enable-intinf-as-int. This isn't fully tested yet,
but it will be in the next release.

Thanks to Phil for supplying a work-around.

Regards,

Rob.

> I also tried using smlnj (On a mac at the moment, brew installs 110.80), and this also installed perfectly.
> 
> Thanks very much for your patch...
> 
> Cheers Hugh
> 
> On Sun, 14 May 2017, Phil Clayton wrote:
> 
>> Hi Hugh,
>> 
>> In brief, try the attached patch.
>> 
>> As of Poly/ML 5.7, the types int and LargeInt.int are no longer the same, hence your error:
>> 
>>      Reason:
>>         Can't unify int (*In Basis*) with LargeInt.int (*In Basis*)
>>            (Different type constructors)
>> 
>> When building Poly/ML 5.7, giving --enable-intinf-as-int as an argument to ./configure would avoid this issue.  However, I have just discovered that the build still won't work.  With Poly/ML 5.7, I get a build failure in imp108.sml because the types int and FixedInt.int are not the same.  This seems to be a change between Poly/ML 5.6.1 Testing and the final Poly/ML 5.7.
>> 
>> The attached patch should fix both issues and allow you to build with Poly/ML 5.7.  I have only tested on my Fedora machine.  Apply as usual, according to the instructions here:
>> http://www.lemma-one.com/ProofPower/patches/patches.html
>> 
>> Regards,
>> Phil
>> 
>> On 13/05/17 04:20, Hugh Anderson wrote:
>>> Hi - I am trying to install ProofPower-Z using my new mac/Sierra machine,
>>> using polyml, installed from brew: Poly/ML 5.7 Release RTS version: X86_64-5.6
>>> I applied the MAC patch in the OpenProofPower-3.1w7 directory:
>>> 
>>>     Hughs-MacBook:OpenProofPower-3.1w7 hugh$ cat ../patch-3.1.rda.20170310.diff| patch -p1 -b -B orig/
>>>        patching file configure
>>>        Hunk #1 FAILED at 25.
>>>        Hunk #3 FAILED at 71.
>>>        2 out of 6 hunks FAILED -- saving rejects to file configure.rej
>>>        patching file src/hol/hol.mkf
>>>        patching file src/pptex/imp096.doc
>>>        patching file src/xpp/imp096.doc
>>>     Hughs-MacBook:OpenProofPower-3.1w7 hugh$
>>> These two hunks did not seem important to me, so I carried on, but the configure failed. The offending part seemed to be attempting to build slrp-bin:
>>> 
>>>    Hughs-MacBook:OpenProofPower-3.1w7 hugh$ tail -7 build.log
>>>       docsml -f hol.svf imp018
>>>       docsml -f hol.svf dtd017
>>>       echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1
>>>       polyc -o slrp-bin slrp-bin.o
>>>       Error: slrp-bin.o: No such file
>>>       Usage: polyc [OPTION]... [SOURCEFILE]
>>>       make: *** [slrp-bin] Error 1
>>>     Hughs-MacBook:OpenProofPower-3.1w7 hugh$
>>> I had a look at the src/dev/slrp-bin.log file, and found two errors like this:
>>> 
>>>    imp001.sml:825: error: Type error in function application.
>>>       Function: o : (int -> int) * (Time.time -> int) -> Time.time -> int
>>>       Argument:
>>>          (
>>>             TimeInt.toInt,
>>>             (
>>>             case units of
>>>                Microseconds => Time.toMicroseconds |
>>>                Milliseconds => Time.toMilliseconds |
>>>                ... => ...)
>>>             ) : (int -> int) * (Time.time -> LargeInt.int)
>>>       Reason:
>>>          Can't unify int (*In Basis*) with LargeInt.int (*In Basis*)
>>>             (Different type constructors)
>>>    Found near
>>>      TimeInt.toInt o
>>>      (
>>>      case units of
>>>         Microseconds => Time.toMicroseconds |
>>>         Milliseconds => Time.toMilliseconds |
>>>         Seconds => Time.toSeconds)
>>>    ...
>>>    Exception- Fail "Static Errors" raised
>>> So - is there some update or patch I can apply? This all worked fine for me on my old mac :) - maybe an  El Capitan / Sierra change? Or a change to
>>> sml/time declarations?
>>> Can anyone help? Cheers Hugh
>>> Hugh Anderson                             E-mail: hugh at comp.nus.edu.sg
>>> SoC, National University of Singapore     http://www.comp.nus.edu.sg/~hugh
>>> _______________________________________________
>>> Proofpower mailing list
>>> Proofpower at lemma-one.com
>>> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>> 
>> 
>> 
> 
> 
> Hugh Anderson                             E-mail: hugh at comp.nus.edu.sg
> SoC, National University of Singapore     http://www.comp.nus.edu.sg/~hugh
> 
> _______________________________________________
> Proofpower mailing list
> Proofpower at lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com