Admin/polyml/README
changeset 67589 085f5c2e11f7
parent 67583 c933a5d4e1ee
child 67593 5efb88c90051
--- a/Admin/polyml/README	Sat Feb 10 11:55:12 2018 +0100
+++ b/Admin/polyml/README	Sat Feb 10 12:20:18 2018 +0100
@@ -19,18 +19,35 @@
 
 * Mac OS X:
 
-  $ isabelle build_polyml -m32 -s sha1 src --without-gmp
+  $ isabelle build_polyml -m32 -s sha1 src --with-gmp
   $ isabelle build_polyml -m64 -s sha1 src --with-gmp
 
-  The latter is based on libgmp for x86_64-darwin:
+
+Building libgmp on Mac OS X
+===========================
+
+The GNU Multiple Precision Arithmetic Library is not included in Mac OS X
+by default, but it can be built from sources as follows.
+
+* Download:
+
+  $ curl https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz | xz -dc | tar xf -
+  $ cd gmp-6.1.2
 
-  curl https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz | xz -dc | tar xf -
-  cd gmp-6.1.2
-  ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
-  make
-  make check
-  make install
+* build x86-darwin:
+
+  $ make distclean
+  $ env ABI=32 ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)" --libdir=/usr/local/lib32
+  $ make && make check
+  $ sudo make install
+
+* build x86_64-darwin:
+
+  $ make distclean
+  $ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
+  $ make && make check
+  $ sudo make install
 
 
         Makarius
-        09-Feb-2018
+        10-Feb-2018