[isabelle-dev] Speed of @{thm}

[Makarius]

On Sat, 11 Aug 2012, Jasmin Blanchette wrote:

> Am 10.08.2012 um 23:43 schrieb Makarius:
>
>> On Fri, 10 Aug 2012, Jasmin Blanchette wrote:
>>
>>> The slowdown is neither in "put_thms" nor "the_thm(s)", but apparently 
>>> rather in the compiler somehow. The ML code in "ml" appears to be 
>>> executed two orders of magnitude slower than normal ML code. For 
>>> example, a single call to "ML_Context.the_local_context ()" takes 40 
>>> microseconds normally, but 6 milliseconds when it occurs in the #1 
>>> component of "ml" and 23 milliseconds if it occurs in the #2 
>>> component.
>>
>> I have made similar observations.  Toplevel.profiling shows a lot of 
>> genuine compiler readings, so I would say it is one of the mysteries of 
>> how David Matthews generates code.
>>
>> If you can continue with some local workarounds for now, I will later 
>> look again into the ML antiquotation wrapper, to eliminate most of 
>> these odd ML_Context.the_local_context () invocations.

See Isabelle/37cd53e69840, which is a bit better, but not quite a factor 
of 10.  At least the HOL image requires now 10s less CPU time, which is 
already something.

It seems that the code optimization of Poly/ML costs quite a bit for these 
large arrays of bindings.  The complexity is non-linear: beyond a few 
hundred antiquotation bindings per file the runtime to build up the 
environment becomes very noticeable.

It already helps if ML files are not made too big (20-50kb), with not too 
many things being antiquoted.


 	Makarius