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
David,
Many thanks for the new release. ProofPower builds and test fine on it. I don't have any specific feedback on performance yet - the build process itself is somewhat atypical.
On 15 Sep 2012, at 09:16, David Matthews wrote:
... 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.
I have make files that detect Mac OS X and insert the -segprot option automatically. Should I change these to be more specific about Poly/ML versions, or is it harmless to continue to give the -segprot option?
Regards,
Rob.
On 17/09/12 00:02, Rob Arthan wrote:
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.
I have make files that detect Mac OS X and insert the -segprot option automatically. Should I change these to be more specific about Poly/ML versions, or is it harmless to continue to give the -segprot option?
I have the same question.
Michael
On 17/09/2012 02:32, Michael Norrish wrote:
On 17/09/12 00:02, Rob Arthan wrote:
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.
I have make files that detect Mac OS X and insert the -segprot option automatically. Should I change these to be more specific about Poly/ML versions, or is it harmless to continue to give the -segprot option?
I have the same question.
If the linker doesn't complain then I don't see any harm in continuing to provide it.
The option says: set the protection on the "segment" (Mac object-file terminology) called "POLY" to be read/write/execute. There no longer is a segment called "POLY" so it's possible, but unlikely, that the linker might complain.
The reason for using the option was that Poly's object-file exporter used to put everything into a single segment and set the protection bits in the object file to read/write/execute. It seems that the linker removed the execute permission which had no effect on 32-bit which doesn't check the execute bit but caused a bus error on 64-bit when trying to execute code in the final executable. Poly/ML 5.5 splits the object file into code (read/execute) and data (read/write) which is the way other languages work. The linker sets the correct permissions without the need for an option.
David
On Sat, Sep 15, 2012 at 9:16 AM, 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.
I guess that also means updating the fixes-5.5 branch? I just built r1595 from that, but the executable still calls itself 5.4.1 Release. (Or maybe I didn't do enough cleaning before building?)
On 17/09/2012 10:31, Ramana Kumar wrote:
On Sat, Sep 15, 2012 at 9:16 AM, 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.
I guess that also means updating the fixes-5.5 branch? I just built r1595 from that, but the executable still calls itself 5.4.1 Release. (Or maybe I didn't do enough cleaning before building?)
Are you sure you checked out the 5.5 branch? You need something like svn co https://polyml.svn.sourceforge.net/svnroot/polyml/fixes-5.5/polyml polyml-5.5fixes I don't think you can switch the 5.4 branch over but maybe there's some svn command to do it. It's probably simpler just to check out the correct branch.
David
On 17/09/12 11:30, David Matthews wrote:
Are you sure you checked out the 5.5 branch? You need something like svn co https://polyml.svn.sourceforge.net/svnroot/polyml/fixes-5.5/polyml polyml-5.5fixes I don't think you can switch the 5.4 branch over but maybe there's some svn command to do it. It's probably simpler just to check out the correct branch.
"svn switch" is the command you want, for future reference...
I cleaned out my build directory and tried again; now I have 5.5.0 as expected. Thanks. (I don't deal with svn commands directly; I maintain https://aur.archlinux.org/packages.php?ID=28880 and the build scripts do the checkout under the hood.)
Building HOL4 with 5.5.0 seems to be very slow, compared to 5.4.1. I don't have numbers yet, just an impression. Any clues why this might be? Are the release notes online?
On Mon, Sep 17, 2012 at 11:58 AM, Alex Merry alex.merry@cs.ox.ac.uk wrote:
On 17/09/12 11:30, David Matthews wrote:
Are you sure you checked out the 5.5 branch? You need something like svn co https://polyml.svn.**sourceforge.net/svnroot/** polyml/fixes-5.5/polymlhttps://polyml.svn.sourceforge.net/svnroot/polyml/fixes-5.5/polymlpolyml-5.5fixes I don't think you can switch the 5.4 branch over but maybe there's some svn command to do it. It's probably simpler just to check out the correct branch.
"svn switch" is the command you want, for future reference...
-- Alexander Merry DPhil Computer Science Department of Computer Science University of Oxford
______________________________**_________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/**mailman/listinfo/polymlhttp://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 17/09/2012 16:22, Ramana Kumar wrote:
Building HOL4 with 5.5.0 seems to be very slow, compared to 5.4.1. I don't have numbers yet, just an impression. Any clues why this might be? Are the release notes online?
I've updated the release notes which list the changes but I really need to go through and add more documentation. If 5.5 really is slower with HOL4 I would like to know why. Measurements with Isabelle show big improvements.
David
Building HOL4 with 5.5.0 seems to be very slow, compared to 5.4.1. I don't have numbers yet, just an impression. Any clues why this might be? Are the release notes online?
I encountered poor performance the first time I did a HOL4 build under Poly/ML 5.5, but now I?m almost certain that this must have been due to other processes that were running at the same time.
I?ve now built HOL4 using Poly/ML 5.5 a few times and on a couple of different machines. Scott Owens has also done a build as well. My conclusion is that, in the context of HOL4, version 5.5 offers a modest speedup over 5.4.1 (I?d say under 10% faster overall).
Anthony Fox
On 18/09/2012 19:24, Anthony Fox wrote:
I encountered poor performance the first time I did a HOL4 build under Poly/ML 5.5, but now I?m almost certain that this must have been due to other processes that were running at the same time.
I?ve now built HOL4 using Poly/ML 5.5 a few times and on a couple of different machines. Scott Owens has also done a build as well. My conclusion is that, in the context of HOL4, version 5.5 offers a modest speedup over 5.4.1 (I?d say under 10% faster overall).
That's fine. I was concerned about the possibility that it might have been slower than 5.4.1 but if there's a small speed-up I'm quite happy. If GC time is not a significant factor for you then any improvement in it will only produce a marginal improvement.
David
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
-
acjf3＠cam.ac.uk -
alex.merry＠cs.ox.ac.uk -
David.Matthews＠prolingua.co.uk -
kleing＠cse.unsw.edu.au -
michael.norrish＠nicta.com.au -
ramana.kumar＠gmail.com -
rda＠lemma-one.com