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

[Hugh Anderson]

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

[Hugh Anderson]

Hi - I just tried using SMLNJ instead of polyML, but I got the same error
at the same place...

Cheers Hugh

Post by Hugh Anderson
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

...

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

[Phil Clayton]

I have successfully built ProofPower with SML/NJ 110.81 which was
recently released. (That was on Fedora but any SML type errors should
be the same on different platforms.) I haven't tried earlier versions.

In the ProofPower source directory, did you run
./distclean
before rebuilding?

Phil

Post by Hugh Anderson
Hi - I just tried using SMLNJ instead of polyML, but I got the same
error at the same place...
Cheers Hugh

Post by Hugh Anderson
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

...
SoC, National University of Singapore http://www.comp.nus.edu.sg/~hugh
_______________________________________________
Proofpower mailing list
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[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

Post by Hugh Anderson
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
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
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
imp001.sml:825: error: Type error in function application.
Function: o : (int -> int) * (Time.time -> int) -> Time.time -> int
(
TimeInt.toInt,
(
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
SoC, National University of Singapore http://www.comp.nus.edu.sg/~hugh
_______________________________________________
Proofpower mailing list
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[Hugh Anderson]

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

Post by 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,
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
http://www.lemma-one.com/ProofPower/patches/patches.html
Regards,
Phil

Post by Hugh Anderson
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
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
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
imp001.sml:825: error: Type error in function application.
Function: o : (int -> int) * (Time.time -> int) -> Time.time -> int
(
TimeInt.toInt,
(
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
SoC, National University of Singapore http://www.comp.nus.edu.sg/~hugh
_______________________________________________
Proofpower mailing list
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

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

[Rob Arthan]

Hugh,

Post by Hugh Anderson
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.

Post by Hugh Anderson
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

Post by Phil Clayton
Hi Hugh,
In brief, try the attached patch.
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.
http://www.lemma-one.com/ProofPower/patches/patches.html
Regards,
Phil

Post by Hugh Anderson
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
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$
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$
imp001.sml:825: error: Type error in function application.
Function: o : (int -> int) * (Time.time -> int) -> Time.time -> int
(
TimeInt.toInt,
(
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
SoC, National University of Singapore http://www.comp.nus.edu.sg/~hugh
_______________________________________________
Proofpower mailing list
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

SoC, National University of Singapore http://www.comp.nus.edu.sg/~hugh
_______________________________________________
Proofpower mailing list
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com