There's no command to show such a list directly, but it can be constructed from information provided by the program. There are many ways to do this (and maybe someone has a better way) but here is one way:
MM> open log usage.txt MM> show usage * Statement "a1ii" is not referenced in the proof of any statement. (None) Statement "idi" is directly referenced in the proofs of 15 statements: opfi1uzind opfi1uzindOLD opphllem2 madjusmdetlem2 frege55lem2a fsovrfovd imo72b2lem0 ssmapsn fprodcnlem dvmptfprod dvnprodlem1 sge0f1o ovncvr2 pfxcl rngcifuestrc Statement "wn" is directly referenced in the proofs of 7242 statements: con4i con4d pm2.21i pm2.21d pm2.21 pm2.24 pm2.18 pm2.18i pm2.18d notnotr ... MM> close log You can then grep for "referenced in the proof" in usage.txt, which will extract the lines with the usage numbers, then you can sort those lines. If you don't want the syntax axioms like "wn", you can extract all non-syntax $a and $p labels from the output of "search * '|-'". You can prefix this label list with "show usage " then use it as a command file for the "submit" command in metamath.exe, instead of the "show usage *" command that I show above. If you don't have a bash shell, the "tools" command provides processing functions that can accomplish what you need (extracting labels, sorting, etc.), if less efficiently. Sometimes I use it just because unlike bash tools, there are no special characters to remember to escape (other than quotes inside of a quoted string) that can make matching set.mm graphics symbols tricky. Whether to make an actual script as opposed to just typing in the commands is up to you, depending on whether this is a one-off effort. Even if I planned to build a script, I would probably type them in first, saving everything to a log file, and use that to guide constructing a script once I'm happy with the output. Norm On Monday, July 19, 2021 at 3:07:07 PM UTC-4 kylew... wrote: > Hello all, > > I was wondering if it is possible to create a list of the most frequently > used assertions in set.mm using the commands of the Metamath program. I > know that the description of syl has the next five most popularly > referenced assertions, but I would like to extend this out to the next 100, > or 1000 most referenced. > > Thanks in advanced, > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/73d38c6c-256d-4b35-a73f-3f3ffe169148n%40googlegroups.com.
