Re: [isabelle] Slow rule application in case of many parameters?
It looks like you are working on rather large problems! Still I don't
think such runtimes should be normal. Are you using Poly/ML? Does your
machine have ample memory?
On 15 Mar 2009, at 20:32, Dennis Walter wrote:
I'm having problems solving large structured goals involving many
parameters. Even rule applications like
apply (rule allI | rule impI | erule conjE)+
take several minutes. I've experienced this slowdown in cases where
the number of parameters (bound meta-variables) is > 30, and these
repeatedly occur in various places within the goal (~2000 lines, no
abbreviations). I suspect that Isabelle's lifting of rules over
parameters is to blame, but I can't see why this should be the case.
Can anybody explain this phenomenon to me?
Thanks a lot,
This archive was generated by a fusion of
Pipermail (Mailman edition) and