Admin/polyml/README
changeset 62281 707f9b182f4f
parent 62252 6a87f7b15b69
child 64544 d23b7c9b9dd4
equal deleted inserted replaced
62280:d9cfe5c3815d 62281:707f9b182f4f
     1 Poly/ML for Isabelle
     1 Poly/ML for Isabelle
     2 ====================
     2 ====================
     3 
     3 
     4 This compilation of Poly/ML 5.6 (http://www.polyml.org) is based on the source
     4 This compilation of Poly/ML 5.6 (http://www.polyml.org) is based on the source
     5 distribution from https://github.com/polyml/polyml/releases/tag/v5.6/.
     5 distribution from https://github.com/polyml/polyml/releases/tag/v5.6/.
       
     6 
       
     7 On Linux the sources have changed as follows, in order to evade a
       
     8 potential conflict of /bin/bash versus /bin/sh -> dash (notably on
       
     9 Ubuntu and Debian):
       
    10 
       
    11 diff -r src-orig/libpolyml/process_env.cpp src/libpolyml/process_env.cpp
       
    12 228c228
       
    13 <                 execve("/bin/sh", argv, environ);
       
    14 ---
       
    15 >                 execvp("bash", argv);
       
    16 
     6 
    17 
     7 The included build script is used like this:
    18 The included build script is used like this:
     8 
    19 
     9   ./build src x86-linux --with-gmp
    20   ./build src x86-linux --with-gmp
    10   ./build src x86_64-linux --with-gmp
    21   ./build src x86_64-linux --with-gmp
    16 Also note that the separate "sha1" library module is required for
    27 Also note that the separate "sha1" library module is required for
    17 efficient digestion of strings according to SHA-1.
    28 efficient digestion of strings according to SHA-1.
    18 
    29 
    19 
    30 
    20         Makarius
    31         Makarius
    21         31-Jan-2016
    32         11-Feb-2016