Admin/polyml/README
author wenzelm
Sat, 28 Nov 2020 16:25:29 +0100
changeset 72759 bd5ee3148132
parent 72660 7d4e9f7742c6
child 73643 9b4579e5bced
permissions -rw-r--r--
more antiquotations (reverting 4df341249348);
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
72131
284d6c06cbfb updated to polyml-test-159dc81efc3b;
wenzelm
parents: 72061
diff changeset
     4
This compilation of Poly/ML (http://www.polyml.org) is based on the
284d6c06cbfb updated to polyml-test-159dc81efc3b;
wenzelm
parents: 72061
diff changeset
     5
repository version
72660
7d4e9f7742c6 updated to polyml-test-7e49fce62e3d --- follow current ongoing development;
wenzelm
parents: 72533
diff changeset
     6
https://github.com/polyml/polyml/commit/f86ae3dc1686
57689
e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes;
wenzelm
parents: 56958
diff changeset
     7
69903
63721ee8c86c updated to polyml-5.8 (official release);
wenzelm
parents: 69871
diff changeset
     8
The Isabelle repository provides an administrative tool "isabelle
63721ee8c86c updated to polyml-5.8 (official release);
wenzelm
parents: 69871
diff changeset
     9
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
    10
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
    11
64544
d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents: 62281
diff changeset
    12
* 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
    13
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    14
  $ isabelle build_polyml -m32 -s sha1 src
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    15
  $ 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
    16
71492
a296d3697e50 updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
wenzelm
parents: 71160
diff changeset
    17
* macOS:
67595
wenzelm
parents: 67593
diff changeset
    18
wenzelm
parents: 67593
diff changeset
    19
  $ isabelle build_polyml -m32 -s sha1 src
wenzelm
parents: 67593
diff changeset
    20
  $ isabelle build_polyml -m64 -s sha1 src
wenzelm
parents: 67593
diff changeset
    21
64544
d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents: 62281
diff changeset
    22
* Windows (Cygwin shell)
d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016);
wenzelm
parents: 62281
diff changeset
    23
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    24
  $ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    25
  $ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src
41331
wenzelm
parents: 41330
diff changeset
    26
67589
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    27
71492
a296d3697e50 updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
wenzelm
parents: 71160
diff changeset
    28
Building libgmp on macOS
a296d3697e50 updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
wenzelm
parents: 71160
diff changeset
    29
========================
67589
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    30
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    31
The build_polyml invocations above implicitly use the GNU Multiple Precision
71492
a296d3697e50 updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);
wenzelm
parents: 71160
diff changeset
    32
Arithmetic Library (libgmp), but that is not available on macOS by default.
67593
5efb88c90051 clarified command-line defaults;
wenzelm
parents: 67589
diff changeset
    33
Appending "--without-gmp" to the command-line omits this library. Building
67595
wenzelm
parents: 67593
diff changeset
    34
libgmp properly from sources works as follows (library headers and binaries
wenzelm
parents: 67593
diff changeset
    35
will be placed in /usr/local).
67589
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
* Download:
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    38
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    39
  $ 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
    40
  $ cd gmp-6.1.2
67583
c933a5d4e1ee support for libgmp for x86_64-darwin;
wenzelm
parents: 67099
diff changeset
    41
69704
3fb94d9b87b0 updated polyml platform: 32=x86_64_32;
wenzelm
parents: 68702
diff changeset
    42
* build:
67589
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    43
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    44
  $ make distclean
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    45
  $ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    46
  $ make && make check
085f5c2e11f7 support for libgmp for x86-darwin;
wenzelm
parents: 67583
diff changeset
    47
  $ sudo make install
67583
c933a5d4e1ee support for libgmp for x86_64-darwin;
wenzelm
parents: 67099
diff changeset
    48
41331
wenzelm
parents: 41330
diff changeset
    49
57689
e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes;
wenzelm
parents: 56958
diff changeset
    50
        Makarius
72660
7d4e9f7742c6 updated to polyml-test-7e49fce62e3d --- follow current ongoing development;
wenzelm
parents: 72533
diff changeset
    51
        19-Nov-2020