Admin/polyml/README
author wenzelm
Fri, 28 Feb 2020 21:34:04 +0100
changeset 71706 a296d3697e50
parent 71358 625df1eb7873
child 72233 a7e6ac2dfa58
permissions -rw-r--r--
updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
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
71184
38ade730f6df updated to polyml-5.8.1-20191101 test version;
wenzelm
parents: 70084
diff changeset
     4
This test version of Poly/ML pre-5.8.1 is based on the repository
71706
a296d3697e50 updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
wenzelm
parents: 71358
diff changeset
     5
snapshot https://github.com/polyml/polyml/commit/6025c250b4f1
57689
e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes;
wenzelm
parents: 56958
diff changeset
     6
70084
63721ee8c86c updated to polyml-5.8 (official release);
wenzelm
parents: 70052
diff changeset
     7
The Isabelle repository provides an administrative tool "isabelle
63721ee8c86c updated to polyml-5.8 (official release);
wenzelm
parents: 70052
diff changeset
     8
build_polyml", which can be used in the polyml component directory as
69720
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
71706
a296d3697e50 updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
wenzelm
parents: 71358
diff changeset
    16
* macOS:
67595
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
71706
a296d3697e50 updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
wenzelm
parents: 71358
diff changeset
    27
Building libgmp on macOS
a296d3697e50 updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
wenzelm
parents: 71358
diff changeset
    28
========================
67589
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
71706
a296d3697e50 updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
wenzelm
parents: 71358
diff changeset
    31
Arithmetic Library (libgmp), but that is not available on macOS by default.
67593
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
69720
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
71706
a296d3697e50 updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
wenzelm
parents: 71358
diff changeset
    50
        28-Feb-2020