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