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.6I 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" raisedSo - 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 tosml/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
patch-3.1w7-pbc-20170513.diff.gz
Description: application/gzip
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
