[isabelle-dev] Performance of "class" command

Brian Huffman brianh at cs.pdx.edu
Wed Feb 25 00:57:08 CET 2009


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

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

I don't know what the "class" command is doing behind the scenes, but  
is it supposed to be taking this long? Should this be considered a  
performance bug?

- Brian





More information about the isabelle-dev mailing list