Hi David,
just wanted to confirm that the L4.verified Isabelle proofs run fine with the polyml 5.5 release, with much increased performance.
As you might have seen on isabelle-users, because of the better memory handling (combined with a machine with a lot of memory), we can now make full use of Isabelle's concurrency features and have reduced our run time from 8h to 3h, if pushed hard to 2.5h.
Thanks for the awesome work!
Cheers, Gerwin
On 15/09/2012, at 6:16 PM, David Matthews David.Matthews@prolingua.co.uk wrote:
I have finally released Poly/ML 5.5 on the SourceForge site. I still need to finish the release notes and update the Poly/ML web site. The major change is of course the complete rewrite of the storage management with the garbage-collector now parallelised. In testing the GC sharing pass made a dramatic difference to large Isabelle examples. It would be interesting to know if this makes a difference to other examples.
Other major changes are:
PolyML.shareCommonData has been parallelised and improved.
Support for 64-bit under Windows (Visual Studio or mingw).
Object files now use standard "text" and "data" areas when exporting. In particular this means that it is no longer necessary to use --segprot on Mac OS X to avoid a bus error.
Libffi is used for the foreign-function interface (CInterface structure). In particular this means that the full range of data types are supported on X86/64.
Support for native code on PPC and Sparc has been withdrawn.
There are quite a few other minor changes and bug fixes.
David _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml