Hugh, > On 14 May 2017, at 03:21, Hugh Anderson <[email protected]> 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: [email protected] >>> SoC, National University of Singapore http://www.comp.nus.edu.sg/~hugh >>> _______________________________________________ >>> Proofpower mailing list >>> [email protected] >>> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com >> >> >> > > > Hugh Anderson E-mail: [email protected] > SoC, National University of Singapore http://www.comp.nus.edu.sg/~hugh > > _______________________________________________ > Proofpower mailing list > [email protected] > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
