1Poly/ML for Isabelle 2==================== 3 4This compilation of Poly/ML 5.7.1 (http://www.polyml.org) is based on the 5source distribution from https://github.com/polyml/polyml/commits/fixes-5.7.1 6up to commit b3d1ff33a4b4. 7 8The Isabelle repository provides the administrative tool "build_polyml", 9which can be used in the polyml component directory as follows. 10 11* Linux: 12 13 $ isabelle build_polyml -m32 -s sha1 src 14 $ isabelle build_polyml -m64 -s sha1 src 15 16* Mac OS X: 17 18 $ isabelle build_polyml -m32 -s sha1 src 19 $ isabelle build_polyml -m64 -s sha1 src 20 21* Windows (Cygwin shell) 22 23 $ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src 24 $ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src 25 26 27Building libgmp on Mac OS X 28=========================== 29 30The build_polyml invocations above implicitly use the GNU Multiple Precision 31Arithmetic Library (libgmp), but that is not available on Mac OS X by default. 32Appending "--without-gmp" to the command-line omits this library. Building 33libgmp properly from sources works as follows (library headers and binaries 34will be placed in /usr/local). 35 36* Download: 37 38 $ curl https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz | xz -dc | tar xf - 39 $ cd gmp-6.1.2 40 41* build x86-darwin: 42 43 $ make distclean 44 $ env ABI=32 ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)" --libdir=/usr/local/lib32 45 $ make && make check 46 $ sudo make install 47 48* build x86_64-darwin: 49 50 $ make distclean 51 $ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)" 52 $ make && make check 53 $ sudo make install 54 55 56 Makarius 57 28-Jul-2018 58