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

[Phil Clayton]

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
> 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch-3.1w7-pbc-20170513.diff.gz
Type: application/gzip
Size: 761 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20170514/984bbc3f/attachment.gz>