Dear Poly/ML enthusiasts and experts of the gcc toolchain on macOS,
building Poly/ML with libgmp has always been a challenge, but I have now managed as follows for x86_64-darwin.
The approach works as follows:
(1) Build libgmp from sources. (2) Build Poly/ML --with-gmp using that homemade version. (3) Copy libgmp.10.dylib into the Poly/ML lib directory and adjust locations with install_name_tool
Afterwards it is possible to copy the resulting Poly/ML target directory to a different location on a different machine, with a different (newer) macOS version.
The details are in the included build.txt (e.g. for macOS 10.12 Sierra). This is not a shell script! It should be run carefully line-by-line. Towards the end there are two install_name_tool invocations with locations determined beforehand by "otool -L". The final "otool -L" is just a sanity check, the result is like this:
target/bin/poly: @executable_path/../lib/libpolyml.9.dylib (compatibility version 10.0.0, current version 10.0.0) @executable_path/../lib/libgmp.10.dylib (compatibility version 14.0.0, current version 14.2.0) /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 307.4.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1238.0.0)
This setup is already part of "isabelle build_polyml", see http://isabelle.in.tum.de/repos/isabelle/file/8b19a8a7f029/src/Pure/Admin/bu... -- but that assumes that libgmp has been installed in a standard place (e.g. /usr/local/lib).
I wonder if anybody has managed to build libgmp for x86-darwin (32bit) platform. That platform variant still provides better performance for big applications like Isabelle, because it requires only half the memory.
Makarius
Hello. I build PolyML with libgmp on FreeBSD by help env CFLAGS=-I/usr/local/include LDFLAGS=-L/usr/local/lib ./configure --with-gmp && make
If my c compiler is clang, I remove AC_CHECK_LIB(stdc++, main) from configure.ac and run autoreconf -fi before configure
2018-02-10 0:06 GMT+02:00 Makarius <makarius at sketis.net>:
Dear Poly/ML enthusiasts and experts of the gcc toolchain on macOS,
building Poly/ML with libgmp has always been a challenge, but I have now managed as follows for x86_64-darwin.
The approach works as follows:
(1) Build libgmp from sources. (2) Build Poly/ML --with-gmp using that homemade version. (3) Copy libgmp.10.dylib into the Poly/ML lib directory and adjust locations with install_name_tool
Afterwards it is possible to copy the resulting Poly/ML target directory to a different location on a different machine, with a different (newer) macOS version.
The details are in the included build.txt (e.g. for macOS 10.12 Sierra). This is not a shell script! It should be run carefully line-by-line. Towards the end there are two install_name_tool invocations with locations determined beforehand by "otool -L". The final "otool -L" is just a sanity check, the result is like this:
target/bin/poly: @executable_path/../lib/libpolyml.9.dylib (compatibility version 10.0.0, current version 10.0.0) @executable_path/../lib/libgmp.10.dylib (compatibility version 14.0.0, current version 14.2.0) /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 307.4.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1238.0.0)
This setup is already part of "isabelle build_polyml", see http://isabelle.in.tum.de/repos/isabelle/file/8b19a8a7f029/src/Pure/Admin/bu... -- but that assumes that libgmp has been installed in a standard place (e.g. /usr/local/lib).
I wonder if anybody has managed to build libgmp for x86-darwin (32bit) platform. That platform variant still provides better performance for big applications like Isabelle, because it requires only half the memory.
Makarius
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Hi Makarius,
I could build libgmp 6.1.2 for i386 on macOS Sierra by first setting the shell variable ABI to 32, then proceed as usual (configure, make, ..):
??? file build/intel-pc/lib/libgmp.10.dylib ??? build/intel-pc/lib/libgmp.10.dylib: Mach-O dynamically linked shared library i386
? Bernard.
On 09/02/2018 23:06, Makarius wrote:
I wonder if anybody has managed to build libgmp for x86-darwin (32bit) platform. That platform variant still provides better performance for big applications like Isabelle, because it requires only half the memory.
Makarius
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 10/02/18 07:33, Bernard Berthomieu wrote:
I could build libgmp 6.1.2 for i386 on macOS Sierra by first setting the shell variable ABI to 32, then proceed as usual (configure, make, ..):
Great, that was the key hint. I have now managed to build libgmp for x86-darwin as follows:
env ABI=32 ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)" --libdir=/usr/local/lib32
For the Poly/ML build I merely include -L/usr/local/lib32 in LDFLAGS; the header files are implicitly taken from /usr/local/include (i.e. from the default installation location of libgmp for x86_64-darwin).
See also the full story in http://isabelle.in.tum.de/repos/isabelle/file/4fb9cbe10f3e/Admin/polyml/READ...
Makarius
Makarius, were you saying that building Poly/ML with libgmp *at all* has been a challenge? Or specifically building a portable Poly/ML with libgmp? I have never had a problem building Poly/ML on macOS using a MacPorts-installed libgmp:
CFLAGS="-I /opt/local/include -L/opt/local/lib" CXXFLAGS="-I /opt/local/include -L/opt/local/lib" LDFLAGS="-L/opt/local/lib" ./configure make
I don?t know what the scenario is for Homebrew users, but I imagine it would be similar. For a long time I didn?t pay much attention to macOS questions, not having a Mac myself and after ending up with one I just assumed the cryptic flags juggling was common knowledge. Apologies if I was mistaken.
The above steps are probably not suitable for building a portable Poly/ML. If you?re building libgmp from source maybe you want to try building a static library (-disable-shared to the libgmp build system)? I have not tried this, but they claim it works [0].
[0]: https://gmplib.org/manual/Known-Build-Problems.html#index-MacOS-X
On Feb 9, 2018, at 14:06, Makarius <makarius at sketis.net> wrote:
Dear Poly/ML enthusiasts and experts of the gcc toolchain on macOS,
building Poly/ML with libgmp has always been a challenge, but I have now managed as follows for x86_64-darwin.
The approach works as follows:
(1) Build libgmp from sources. (2) Build Poly/ML --with-gmp using that homemade version. (3) Copy libgmp.10.dylib into the Poly/ML lib directory and adjust locations with install_name_tool
Afterwards it is possible to copy the resulting Poly/ML target directory to a different location on a different machine, with a different (newer) macOS version.
The details are in the included build.txt (e.g. for macOS 10.12 Sierra). This is not a shell script! It should be run carefully line-by-line. Towards the end there are two install_name_tool invocations with locations determined beforehand by "otool -L". The final "otool -L" is just a sanity check, the result is like this:
target/bin/poly: @executable_path/../lib/libpolyml.9.dylib (compatibility version 10.0.0, current version 10.0.0) @executable_path/../lib/libgmp.10.dylib (compatibility version 14.0.0, current version 14.2.0) /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 307.4.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1238.0.0)
This setup is already part of "isabelle build_polyml", see http://isabelle.in.tum.de/repos/isabelle/file/8b19a8a7f029/src/Pure/Admin/bu... -- but that assumes that libgmp has been installed in a standard place (e.g. /usr/local/lib).
I wonder if anybody has managed to build libgmp for x86-darwin (32bit) platform. That platform variant still provides better performance for big applications like Isabelle, because it requires only half the memory.
Makarius <build.txt>_______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
I'm not able to build poly/ML on my Mac, with or without libgmp, for about a year. The funny thing is, it builds fine on my similarly-configured MacBook Pro at home. I've given up trying to figure out why. Upgrading to High Sierra or downloading more recent versions of the sources hasn't changed this. Something in the setup must be very fragile.
ld: symbol(s) not found for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) make[1]: *** [polyimport] Error 1 make: *** [install-recursive] Error 1
I use Homebrew, not macports.
Larry
On 10 Feb 2018, at 07:12, Matthew Fernandez <matthew.fernandez at gmail.com> wrote:
Makarius, were you saying that building Poly/ML with libgmp *at all* has been a challenge? Or specifically building a portable Poly/ML with libgmp? I have never had a problem building Poly/ML on macOS using a MacPorts-installed libgmp:
CFLAGS="-I /opt/local/include -L/opt/local/lib" CXXFLAGS="-I /opt/local/include -L/opt/local/lib" LDFLAGS="-L/opt/local/lib" ./configure make
I don?t know what the scenario is for Homebrew users, but I imagine it would be similar. For a long time I didn?t pay much attention to macOS questions, not having a Mac myself and after ending up with one I just assumed the cryptic flags juggling was common knowledge. Apologies if I was mistaken.
Does the polyml version built on your MacBook run on your other mac ?
? Bernard.
On 12/02/2018 12:45, Lawrence Paulson wrote:
I'm not able to build poly/ML on my Mac, with or without libgmp, for about a year. The funny thing is, it builds fine on my similarly-configured MacBook Pro at home. I've given up trying to figure out why. ?Upgrading to High Sierra or downloading more recent versions of the sources hasn't changed this. Something in the setup must be very fragile.
ld: symbol(s) not found for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) make[1]: *** [polyimport] Error 1 make: *** [install-recursive] Error 1
I use Homebrew, not macports.
Larry
On 10 Feb 2018, at 07:12, Matthew Fernandez <matthew.fernandez at gmail.com <mailto:matthew.fernandez at gmail.com>> wrote:
Makarius, were you saying that building Poly/ML with libgmp *at all* has been a challenge? Or specifically building a portable Poly/ML with libgmp? I have never had a problem building Poly/ML on macOS using a MacPorts-installed libgmp:
???CFLAGS="-I /opt/local/include -L/opt/local/lib" CXXFLAGS="-I /opt/local/include -L/opt/local/lib" LDFLAGS="-L/opt/local/lib" ./configure ???make
I don?t know what the scenario is for Homebrew users, but I imagine it would be similar. For a long time I didn?t pay much attention to macOS questions, not having a Mac myself and after ending up with one I just assumed the cryptic flags juggling was common knowledge. Apologies if I was mistaken.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
It does indeed. I just tried again with the 5.7.1 release. Larry
On 12 Feb 2018, at 17:01, Bernard Berthomieu <Bernard.Berthomieu at laas.fr> wrote:
Does the polyml version built on your MacBook run on your other mac ?
Bernard.
On 12/02/2018 12:45, Lawrence Paulson wrote:
I'm not able to build poly/ML on my Mac, with or without libgmp, for about a year. The funny thing is, it builds fine on my similarly-configured MacBook Pro at home. I've given up trying to figure out why. Upgrading to High Sierra or downloading more recent versions of the sources hasn't changed this. Something in the setup must be very fragile.
ld: symbol(s) not found for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) make[1]: *** [polyimport] Error 1 make: *** [install-recursive] Error 1
I use Homebrew, not macports.
Larry
On 10 Feb 2018, at 07:12, Matthew Fernandez <matthew.fernandez at gmail.com <mailto:matthew.fernandez at gmail.com>> wrote:
Makarius, were you saying that building Poly/ML with libgmp *at all* has been a challenge? Or specifically building a portable Poly/ML with libgmp? I have never had a problem building Poly/ML on macOS using a MacPorts-installed libgmp:
CFLAGS="-I /opt/local/include -L/opt/local/lib" CXXFLAGS="-I /opt/local/include -L/opt/local/lib" LDFLAGS="-L/opt/local/lib" ./configure make
I don?t know what the scenario is for Homebrew users, but I imagine it would be similar. For a long time I didn?t pay much attention to macOS questions, not having a Mac myself and after ending up with one I just assumed the cryptic flags juggling was common knowledge. Apologies if I was mistaken.
polyml mailing list polyml at inf.ed.ac.uk <mailto:polyml at inf.ed.ac.uk> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
-
Bernard.Berthomieu＠laas.fr -
kostirya＠gmail.com -
lp15＠cam.ac.uk -
makarius＠sketis.net -
matthew.fernandez＠gmail.com