Re: [isabelle] Creating ML data is slow. No sharing/caching?

Weâve observed similar things in the past with printing large goal states and Simpl terms, esp when lots of abbreviations are active.

It has gotten below the pain threshold for us, I think mainly after Makarius reorganised the whole syntax stack a few years ago, so we havenât done anything about it in a long time. (Maybe we just got used to it too much).

If someone feels motivated to look at what exactly is taking so long in printing and if there is anything that could be done about it, weâd be happy to help and dig out examples.


> On 30.07.2015, at 04:35, C. Diekmann <diekmann at> wrote:
> ... I just wanted to share those numbers in the previous mail. I never
> thought that writing a custom toString function can make such a huge
> difference. 30min vs. 30sec. The tested data is a ~500 rules iptables
> firewall [1]
>  Cornelius
> (and probably I should unify my mail clients key binding to avoid
> those half-finished mails. Sorry for the noise.)
> [1] paper at FM'15


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.