[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