[isabelle-dev] Performance of "class" command

[ballarin at in.tum.de]

Quoting Brian Huffman <brianh at cs.pdx.edu>:

> Sometimes the "class" command can be rather slow, for example:
>
> class archimedean_field = ordered_field +
>   assumes ex_less_of_nat: "EX n. x < of_nat n"
>
> ### command "class"
> ### User 2.596  All 2.604 secs
>
> For comparison, deriving from earlier classes is a lot faster:
>
> class archimedean_field = semiring_1 + ord +
>   assumes ex_less_of_nat: "EX n. x < of_nat n"
>
> ### command "class"
> ### User 0.272  All 0.272 secs

Processing times in this order of magnitude indicate that the locale  
(underlying the class construction) contains (theorem) declarations  
that are inherently slow to process (for example, with attributes  
[simplified] or [folded]).  The diagnostic command

   print_locale! L

will print all theorems of locale L (along with its parameters and  
assumptions).  I just cannot remember from the top of my head what the  
locale underlying class C is called: C, C_class, C_locale, but you can  
use

   print_locales

to obtain a list of all locales.

> And finally, a temptation to just give up and use "axclass":
>
> axclass archimedean_field < ordered_field
>   ex_less_of_nat: "EX n. x < of_nat n"
>
> ### command "axclass"
> ### User 0.008  All 0.008 secs

Now that, of course, would be heresy ;-)  Better to buy a faster computer ...

Clemens