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

[Hugh Anderson]

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).
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