[isabelle-dev] Poly/ML x86_64_32 available for testing

[Makarius]

On 23/01/2019 14:14, Bertram Felgenhauer wrote:
> Makarius wrote:
>> On 22/01/2019 12:31, Bertram Felgenhauer wrote:
>>> Makarius wrote:
>>>> So this is the right time for further testing of applications:
>>>> Isabelle2018 should work as well, but I have not done any testing beyond
>>>> "isabelle build -g main" -- Isabelle development only moves forward in
>>>> one direction on a single branch.
>>>
>>> I have tried this with Isabelle2018 and IsaFoR; I've encountered no
>>> problems and there's a nice speedup (estimated 1.25 times faster).
>>> Heap images are 40% smaller, which is a welcome change as well.
>>
>> Is that compared to x86_64 (full 64-bit) or x86 (old 32-bit)?
> 
> This is compared to x86_64. Sorry, I should have mentioned this,
> but to my mind it was implied because IsaFoR is notorious for running
> out of memory with the x86 version of PolyML.

OK, this is the kind of applications that x86_64_32 has been made for:
less memory requirements (< 16 GB) and much faster within it.


>> I am asking this, because I have noted a speedup of building heap
>> images: x86_64_32 compared to x86, and was wondering about the reasons
>> for it. (For x86_64 everything is just more bulky, of course, including
>> heaps.)
> 
> As far as I can see, one difference between x86 and x86_64_32 is that
> PolyML keeps heap objects aligned to 8 byte boundaries for the latter.
> This may impact performance.

I misinterpreted my earlier measurements: the test version is actually a
bit slower in dumping heap images, but x86 is worse than x86_64_32 in
this respect. Something to be investigated further ...


	Makarius