Admin/polyml/README
author haftmann
Fri, 14 Jun 2019 08:34:27 +0000
changeset 70335 9bd8c16b6627
parent 69903 63721ee8c86c
child 70988 38ade730f6df
permissions -rw-r--r--
using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
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
69903
63721ee8c86c updated to polyml-5.8 (official release);
wenzelm
parents: 69871
diff changeset
     4
This compilation of Poly/ML 5.8 (https://www.polyml.org) is based on the
63721ee8c86c updated to polyml-5.8 (official release);
wenzelm
parents: 69871
diff changeset
     5
source distribution from https://github.com/polyml/polyml/releases/tag/v5.8
57689
e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes;
wenzelm
parents: 56958
diff changeset
     6
69903
63721ee8c86c updated to polyml-5.8 (official release);
wenzelm
parents: 69871
diff changeset
     7
The Isabelle repository provides an administrative tool "isabelle
63721ee8c86c updated to polyml-5.8 (official release);
wenzelm
parents: 69871
diff changeset
     8
build_polyml", which can be used in the polyml component directory as
69704
3fb94d9b87b0 updated polyml platform: 32=x86_64_32;
wenzelm
parents: 68702
diff changeset
     9
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
    10
64544
d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents: 62281
diff changeset
    11
* 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
    12
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    13
  $ isabelle build_polyml -m32 -s sha1 src
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    14
  $ 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
    15
67595
wenzelm
parents: 67593
diff changeset
    16
* Mac OS X:
wenzelm
parents: 67593
diff changeset
    17
wenzelm
parents: 67593
diff changeset
    18
  $ isabelle build_polyml -m32 -s sha1 src
wenzelm
parents: 67593
diff changeset
    19
  $ isabelle build_polyml -m64 -s sha1 src
wenzelm
parents: 67593
diff changeset
    20
64544
d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents: 62281
diff changeset
    21
* Windows (Cygwin shell)
d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents: 62281
diff changeset
    22
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    23
  $ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    24
  $ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src
41331
wenzelm
parents: 41330
diff changeset
    25
67589
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    26
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    27
Building libgmp on Mac OS X
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    28
===========================
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    29
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    30
The build_polyml invocations above implicitly use the GNU Multiple Precision
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    31
Arithmetic Library (libgmp), but that is not available on Mac OS X by default.
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    32
Appending "--without-gmp" to the command-line omits this library. Building
67595
wenzelm
parents: 67593
diff changeset
    33
libgmp properly from sources works as follows (library headers and binaries
wenzelm
parents: 67593
diff changeset
    34
will be placed in /usr/local).
67589
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    35
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    36
* Download:
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    37
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    38
  $ 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
    39
  $ cd gmp-6.1.2
67583
c933a5d4e1ee support for libgmp for x86_64-darwin;
wenzelm
parents: 67099
diff changeset
    40
69704
3fb94d9b87b0 updated polyml platform: 32=x86_64_32;
wenzelm
parents: 68702
diff changeset
    41
* build:
67589
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    42
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    43
  $ make distclean
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    44
  $ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    45
  $ make && make check
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    46
  $ sudo make install
67583
c933a5d4e1ee support for libgmp for x86_64-darwin;
wenzelm
parents: 67099
diff changeset
    47
41331
wenzelm
parents: 41330
diff changeset
    48
57689
e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes;
wenzelm
parents: 56958
diff changeset
    49
        Makarius
69903
63721ee8c86c updated to polyml-5.8 (official release);
wenzelm
parents: 69871
diff changeset
    50
        12-Mar-2019