[isabelle-dev] Speed of @{thm}

[Jasmin Blanchette]

Am 10.08.2012 um 20:02 schrieb Makarius:

> 30ms for the conjuring trick with fully abstract @{thm} is odd, it should not happen.  Can you spend some time to figure out the time hole?

The delta between @{thm} and @{fasthm} is really just a couple of lines of code:

      val i = serial ();
      val (a, background') = background
        |> ML_Antiquote.variant kind ||> put_thms (i, ths);
      val ml = (thm_bind kind a i, "Isabelle." ^ a);

So the slowdown must be in either "put_thms" or "the_thm(s)". I'll have a closer look.

I'm attaching my test files for the record. Dmitriy tried these already and confirmed my measurements.

Jasmin

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Speed.thy
Type: application/octet-stream
Size: 28985 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120810/4b760267/attachment-0004.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: speed.ML
Type: application/octet-stream
Size: 6558 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120810/4b760267/attachment-0005.obj>