1Poly/ML for Isabelle 2==================== 3 4This test version of Poly/ML pre-5.8.1 is based on the repository 5snapshot https://github.com/polyml/polyml/commit/6025c250b4f1 6 7The Isabelle repository provides an administrative tool "isabelle 8build_polyml", which can be used in the polyml component directory as 9follows. 10 11* Linux: 12 13 $ isabelle build_polyml -m32 -s sha1 src 14 $ isabelle build_polyml -m64 -s sha1 src 15 16* macOS: 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 macOS 28======================== 29 30The build_polyml invocations above implicitly use the GNU Multiple Precision 31Arithmetic Library (libgmp), but that is not available on macOS 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: 42 43 $ make distclean 44 $ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)" 45 $ make && make check 46 $ sudo make install 47 48 49 Makarius 50 28-Feb-2020 51