Admin/polyml/README
author wenzelm
Sun, 11 Feb 2018 13:13:03 +0100
changeset 67595 5b4dd7a5b882
parent 67593 5efb88c90051
child 68473 1b8457cc4de8
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38469
5c6c5d63f3c3 updated for prospective Poly/ML 5.4;
wenzelm
parents: 37122
diff changeset
     1
Poly/ML for Isabelle
5c6c5d63f3c3 updated for prospective Poly/ML 5.4;
wenzelm
parents: 37122
diff changeset
     2
====================
27012
e6229d8d6aaa moved README-polyml to polyml/README;
wenzelm
parents:
diff changeset
     3
67099
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 65805
diff changeset
     4
This compilation of Poly/ML 5.7.1 (http://www.polyml.org) is based on the
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 65805
diff changeset
     5
source distribution from https://github.com/polyml/polyml/releases/tag/v5.7.1
57689
e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes;
wenzelm
parents: 56958
diff changeset
     6
65805
d3c5898f1a5e updated to polyml-5.7 for testing (not yet ready for production use);
wenzelm
parents: 65032
diff changeset
     7
The Isabelle repository provides the administrative tool "build_polyml",
d3c5898f1a5e updated to polyml-5.7 for testing (not yet ready for production use);
wenzelm
parents: 65032
diff changeset
     8
which can be used in the polyml component directory as follows.
62281
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged;
wenzelm
parents: 62252
diff changeset
     9
64544
d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents: 62281
diff changeset
    10
* Linux:
62281
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged;
wenzelm
parents: 62252
diff changeset
    11
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    12
  $ isabelle build_polyml -m32 -s sha1 src
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    13
  $ isabelle build_polyml -m64 -s sha1 src
62281
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged;
wenzelm
parents: 62252
diff changeset
    14
67595
wenzelm
parents: 67593
diff changeset
    15
* Mac OS X:
wenzelm
parents: 67593
diff changeset
    16
wenzelm
parents: 67593
diff changeset
    17
  $ isabelle build_polyml -m32 -s sha1 src
wenzelm
parents: 67593
diff changeset
    18
  $ isabelle build_polyml -m64 -s sha1 src
wenzelm
parents: 67593
diff changeset
    19
64544
d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents: 62281
diff changeset
    20
* Windows (Cygwin shell)
d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents: 62281
diff changeset
    21
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    22
  $ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    23
  $ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src
41331
wenzelm
parents: 41330
diff changeset
    24
67589
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    25
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    26
Building libgmp on Mac OS X
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    27
===========================
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    28
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    29
The build_polyml invocations above implicitly use the GNU Multiple Precision
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    30
Arithmetic Library (libgmp), but that is not available on Mac OS X by default.
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    31
Appending "--without-gmp" to the command-line omits this library. Building
67595
wenzelm
parents: 67593
diff changeset
    32
libgmp properly from sources works as follows (library headers and binaries
wenzelm
parents: 67593
diff changeset
    33
will be placed in /usr/local).
67589
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    34
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    35
* Download:
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    36
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    37
  $ curl https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz | xz -dc | tar xf -
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    38
  $ cd gmp-6.1.2
67583
c933a5d4e1ee support for libgmp for x86_64-darwin;
wenzelm
parents: 67099
diff changeset
    39
67589
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    40
* build x86-darwin:
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    41
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    42
  $ make distclean
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    43
  $ env ABI=32 ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)" --libdir=/usr/local/lib32
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    44
  $ make && make check
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    45
  $ sudo make install
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    46
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    47
* build x86_64-darwin:
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    48
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    49
  $ make distclean
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    50
  $ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    51
  $ make && make check
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    52
  $ sudo make install
67583
c933a5d4e1ee support for libgmp for x86_64-darwin;
wenzelm
parents: 67099
diff changeset
    53
41331
wenzelm
parents: 41330
diff changeset
    54
57689
e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes;
wenzelm
parents: 56958
diff changeset
    55
        Makarius
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    56
        11-Feb-2018