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
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
