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 |