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 <[email protected]> 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 > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
