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
            case units of
               Microseconds => Time.toMicroseconds |
               Milliseconds => Time.toMilliseconds |
               ... => ...)
            ) : (int -> int) * (Time.time -> LargeInt.int)
         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

Reply via email to