[isabelle-dev] Speed of @{thm}

[Jasmin Blanchette]

Hi Makarius,

> This is the situation in Isabelle/e955964d89cb:
> 
>  more direct embedding of abstract thm values into the ML environment --
>  avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation
>  time for Poly/ML 5.4.x;

This is very nice!! Thank you for looking into this so quickly!

> This means there is just one lookup into the context, and the bindings are done via list pattern matching.  This approach happens to scale into the range of 1000-2000 variables, beyond that it is getting difficult again.

Thankfully, Dmitriy's 1270 or so @{thm}s are spread over several files (and we can break up the files further if necessary).

> Some side remarks:
> 
>  * "declare [[ML_trace]]" produces helpful output of the ML source
>    produced from antiquotations.

Nice.

>  * "ML {* Toplevel.timing := true *}" makes TTY commands emit timing
>    information implicitly, although that spams the Proof General
>    *response* buffer.
> 
>  * Timing of commands is always enabled in the Prover IDE.  Results can
>    be seen in the command status markup in Sidekick with the
>    "isabelle-raw" parser.
> 
>  * Multiple theorems can be grouped: @{thms foo bar baz} produces a list
>    of facts as expected; no need for [@{thm foo}, @{thm bar}, @{thm baz}]
> 
>  * ML files that are "used" within a theory should not become arbitrary
>    large.  The system needs to manage them as a single blob, while for
>    theory sources every command is one small unit.  20-50kb should be
>    still healthy, although external files are not yet wired up with the
>    PIDE markup protocol, so the overall impact is unknown.

Some of these were known to me (e.g. the "Toplevel.timing" feature is extremely useful to find out whether "blast" or "auto" is faster for a specific goal). Dmitriy noticed that performance decreased significantly when he moved his ML code from ".thy" files to ".ML" files, probably because he had many smaller "ML {* *}" blocks before.

Thanks again!

Jasmin