Admin/polyml/README
changeset 45147 c23029f6357f
parent 41331 8cdadd543fc8
child 49400 f0c86a5ef4e2
equal deleted inserted replaced
45146:5465824c1c8d 45147:c23029f6357f
     1 Poly/ML for Isabelle
     1 Poly/ML for Isabelle
     2 ====================
     2 ====================
     3 
     3 
     4 This compilation of Poly/ML 5.4 is based on the official sources from
     4 This compilation of Poly/ML 5.4.1 is based on the official sources
     5 http://www.polyml.org with the following patch from the SVN (which is
     5 from http://www.polyml.org
     6 also part of the fixes-5.4 source tree):
       
     7 
       
     8 ------------------------------------------------------------------------
       
     9 r1214 | dcjm | 2010-09-14 20:03:52 +0200 (Tue, 14 Sep 2010) | 1 line
       
    10 
       
    11 Fix to arbitrary precision emulation for X86.  A GC during emulating
       
    12 an operation could cause the stack to move resulting in the result of
       
    13 the operation not being stored into the result register.
       
    14 ------------------------------------------------------------------------
       
    15 diff libpolyml/x86_dep.cpp libpolyml/x86_dep.cpp.orig
       
    16 1308,1311c1308
       
    17 <                     if (! inConsts) {
       
    18 <                         destReg = get_reg(taskData, rrr); // May have moved because of a GC.
       
    19 <                         *destReg = PolyWord::FromUnsigned(destReg->AsUnsigned()+1);
       
    20 <                     }
       
    21 ---
       
    22 >                     if (! inConsts) *destReg = PolyWord::FromUnsigned(destReg->AsUnsigned()+1);
       
    23 1344,1347c1341
       
    24 <                     if (! inConsts) {
       
    25 <                         destReg = get_reg(taskData, rrr); // May have moved because of a GC.
       
    26 <                         *destReg = PolyWord::FromUnsigned(destReg->AsUnsigned()-1);
       
    27 <                     }
       
    28 ---
       
    29 >                     if (! inConsts) *destReg = PolyWord::FromUnsigned(destReg->AsUnsigned()-1);
       
    30 
       
    31 ------------------------------------------------------------------------
       
    32 
       
    33 
     6 
    34 The included build script is used like this:
     7 The included build script is used like this:
    35 
     8 
    36   ./build src x86-linux --with-gmp
     9   ./build src x86-linux --with-gmp
    37   ./build src x86_64-linux --with-gmp
    10   ./build src x86_64-linux --with-gmp
    40   ./build src x86-cygwin --with-gmp
    13   ./build src x86-cygwin --with-gmp
    41 
    14 
    42 The multi-platform directory layout for executables and shared
    15 The multi-platform directory layout for executables and shared
    43 libraries accommodates the standard ML_HOME settings for Isabelle.
    16 libraries accommodates the standard ML_HOME settings for Isabelle.
    44 
    17 
    45 
       
    46 Also note that the separate "sha1" library module is required for
    18 Also note that the separate "sha1" library module is required for
    47 efficient digesting of strings according to SHA-1.
    19 efficient digesting of strings according to SHA-1.
    48 
    20 
    49 
    21 
    50 	Makarius
    22 	Makarius
    51 	20-Dec-2010
    23 	15-Oct-2011