Hi all,
I am trying to profile a piece of Isabelle code (with profiling type 1), and in the end I get a report like the following:
24 Term_Subst.instT_same(3)subst_typ(1) 24 Term.abstract_over(2)abs(2) 26 Term.fastype_of1(2) 27 Ord_List.union(3)unio(2) 28 TextIO.openAppend(1) 28 Term_Subst.instT_same(3)subst_typs(1) 32 Table().lookup_key(2)look(1) 33 BasicStreamIO().flushOut'(1)flushBuff(1) 35 Ord_List.unions(2)unios(2) 39 Thm.deriv_rule2(3) 41 Table().del(3) 43 TextIO.input'(1) 44 Term_Subst.inst_same(4)subst(1) 52 Table().lookup_key(2)look(1) 57 Term_Ord.atoms_ord(2) 62 Sorts.mg_domain(3) 70 Term_Ord.types_ord(2) 77 Table().lookup_key(2)look(1) 79 Table().modify(3)modfy(1) 80 Term_Ord.struct_ord(2) 87 Table().defined(2)def(1) 149 GARBAGE COLLECTION (minor collection) 150 GARBAGE COLLECTION (total) 13313 UNKNOWN
What does UNKNOWN mean? Is there anything I can do to make the result more meaningful?
Alex