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