[isabelle-dev] Speed of @{thm}

[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.


 	Makarius