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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev