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: h...@comp.nus.edu.sg
SoC, National University of Singapore     http://www.comp.nus.edu.sg/~hugh

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com






Hugh Anderson                             E-mail: h...@comp.nus.edu.sg
SoC, National University of Singapore     http://www.comp.nus.edu.sg/~hugh

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to