My first attempt to compile Poly/ML 5.2.1 on Snow Leopard (= MacOS X 10.6) resulted in an error due to a cast of a pointer to an int in libpolyml/x86_dep.cpp. There is a fix for this in the latest source, but the build then falls over as follows:
... g++ -DHAVE_CONFIG_H -I. -I.. -DMACOSX -Wall -O3 -MT x86_dep.lo -MD -MP -MF .deps/x86_dep.Tpo -c x86_dep.cpp -fno-common -DPIC -o .libs/x86_dep.o /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:1063:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:1774:Incorrect register `%rsi' used with `l' suffix /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:1968:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:1973:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:2097:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:2129:Incorrect register `%rsi' used with `l' suffix /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:2416:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4660:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4666:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4672:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4696:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4702:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4738:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4759:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4777:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4780:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4783:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4789:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4792:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4795:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4798:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4801:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4804:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4807:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4819:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4822:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4891:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4894:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4897:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4900:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4903:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4906:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4909:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4912:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4915:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4924:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4927:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4936:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4939:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4978:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4981:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4984:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4987:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4990:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4992:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4994:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4996:suffix or operands invalid for `pop' /var/folders/Ih/IhQgyfokGpO8Wx1qsxaKZ++++TI/-Tmp-//ccWgMIs0.s:4998:suffix or operands invalid for `pop' make[2]: *** [x86_dep.lo] Error 1 make[1]: *** [all-recursive] Error 1 make: *** [all] Error 2
Any suggestions gratefully received.
Regards,
Rob.
rda@lemma-one.com wrote:
My first attempt to compile Poly/ML 5.2.1 on Snow Leopard (= MacOS X 10.6) resulted in an error due to a cast of a pointer to an int in libpolyml/x86_dep.cpp. There is a fix for this in the latest source, but the build then falls over as follows:
Rob, I had an email about this from Peter Homeier. Since I don't have access to a machine running this I can't test it directly. My feeling is that it is building the 64-bit version by default. Try grep SIZEOF_VOIDP config.h and see what it says. I have managed to build the 64-bit version on an older version of Mac OS X with the following: ./configure --build=x86_64-darwin CFLAGS='-arch x86_64 -O3' \ CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64' \ LDFLAGS='-segprot POLY rwx rwx'
This may work on 10.6. If so, some of the arguments may not actually be necessary and I'd like to know exactly which. I would expect that the CFLAGS, CXXFLAGS and CCASFLAGS can all be omitted if it is defaulting to 64-bit anyway. The LDFLAGS wasn't needed for the build itself but without it the resulting poly executable would SEGFAULT as soon as it was run. The problem was that the linker was ignoring the access rights in the object file itself and removing execute permission. This doesn't have any effect in 32-bit mode but in 64-bit mode it seems the processor was respecting the no-execute flag and failing. If this is needed it will have to be provided on any link step with your own code.
It may be possible to force 32-bit mode with ./configure CFLAGS='-arch i386 -O3' CXXFLAGS='-arch i386 -O3' \ CCASFLAGS='-arch i386'
Regards, David
David,
Thanks for that.
If I do:
./configure --build=x86_64-darwin
then make works, but make cvs then fails like this:
make all-recursive Making all in libpolyml make[2]: Nothing to be done for `all'. Making all in libpolymain make[2]: Nothing to be done for `all'. make[2]: Nothing to be done for `all-am'. ./poly -H 10 < mlsource/BuildExport.sml /bin/sh: line 1: 18804 Bus error ./poly -H 10 < mlsource/BuildExport.sml make: *** [compiler] Error 138
If I do:
./configure --build=x86_64-darwin LDFLAGS='-segprot POLY rwx rwx'
then everything works (but as you predict I also have to put -segprot POLY rwx rwx in the steps in my make files that link a poly program.
If I do:
./configure CFLAGS='-arch i386'
It fails on x86_dep.lo just as it does with no extra settings.
Regards,
Rob.
rda@lemma-one.com wrote:
My first attempt to compile Poly/ML 5.2.1 on Snow Leopard (= MacOS X 10.6) resulted in an error due to a cast of a pointer to an int in libpolyml/x86_dep.cpp. There is a fix for this in the latest source, but the build then falls over as follows:
Rob, I had an email about this from Peter Homeier. Since I don't have access to a machine running this I can't test it directly. My feeling is that it is building the 64-bit version by default. Try grep SIZEOF_VOIDP config.h and see what it says. I have managed to build the 64-bit version on an older version of Mac OS X with the following: ./configure --build=x86_64-darwin CFLAGS='-arch x86_64 -O3' \ CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64' \ LDFLAGS='-segprot POLY rwx rwx'
This may work on 10.6. If so, some of the arguments may not actually be necessary and I'd like to know exactly which. I would expect that the CFLAGS, CXXFLAGS and CCASFLAGS can all be omitted if it is defaulting to 64-bit anyway. The LDFLAGS wasn't needed for the build itself but without it the resulting poly executable would SEGFAULT as soon as it was run. The problem was that the linker was ignoring the access rights in the object file itself and removing execute permission. This doesn't have any effect in 32-bit mode but in 64-bit mode it seems the processor was respecting the no-execute flag and failing. If this is needed it will have to be provided on any link step with your own code.
It may be possible to force 32-bit mode with ./configure CFLAGS='-arch i386 -O3' CXXFLAGS='-arch i386 -O3' \ CCASFLAGS='-arch i386'
Regards, David
Rob,
rda@lemma-one.com wrote:
If I do:
./configure --build=x86_64-darwin
then make works, but make cvs then fails like this:
make all-recursive Making all in libpolyml make[2]: Nothing to be done for `all'. Making all in libpolymain make[2]: Nothing to be done for `all'. make[2]: Nothing to be done for `all-am'. ./poly -H 10 < mlsource/BuildExport.sml /bin/sh: line 1: 18804 Bus error ./poly -H 10 < mlsource/BuildExport.sml make: *** [compiler] Error 138
./configure --build=x86_64-darwin LDFLAGS='-segprot POLY rwx rwx'
then everything works (but as you predict I also have to put -segprot POLY rwx rwx in the steps in my make files that link a poly program.
OK, that confirms what I found on the older version of Mac OS X; the linker is removing the execute bit from the POLY segment and it needs to be explicitly set. I'll update the configure/Make files to add this for the Poly/ML build.
If I do:
./configure CFLAGS='-arch i386'
It fails on x86_dep.lo just as it does with no extra settings.
It may be possible to force 32-bit mode with ./configure CFLAGS='-arch i386 -O3' CXXFLAGS='-arch i386 -O3' \ CCASFLAGS='-arch i386'
Did you try with the CXXFLAGS option as well? From what I can tell CFLAGS is only used in C programs not in the C++ parts such as x86_dep.cpp.
Regards, David
Just a further update on this: the problem seems to be the config.guess script which reports that this is a 32-bit processor rather than a 64-bit one. I've updated to the latest version from the master version at git.savannah.gnu.org but I'm not sure that this fixes it. I came across a proposed patch to this in a GCC mailing list archive http://www.mail-archive.com/gcc-bugs@gcc.gnu.org/msg263541.html which hasn't made it into the master yet. I've added this in so I'd be interested to know if it works. To see what it's reporting now run sh config.guess in the polyml directory.
I've also added the -segprot option so hopefully it will all build on Mac OS X 10.6 without any special options.
David
I have had some luck with the following approach:
First, download the current developer (svn) source version of Poly/ML, freshly, as described on http://www.polyml.org/download.html. Then
./configure --build=x86_64-darwin LDFLAGS='-segprot POLY rwx rwx' make make cvs make sudo make install
This mostly seemed to work, except that the "make cvs" seemed not to do anything... I had not done a "make distclean" before the ./configure.
Attempting to use Poly/ML to build the HOL4 theorem prover, I then found that the following change was needed to the file <main HOL4 dir>/tools-poly/configure.sml: change line 51 as follows:
51c51 < "-lpolymain", "-lpolyml"]; ---
"-lpolymain", "-lpolyml", "-segprot", "POLY", "rwx", "rwx"];
This allows the build of HOL4 to begin. However, this later fails for some reason when trying to build the HolSat library:
. . . Analysing satScript.sml Compiling satScript.sml Linking satScript.uo to produce theory-builder executable /Users/palantir/hol/hol-omega/src/HolSat/satScript: line 7: 5860 Bus error /Users/palantir/hol/hol-omega/bin/hol.builder0 <<'__end-of-file__' val _ = PolyML.Compiler.prompt1:=""; val _ = PolyML.Compiler.prompt2:=""; val _ = PolyML.print_depth 0; val _ = List.map load ["holmake_not_interactive","satScript"] handle x => ((case x of Fail s => print (s^"\n") | _ => ()); OS.Process.exit OS.Process.failure); __end-of-file__
Build failed in directory /Users/palantir/hol/hol-omega/src/HolSat
David Matthews has said
It would appear that the Mac OS X linker will require the LDFLAGS="-segprot POLY rwx rwx' option whenever an executable file is built using an exported Poly object file.
Perhaps some other element of the build program for building HOL4 needs this option.
I also tried, after the normal build failed as above, running "Holmake" directly in the src/HolSat directory, with the following results:
$ Holmake Compiling satScript.sml Linking satScript.uo to produce theory-builder executable dyld: Library not loaded: /usr/local/lib/libpolyml.1.dylib Referenced from: /Users/palantir/hol/hol-omega/bin/hol.builder Reason: no suitable image found. Did find: /usr/local/lib/libpolyml.1.dylib: mach-o, but wrong architecture /usr/local/lib/libpolyml.1.dylib: mach-o, but wrong architecture /usr/local/lib/libpolyml.1.dylib: mach-o, but wrong architecture /Users/palantir/hol/hol-omega/src/HolSat/satScript: line 7: 6000 Trace/BPT trap /Users/palantir/hol/hol-omega/bin/hol.builder <<'__end-of-file__' val _ = PolyML.Compiler.prompt1:=""; val _ = PolyML.Compiler.prompt2:=""; val _ = PolyML.print_depth 0; val _ = List.map load ["holmake_not_interactive","holmakebuild","satScript"] handle x => ((case x of Fail s => print (s^"\n") | _ => ()); OS.Process.exit OS.Process.failure); __end-of-file__
Any suggestions?
Peter
-
David.Matthews＠prolingua.co.uk -
palantir＠trustworthytools.com -
rda＠lemma-one.com