Admin/polyml/README
author wenzelm
Sun May 13 20:24:33 2018 +0200 (15 months ago)
changeset 68172 0f14cf9c632f
parent 67595 5b4dd7a5b882
child 68473 1b8457cc4de8
permissions -rw-r--r--
more concise information;
wenzelm@38469
     1
Poly/ML for Isabelle
wenzelm@38469
     2
====================
wenzelm@27012
     3
wenzelm@67099
     4
This compilation of Poly/ML 5.7.1 (http://www.polyml.org) is based on the
wenzelm@67099
     5
source distribution from https://github.com/polyml/polyml/releases/tag/v5.7.1
wenzelm@57689
     6
wenzelm@65805
     7
The Isabelle repository provides the administrative tool "build_polyml",
wenzelm@65805
     8
which can be used in the polyml component directory as follows.
wenzelm@62281
     9
wenzelm@64544
    10
* Linux:
wenzelm@62281
    11
wenzelm@67593
    12
  $ isabelle build_polyml -m32 -s sha1 src
wenzelm@67593
    13
  $ isabelle build_polyml -m64 -s sha1 src
wenzelm@62281
    14
wenzelm@67595
    15
* Mac OS X:
wenzelm@67595
    16
wenzelm@67595
    17
  $ isabelle build_polyml -m32 -s sha1 src
wenzelm@67595
    18
  $ isabelle build_polyml -m64 -s sha1 src
wenzelm@67595
    19
wenzelm@64544
    20
* Windows (Cygwin shell)
wenzelm@64544
    21
wenzelm@67593
    22
  $ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src
wenzelm@67593
    23
  $ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src
wenzelm@41331
    24
wenzelm@67589
    25
wenzelm@67589
    26
Building libgmp on Mac OS X
wenzelm@67589
    27
===========================
wenzelm@67589
    28
wenzelm@67593
    29
The build_polyml invocations above implicitly use the GNU Multiple Precision
wenzelm@67593
    30
Arithmetic Library (libgmp), but that is not available on Mac OS X by default.
wenzelm@67593
    31
Appending "--without-gmp" to the command-line omits this library. Building
wenzelm@67595
    32
libgmp properly from sources works as follows (library headers and binaries
wenzelm@67595
    33
will be placed in /usr/local).
wenzelm@67589
    34
wenzelm@67589
    35
* Download:
wenzelm@67589
    36
wenzelm@67589
    37
  $ curl https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz | xz -dc | tar xf -
wenzelm@67589
    38
  $ cd gmp-6.1.2
wenzelm@67583
    39
wenzelm@67589
    40
* build x86-darwin:
wenzelm@67589
    41
wenzelm@67589
    42
  $ make distclean
wenzelm@67589
    43
  $ env ABI=32 ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)" --libdir=/usr/local/lib32
wenzelm@67589
    44
  $ make && make check
wenzelm@67589
    45
  $ sudo make install
wenzelm@67589
    46
wenzelm@67589
    47
* build x86_64-darwin:
wenzelm@67589
    48
wenzelm@67589
    49
  $ make distclean
wenzelm@67589
    50
  $ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
wenzelm@67589
    51
  $ make && make check
wenzelm@67589
    52
  $ sudo make install
wenzelm@67583
    53
wenzelm@41331
    54
wenzelm@57689
    55
        Makarius
wenzelm@67593
    56
        11-Feb-2018