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

[Bertram Felgenhauer]

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.

> 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.

Cheers,

Bertram