Hi, Makarius! It's great to hear from you.
Yes, I must confess that until yesterday I had been using Poly/ML version
5.3. I had not upgraded for years. Partly it was because I was working with
both Moscow ML and Poly/ML at the same time, and even Poly/ML 5.3 was so
much faster than Moscow ML that I never felt the need for any improvement.
But in hindsight I should have upgraded earlier.
In my work I haven't been concentrating on the speed or size of HOL-Omega,
but rather on its functionality and correctness. Perhaps the others on the
hol-info mailing list would have more to add about Poly/ML's performance.
But for myself, given your glowing comments, I look forward to enjoying
these great improvements in Poly/ML.
Peter
On Tue, Mar 5, 2013 at 5:02 AM, Makarius <[email protected]> wrote:
> On Mon, 4 Mar 2013, Peter Vincent Homeier wrote:
>
> There was a bug in the previous version of the HOL-Omega system which
>> prevented it from building with Poly/ML 5.5, the current version of
>> Poly/ML.
>>
>> This has been fixed and posted to the public repository for HOL-Omega,
>> and the current version should build correctly. If anyone has tried
>> building HOL-Omega and been frustrated, please try again with this new
>> version of HOL-Omega.
>>
>
> In your changeset
> https://github.com/mn200/HOL/**commit/9b92ae9<https://github.com/mn200/HOL/commit/9b92ae9>you
> say
>
> ... caused a type error with Poly/ML version 5.5. This is a difference
> from Poly/ML version 5.3.
>
> Does it mean you were still using old Poly/ML 5.3 until recently?
>
> For Isabelle, the advances from 5.3 to 5.4 to 5.5 made a big difference in
> performance. 5.5 is particularly nice, since it allows to run even big
> sessions in plain-old 32bit address space -- due to the online sharing of
> immutable data that David Matthews is doing now for all of us.
>
> How is the situation for HOL4 concerning Poly/ML performance?
>
>
> Makarius
>
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_feb
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
