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