[isabelle-dev] Performance of datatype_new

[Jasmin Christian Blanchette]

Hi Makarius,

Am 12.03.2014 um 13:33 schrieb Makarius <makarius at sketis.net>:

> In Isabelle/4d46d53566e6 I've now made the innermost Proof_Context.transfer_syntax more efficient, by switching to a locally linear change discipline of the background theory that makes the merges with the corresponding tables within the proof context much more light-weight.

This is great news! Thank you very much on behalf of the BNF developers. ;) Your change is very visible on the runtime of the "HOL-BNF_Example" session (with full tests enabled), which is now almost twice as fast.

> macpro ad6bd8030d88
> $ isabelle build -c -D Datatype_Test
> Finished Datatype_Test_Old (0:14:31 elapsed time, 0:27:18 cpu time, factor 1.88)
> Finished Datatype_Test_New (0:05:11 elapsed time, 0:10:47 cpu time, factor 2.08)
[...]
> The first observation is that datatype_new is actually faster!  Are there further observations from early adopters of what is actually a quite advanced definitional tool suite awaiting the release this summer.

Here are some more observations:

1. For small datatypes, "datatype_new" tends to be something like five times slower than "datatype" (before your above change). This partly reflects the fact that it offers more (e.g. "map", "set", and "rel" constants and theorems), but mostly of its functorial architecture, with BNF composition taking a significant portion of the time. (The "bnf_timing" configuration option is helpful to obtain detailed timings.) We have made big progresses in the past month; indeed, the above "Datatype_Test_New" suite used to take 40 minutes when René first sent it to us.

2. For large sets of mutual datatypes, "datatype_new" tends to be slower again. Last time Dmitriy ran "HOL-Datatype_Benchmarks" with "datatype_new" instead of "datatype", it took about 1 hour vs. 15 minutes for "datatype".

3. But for nested datatypes, "datatype_new" is usually faster because of its truly modular approach to nesting. The IsaFoR benchmarks above are revealing in this respect. There's a 5-way mutual recursion in it, but with nesting. With the old "datatype", the nesting gets expanded into a 16-way mutual recursion (IIRC), which explains why "datatype_new" wins by such a margin.

Jasmin