[isabelle-dev] Speed of @{thm}

[Jasmin Blanchette]

Am 10.08.2012 um 22:21 schrieb Makarius:

> On Fri, 10 Aug 2012, Jasmin Blanchette wrote:
> 
>> I'm attaching my test files for the record. Dmitriy tried these already and confirmed my measurements.
> 
> OK, I will also look for the fat.

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.

Now, here's something really strange. If I replace

    fun thm_bind kind a i =
      "val " ^ a ^ " = the_" ^ kind ^
        " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";

with

    fun my_ctxt () = ML_Context.the_local_context ();

    fun thm_bind kind a i =
      "val " ^ a ^ " = the_" ^ kind ^
        " (my_ctxt ()) " ^ string_of_int i ^ ";\n";

then things get 10 times faster (at least on my copy of "ml_thms.ML", all within the "ML {* *}" tags of a ".thy" file). The truth must be hidden somewhere in "ml_context.ML".

Jasmin