Hi All, I'm sorry if this is not the proper place to ask, but I'll try to be "short".
I've been trying to get Isabelle in my macbook and I've joined their discussion list for support. They told me intel macbooks wont work with the modified polyml_ppc_darwin, and sent me a patch to get it working with Polyml 5.0. I tried both Polyml 5.0 and the one from the top SVN tree, and when I try to compile I get the same error:
/bin/sh ../libtool --tag=3DCXX --mode=3Dcompile g++ -DHAVE_CONFIG_H -I. -= I.. -DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c -o machoexport.lo machoexport.cpp g++ -DHAVE_CONFIG_H -I. -I.. -DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c machoexport.cpp -fno-common -DPIC -o .libs/machoexport.o machoexport.h:49: error: 'uint' has not been declared machoexport.h:49: error: 'uint' has not been declared machoexport.h:49: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared make[2]: *** [machoexport.lo] Error 1 make[1]: *** [all-recursive] Error 1 make: *** [all] Error 2 sh-3.2#
Any idea?
thanks,
Fernando
just answering my own e-mail I created a typedef from uint to unsigned which seems to have fixed it.
On 10/30/07, Fernando Costa cusquinho@gmail.com wrote:
Hi All,
I'm sorry if this is not the proper place to ask, but I'll try to be "short".
I've been trying to get Isabelle in my macbook and I've joined their discussion list for support. They told me intel macbooks wont work with t=
he
modified polyml_ppc_darwin, and sent me a patch to get it working with Polyml 5.0. I tried both Polyml 5.0 and the one from the top SVN tree, and when I try to compile I get the same error:
/bin/sh ../libtool --tag=3DCXX --mode=3Dcompile g++ -DHAVE_CONFIG_H -I.=
-I..
-DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c -o machoexport.lo machoexport.cpp g++ -DHAVE_CONFIG_H -I. -I.. -DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c machoexport.cpp -fno-common -DPIC -o .libs/machoexport.o machoexport.h:49: error: 'uint' has not been declared machoexport.h:49: error: 'uint' has not been declared machoexport.h :49: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp :241: error: 'uint' has not been declared make[2]: *** [machoexport.lo] Error 1 make[1]: *** [all-recursive] Error 1 make: *** [all] Error 2 sh-3.2#
Any idea?
thanks,
Fernando
Everything compiled and installed. But this is as far as I could get: sh-3.2# /usr/local/bin/poly
The exported object file does not match this version of the library sh-3.2#
Any ideas?
Thanks
On 10/30/07, Fernando Costa cusquinho@gmail.com wrote:
just answering my own e-mail I created a typedef from uint to unsigned which seems to have fixed it.
On 10/30/07, Fernando Costa < cusquinho@gmail.com> wrote:
Hi All,
I'm sorry if this is not the proper place to ask, but I'll try to be "short".
I've been trying to get Isabelle in my macbook and I've joined their discussion list for support. They told me intel macbooks wont work with=
the
modified polyml_ppc_darwin, and sent me a patch to get it working with Polyml 5.0. I tried both Polyml 5.0 and the one from the top SVN tree, and when I try to compile I get the same error:
/bin/sh ../libtool --tag=3DCXX --mode=3Dcompile g++ -DHAVE_CONFIG_H -=
I.
-I.. -DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c -o machoexport.lo machoexport.cpp g++ -DHAVE_CONFIG_H -I. -I.. -DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c machoexport.cpp -fno-common -DPIC -o .libs/machoexport.o machoexport.h:49: error: 'uint' has not been declared machoexport.h:49: error: 'uint' has not been declared machoexport.h :49: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp :241: error: 'uint' has not been declared make[2]: *** [machoexport.lo] Error 1 make[1]: *** [all-recursive] Error 1 make: *** [all] Error 2 sh-3.2#
Any idea?
thanks,
Fernando
Fernando Costa wrote:
Everything compiled and installed. But this is as far as I could get: sh-3.2# /usr/local/bin/poly
The exported object file does not match this version of the library sh-3.2#
Any ideas?
Have you got another version of the poly libraries installed e.g. in /usr/lib ?
If you have you may want to consider configure --prefix=/usr to force the libraries to be installed there and to overwrite them.
David.
If you don't use fink ignore this message...
If you do use fink I am currently in the process of creating a polyml5 package for fink. I have attached the polyml5.info file. If you put this in /sw/fink/dists/local/main/finkinfo/languages/ then fink index and fink install polyml5 you should get a working version of polyml5. I've also attached the isabelle-polyml5.info and .patch files and the proofgeneral.info and proofgeneral.patch files. All-in- all if you install all three of these packages you should get a working version of Isabelle using polyml5.
I created these packages because I acquired an Intel iMac. They have been submitted to fink but not yet accepted; I would appreciate feed- back.
Peace - John
John> If you don't use fink ignore this message... If you do use fink I John> am currently in the process of creating a polyml5 package for John> fink. I have attached the polyml5.info file. If you put this in John> /sw/fink/dists/local/main/finkinfo/languages/ then fink index and John> fink install polyml5 you should get a working version of polyml5. John> I've also attached the isabelle-polyml5.info and .patch files and John> the proofgeneral.info and proofgeneral.patch files. All-in- all John> if you install all three of these packages you should get a John> working version of Isabelle using polyml5.
John> I created these packages because I acquired an Intel iMac. They John> have been submitted to fink but not yet accepted; I would John> appreciate feed- back.
Does your isabelle package rebuild the logics from scratch?
I am asking because I am not able to do that with polyml5, I run out of memory building HOL (on Debian, 1G RAM, 1G swap).
Yes, it does rebuild the logics from scratch. it takes a while...
I have built it on: Dual-processor G5 (2GB RAM, more swap) iBook G4 (1.25GB RAM, more swap) intel iMac (4GB RAM)
Peace - John
On Oct 30, 2007, at 8:22 PM, Ian Zimmerman wrote:
John> If you don't use fink ignore this message... If you do use fink I John> am currently in the process of creating a polyml5 package for John> fink. I have attached the polyml5.info file. If you put this in John> /sw/fink/dists/local/main/finkinfo/languages/ then fink index and John> fink install polyml5 you should get a working version of polyml5. John> I've also attached the isabelle-polyml5.info and .patch files and John> the proofgeneral.info and proofgeneral.patch files. All-in- all John> if you install all three of these packages you should get a John> working version of Isabelle using polyml5.
John> I created these packages because I acquired an Intel iMac. They John> have been submitted to fink but not yet accepted; I would John> appreciate feed- back.
Does your isabelle package rebuild the logics from scratch?
I am asking because I am not able to do that with polyml5, I run out of memory building HOL (on Debian, 1G RAM, 1G swap).
-- Ham is for reading, not for eating.
Fernando Costa wrote:
I've been trying to get Isabelle in my macbook and I've joined their discussion list for support. They told me intel macbooks wont work with the modified polyml_ppc_darwin, and sent me a patch to get it working with Polyml 5.0. I tried both Polyml 5.0 and the one from the top SVN tree, and when I try to compile I get the same error:
/bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I.. -DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c -o machoexport.lo machoexport.cpp g++ -DHAVE_CONFIG_H -I. -I.. -DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c machoexport.cpp -fno-common -DPIC -o .libs/machoexport.o machoexport.h:49: error: 'uint' has not been declared machoexport.h:49: error: 'uint' has not been declared machoexport.h:49: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared
I don't know why uint has been used here since it doesn't exactly correspond to the types needed for the nlist struct. I've changed it (in CVS) to use unsigned char and unsigned long so this should be fixed.
David.
Skipped content of type multipart/alternative-------------- next part -----= --------- A non-text attachment was scrubbed... Name: polyml5.info Type: application/octet-stream Size: 2630 bytes Desc: not available Url : http://lists.inf.ed.ac.uk/mailman/private/polyml/attachments/20071030= /7f7c501c/polyml5.obj
What does otool -L /sw/bin/poly report?
Peace - John
On Oct 30, 2007, at 8:15 PM, Fernando Costa wrote:
Hi,
John, that's a very nice package. I'll e-mail people from Fink asking them to include your package.
The reason I'm having the uint issue, is probably related to Leopard. I've created a patch inside Fink in order to apply David fix (attached).
Although I was able to get the package installed just fine with fink, I still get this:
sh-3.2# /sw/bin/poly
The exported object file does not match this version of the library sh-3.2#
I'm guessing this is Leopard related, here are my libs:
sh-3.2# find / |grep libpoly /sw/fink/10.4/unstable/main/finkinfo/sci/libpolyxmass10.info /sw/fink/10.4/unstable/main/finkinfo/sci/libpolyxmass10.patch /sw/lib/libpolymain.a /sw/lib/libpolymain.la /sw/lib/libpolyml- 5.0.0.dylib /sw/lib/libpolyml-5.0.dylib /sw/lib/libpolyml-5.dylib /sw/lib/libpolyml.a /sw/lib/libpolyml.dylib /sw/lib/libpolyml.la sh-3.2#
Thanks,
Fernando
On 10/30/07, David Matthews < David.Matthews@prolingua.co.uk> wrote: Fernando Costa wrote:
I've been trying to get Isabelle in my macbook and I've joined their discussion list for support. They told me intel macbooks wont
work with the
modified polyml_ppc_darwin, and sent me a patch to get it working
with
Polyml 5.0. I tried both Polyml 5.0 and the one from the top SVN
tree, and
when I try to compile I get the same error:
/bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H
-I. -I..
-DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c -o
machoexport.lo
machoexport.cpp g++ -DHAVE_CONFIG_H -I. -I.. -DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/
machoexport.Tpo -c
machoexport.cpp -fno-common -DPIC -o .libs/machoexport.o machoexport.h:49: error: 'uint' has not been declared machoexport.h:49: error: 'uint' has not been declared machoexport.h :49: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared
I don't know why uint has been used here since it doesn't exactly correspond to the types needed for the nlist struct. I've changed it (in CVS) to use unsigned char and unsigned long so this should be fixed.
David. _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
<polyml5.info> <polyml5.patch> _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
sh-3.2# otool -L /sw/bin/poly /sw/bin/poly: /sw/lib/libpolyml-5.dylib (compatibility version 0.0.0, current version 0.0.0) /sw/lib/libXm.3.dylib (compatibility version 4.0.0, current version 4.1.0) /usr/X11/lib/libXmu.6.dylib (compatibility version 9.0.0, current version 9.0.0) /usr/X11/lib/libXp.6.dylib (compatibility version 9.0.0, current version 9.0.0) /usr/X11/lib/libXext.6.dylib (compatibility version 11.0.0, current version 11.0.0) /usr/X11/lib/libXt.6.dylib (compatibility version 7.0.0, current version 7.0.0) /usr/X11/lib/libSM.6.dylib (compatibility version 7.0.0, current version 7.0.0) /usr/X11/lib/libICE.6.dylib (compatibility version 10.0.0, current version 10.0.0) /usr/X11/lib/libX11.6.dylib (compatibility version 9.0.0, current version 9.0.0) /usr/X11/lib/libXau.6.dylib (compatibility version 7.0.0, current version 7.0.0) /usr/X11/lib/libXdmcp.6.dylib (compatibility version 7.0.0, current version 7.0.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 111.0.0) /usr/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.4.0) /usr/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0) sh-3.2# poly
The exported object file does not match this version of the library sh-3.2#
On 10/30/07, John Ridgway john@jacelridge.com wrote:
What does otool -L /sw/bin/poly report?
Peace
- John
On Oct 30, 2007, at 8:15 PM, Fernando Costa wrote:
Hi,
John, that's a very nice package. I'll e-mail people from Fink asking them to include your package.
The reason I'm having the uint issue, is probably related to Leopard. I've created a patch inside Fink in order to apply David fix (attached).
Although I was able to get the package installed just fine with fink, I still get this:
sh-3.2# /sw/bin/poly
The exported object file does not match this version of the library sh-3.2#
I'm guessing this is Leopard related, here are my libs:
sh-3.2# find / |grep libpoly /sw/fink/10.4/unstable/main/finkinfo/sci/libpolyxmass10.info /sw/fink/10.4/unstable/main/finkinfo/sci/libpolyxmass10.patch /sw/lib/libpolymain.a /sw/lib/libpolymain.la /sw/lib/libpolyml- 5.0.0.dylib /sw/lib/libpolyml-5.0.dylib /sw/lib/libpolyml-5.dylib /sw/lib/libpolyml.a /sw/lib/libpolyml.dylib /sw/lib/libpolyml.la
sh-3.2#
Thanks,
Fernando
On 10/30/07, David Matthews < David.Matthews@prolingua.co.uk> wrote:
Fernando Costa wrote:
I've been trying to get Isabelle in my macbook and I've joined their discussion list for support. They told me intel macbooks wont work with the modified polyml_ppc_darwin, and sent me a patch to get it working with Polyml 5.0. I tried both Polyml 5.0 and the one from the top SVN tree, and when I try to compile I get the same error:
/bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I.. -DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c -o machoexport.lo machoexport.cpp g++ -DHAVE_CONFIG_H -I. -I.. -DMACOSX -Wall -I/usr/X11/include -O3 -I/usr/X11/include -MT machoexport.lo -MD -MP -MF .deps/machoexport.Tpo -c machoexport.cpp -fno-common -DPIC -o .libs/machoexport.o machoexport.h:49: error: 'uint' has not been declared machoexport.h:49: error: 'uint' has not been declared machoexport.h :49: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared machoexport.cpp:241: error: 'uint' has not been declared
I don't know why uint has been used here since it doesn't exactly correspond to the types needed for the nlist struct. I've changed it (in CVS) to use unsigned char and unsigned long so this should be fixed.
David. _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
<polyml5.info> <polyml5.patch>_______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
-
cusquinho＠gmail.com -
David.Matthews＠prolingua.co.uk -
itz＠madbat.mine.nu -
john＠jacelridge.com