updated to polyml-5.4.1;
authorwenzelm
Sat Oct 15 15:55:10 2011 +0200 (2011-10-15 ago)
changeset 45147c23029f6357f
parent 45146 5465824c1c8d
child 45148 33f0c4a1d25b
updated to polyml-5.4.1;
Admin/CHECKLIST
Admin/polyml/README
etc/settings
src/Pure/ML/ml_compiler_polyml-5.3.ML
     1.1 --- a/Admin/CHECKLIST	Sat Oct 15 00:18:00 2011 +0200
     1.2 +++ b/Admin/CHECKLIST	Sat Oct 15 15:55:10 2011 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  Checklist for official releases
     1.5  ===============================
     1.6  
     1.7 -- test polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
     1.8 +- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
     1.9  
    1.10  - test Proof General 4.1, 3.7.1.1;
    1.11  
     2.1 --- a/Admin/polyml/README	Sat Oct 15 00:18:00 2011 +0200
     2.2 +++ b/Admin/polyml/README	Sat Oct 15 15:55:10 2011 +0200
     2.3 @@ -1,35 +1,8 @@
     2.4  Poly/ML for Isabelle
     2.5  ====================
     2.6  
     2.7 -This compilation of Poly/ML 5.4 is based on the official sources from
     2.8 -http://www.polyml.org with the following patch from the SVN (which is
     2.9 -also part of the fixes-5.4 source tree):
    2.10 -
    2.11 -------------------------------------------------------------------------
    2.12 -r1214 | dcjm | 2010-09-14 20:03:52 +0200 (Tue, 14 Sep 2010) | 1 line
    2.13 -
    2.14 -Fix to arbitrary precision emulation for X86.  A GC during emulating
    2.15 -an operation could cause the stack to move resulting in the result of
    2.16 -the operation not being stored into the result register.
    2.17 -------------------------------------------------------------------------
    2.18 -diff libpolyml/x86_dep.cpp libpolyml/x86_dep.cpp.orig
    2.19 -1308,1311c1308
    2.20 -<                     if (! inConsts) {
    2.21 -<                         destReg = get_reg(taskData, rrr); // May have moved because of a GC.
    2.22 -<                         *destReg = PolyWord::FromUnsigned(destReg->AsUnsigned()+1);
    2.23 -<                     }
    2.24 ----
    2.25 ->                     if (! inConsts) *destReg = PolyWord::FromUnsigned(destReg->AsUnsigned()+1);
    2.26 -1344,1347c1341
    2.27 -<                     if (! inConsts) {
    2.28 -<                         destReg = get_reg(taskData, rrr); // May have moved because of a GC.
    2.29 -<                         *destReg = PolyWord::FromUnsigned(destReg->AsUnsigned()-1);
    2.30 -<                     }
    2.31 ----
    2.32 ->                     if (! inConsts) *destReg = PolyWord::FromUnsigned(destReg->AsUnsigned()-1);
    2.33 -
    2.34 -------------------------------------------------------------------------
    2.35 -
    2.36 +This compilation of Poly/ML 5.4.1 is based on the official sources
    2.37 +from http://www.polyml.org
    2.38  
    2.39  The included build script is used like this:
    2.40  
    2.41 @@ -42,10 +15,9 @@
    2.42  The multi-platform directory layout for executables and shared
    2.43  libraries accommodates the standard ML_HOME settings for Isabelle.
    2.44  
    2.45 -
    2.46  Also note that the separate "sha1" library module is required for
    2.47  efficient digesting of strings according to SHA-1.
    2.48  
    2.49  
    2.50  	Makarius
    2.51 -	20-Dec-2010
    2.52 +	15-Oct-2011
     3.1 --- a/etc/settings	Sat Oct 15 00:18:00 2011 +0200
     3.2 +++ b/etc/settings	Sat Oct 15 15:55:10 2011 +0200
     3.3 @@ -29,14 +29,14 @@
     3.4  ML_SOURCES="$ML_HOME/../src"
     3.5  
     3.6  # Poly/ML 32 bit (manual settings)
     3.7 -#ML_SYSTEM=polyml-5.4.0
     3.8 +#ML_SYSTEM=polyml-5.4.1
     3.9  #ML_PLATFORM="$ISABELLE_PLATFORM"
    3.10  #ML_HOME="$ISABELLE_HOME/contrib/$ML_SYSTEM/$ML_PLATFORM"
    3.11  #ML_OPTIONS="-H 500"
    3.12  #ML_SOURCES="$ML_HOME/../src"
    3.13  
    3.14  # Poly/ML 64 bit (manual settings)
    3.15 -#ML_SYSTEM=polyml-5.4.0
    3.16 +#ML_SYSTEM=polyml-5.4.1
    3.17  #ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
    3.18  #ML_HOME="$ISABELLE_HOME/contrib/$ML_SYSTEM/$ML_PLATFORM"
    3.19  #ML_OPTIONS="-H 1000"
     4.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Oct 15 00:18:00 2011 +0200
     4.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Oct 15 15:55:10 2011 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  (*  Title:      Pure/ML/ml_compiler_polyml-5.3.ML
     4.5      Author:     Makarius
     4.6  
     4.7 -Advanced runtime compilation for Poly/ML 5.3.0.
     4.8 +Advanced runtime compilation for Poly/ML 5.3.0 or later.
     4.9  *)
    4.10  
    4.11  structure ML_Compiler: ML_COMPILER =