I have just recently updated my MacBook Pro from Snow Leopard to Lion (Mac OS X 10.7), and now I am regretting it.
Poly/ML has stopped working for building the HOL theorem prover. When I try to run the configuration script for HOL using my current version of Poly/ML, I see
. . . Making tools/mllex/mllex.exe. Poly/ML 5.3 Release
# ld: library not found for -lcrt1.10.6.o
collect2: ld returned 1 exit status Failed to build mllex.
In fact this library was present in prior versions of Mac OS X, like 10.6, but is not present in 10.7.
So I tried downloading and building the current version of Poly/ML, 5.4.1. I have the current version of the Developer tools, Xcode version 4.1 for Lion. When trying ./configure I see
-bash-3.2$ ./configure checking for a BSD-compatible install... /usr/bin/install -c checking whether build environment is sane... yes checking for a thread-safe mkdir -p... ./install-sh -c -d checking for gawk... no checking for mawk... no checking for nawk... no checking for awk... awk checking whether make sets $(MAKE)... yes checking build system type... x86_64-apple-darwin11.0.0 checking host system type... x86_64-apple-darwin11.0.0 checking for style of include used by make... GNU checking for gcc... gcc checking whether the C compiler works... no configure: error: in `/Users/palantir/sml/polyml/polyml.5.4.1': configure: error: C compiler cannot create executables See `config.log' for more details
When I look at the end of the config.log file, I see
## ----------- ## ## confdefs.h. ## ## ----------- ##
/* confdefs.h */ #define PACKAGE_NAME "Poly/ML" #define PACKAGE_TARNAME "polyml" #define PACKAGE_VERSION "5.4" #define PACKAGE_STRING "Poly/ML 5.4" #define PACKAGE_BUGREPORT "polyml AT polyml DOT org" #define PACKAGE_URL "" #define PACKAGE "polyml" #define VERSION "5.4"
configure: exit 77
Are there any suggestions on how to get Poly/ML working under Lion?
Thanks.
Peter V. Homeier