[isabelle-dev] Speed of @{thm}

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

256 @{thm} antiquotations now take less than 0.5s, and 500 approx. 1s.


Some side remarks:

   * "declare [[ML_trace]]" produces helpful output of the ML source
     produced from antiquotations.

   * "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.


 	Makarius