[isabelle-dev] Speed of @{thm}

[Jasmin Blanchette]

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.

Sounds good. Thanks!

Jasmin